［開発者向け］AIが書いたコードを「証明」で縛る——MicrosoftのPDD KitでWebアプリのログインを形式検証

2026-11-08

はじめに

　Microsoft Researchは2026年11月5日、AIエージェントが書いたコードを数学的に検証するツールキット「PDD Kit」を紹介しました。Rust製のWebアプリのログイン処理を題材に、意図を仕様に落とし込み、証明とテストで裏付けるまでの流れを示しています。本稿ではその仕組みと手順を整理します。

参考記事

タイトル: Formally verifying agent-written full-stack web apps with PDD Kit
著者: Alex Lavaee, Matthai Philipose
発行元: Microsoft Research
発行日: 2026年11月5日
URL: https://www.microsoft.com/en-us/research/blog/formally-verifying-agent-written-full-stack-web-apps-with-pdd-kit/

要点

PDD Kitは、開発者の意図を形式仕様に変換し、エージェントが書いたコードがあらゆる入力でその仕様を満たすことを証明するツールキットである。証明が届かない部分はテストで補う
検証ツールにはRust向けの証明言語「Verus」を使い、GitHub Nextの共同計画環境「Chopin」の中で動作する
約5,000行のRust製Webアプリ「Pet Store」のログイン処理を対象に、2文の要件から8つの仕様条項を導き、その正しさを証明した
証明の対象外となる外部ライブラリや時計などは「信頼境界」として明示され、開発者が1つずつ承認し、テストで確認する
開発者は生成コードを1行ずつ読まず、平易な言葉で書かれた意図をレビューした。レビューの重心をコードから意図へ移す試みである

詳細解説

背景——「計画」は契約のはずだが、守らせる仕組みがない

　Microsoft Researchによれば、コーディングエージェントは数万〜数十万行に及ぶ機能を一度に作るようになり、プルリクエストを1行ずつ読むレビューは追いつかなくなりつつあります。そこで多くのチームは、エージェントと計画やテスト方針をすり合わせ、それを渡して実装させる形に移っています。

　ただし、この計画（自然言語の仕様）には、エージェントに守らせる強制力がありません。エージェントは少し違うものを実装し、自分の実装に合わせたテストを書いてしまうことがあります。テストが増えてカバレッジは良く見えても、依頼内容と実装のずれはバグ報告が来るまで見えないままだと指摘されています。AIが書いたコードのレビューをどう考えるかについては、GitHubが俗説を整理した記事でも議論されていました。

　原文は、レビューが「正しそうに見えるか」を問うのに対し、証明は「正しいか」に答えると対比しています。数学的な証明は、テストが見落とす入力も含めてすべての入力でコードが仕様を満たすことを示します。かつては専門家や特殊な言語が必要で、証明がコードの何倍もの量になるため日常的なソフトウェアには使いにくい手法でした。しかし、エージェントが形式仕様の作成と証明の生成の両方を手伝えるようになったことで状況が変わったとしています。Microsoft Researchはこれを「証明駆動開発（Proof-Driven Development、PDD）」と呼び、そのためのツールキットがPDD Kitです。

PDD Kitの仕組み——形式検証と経験的検証を明確に分ける

　原文は、PDD Kitと形式手法の関係を、GitHubの「Spec Kit」と仕様駆動開発の関係にたとえています。PDD Kitは、チームとエージェントが1つの文書で計画を立てられるGitHub Nextのリアルタイム共同計画環境「Chopin」の中で動作します。

　ワークフローは前半と後半に分かれます。前半では、チームが平易な言葉で意図を確認します。PDD Kitは注意深いレビュアーがするような質問を投げかけ、関連するコードを説明しながら、その回答を「意図アーティファクト」という文書に記録します。形式化できる意図は形式仕様に、信頼に委ねるしかない部分はテスト用の非形式な仕様に変換されます。後半では、形式仕様を満たす証明と、非形式仕様に対するテストが自動生成されます。形式手法の知識は不要だと説明されています。

　PDD Kitの結果には、どちらの検証に基づくかが必ず示されます。

形式検証: コードがあらゆる入力で仕様を満たすことを、検証器が数学的に確認する。現在の検証器はVerusで、Microsoft Research、カーネギーメロン大学、VMware Research、ETHチューリッヒなど多数の機関が共同開発したRust向けの証明言語である
経験的検証: コードを実行して挙動を観察する。サードパーティの暗号ライブラリやUIなど、証明が届かない部分を対象とし、単体テスト、E2Eテスト、ターミナル自動化、ブラウザエージェント、コンピュータ操作エージェントを使う。テストの合格は「試した入力で動いた」ことしか示さないため、PDD Kitはこれを証明ではなく「証拠」として扱う

　両者の境界にあたるのが「信頼済みコンピューティング基盤（TCB）」です。証明が「記述どおりに動く」と仮定しているコードを指し、PDD Kitはこの境界を明示したうえで、開発者に1つずつ承認を求めます。本稿としては、「何を証明し、何を信頼しているか」を常に表示する設計が、形式手法を過信させないための要になっていると受け止めています。

前提条件・環境構成——題材はRust製のフルスタックWebアプリ

　既存のコードベースに組み込めることを示すため、Microsoft Researchは全編Rustで書かれたWebアプリ「Pet Store」を用意しました。構成は次のとおりです。

バックエンド: AxumとSQLiteで構築し、在庫・プロモーション・注文・決済を扱う
フロントエンド: Leptosで書かれ、WebAssemblyにコンパイルされたストアフロント
規模: 合計約5,000行のRust

　記事ではログイン処理に絞って検証していますが、同じ手順でアプリ全体の機能的な正しさも検証できるとしています。PDD Kitは、最も重要な部分から始めて段階的に検証範囲を広げることを推奨しています。ログインのバグは顧客のアカウントや管理者権限を攻撃者に渡しかねないため、証明の効果が最も出やすい箇所という位置づけです。

　開発者がChopinで出した依頼は、次の2文だけでした。

Verify the login logic in backend/src/handlers/auth.rs. Here are my requirements:

You only get a token with the right password.

Only admin accounts get admin tokens.

　「backend/src/handlers/auth.rsのログイン処理を検証してほしい。要件は、1. 正しいパスワードのときだけトークンが得られること、2. 管理者アカウントだけが管理者トークンを得られること」という内容です。依頼はあえて粗いままにしており、それを証明可能な形にするのがPDD Kitの役割だとしています。

Step 1〜3: 質問、意図マップ、証明範囲の決定

　ここから原文は7つのステップで流れを説明しています。

　Step 1: コードを書く前に質問する。 計画ワークフロー「pdd-plan」はコードを読み、何かを書く前に「Decisions」タブで質問を返します。質問がコードの動作に関わる場合は、目的や関連する関数を先に説明するため、開発者はソースを開かずに答えられます。

　最初の質問は「正しいパスワードなら必ずトークンが得られるべきか」でした。「正しいパスワードのときだけトークンを渡す」という要件は、誰も通さないログインでも満たせてしまいます。論理的には前者が「トークン ⇒ 正しいパスワード」という含意で、「正しいパスワードなら必ず通る」はその逆です。両方そろって初めて「〜のときに限り」（必要十分条件）になります。エージェントに任せると黙ってどちらかを選びかねないところを、開発者は両方向の証明を選びました。

　Step 2: 人が読める意図マップ。 PDD Kitは計画の冒頭に「rough work」欄を設け、合意した内容を長いチャットをさかのぼらずに確認できるようにします。ここには、ログインのフローチャート、何を証明し何を信頼するかの一覧、必要に応じてメンタルモデルの図が置かれます。ログインについては「チケット窓口」のたとえが描かれました。送ったフィールドで窓口が決まり、窓口でテーブルと役割が決まり、パスワードが一致するまでチケットは発行されない、という図式です。

　その下の「意図マップ」は、各要件を開発者自身の言葉に結びつけ、どう決着したかを記録します。各項目は対応する形式仕様の箇所とテストにリンクされます。原文によれば、2つの解釈の違いは表の1マスだけ、つまり「正しいパスワードなのにトークンが出ない」場合だけで、そのマスが証明すべき内容を変えるとしています。

　Step 3: ログイン関数の証明範囲を決める。 PDD Kitは実装前に計画全体の承認を求めます。最初の案では、ログインの中心にある判断（テーブルの選択とパスワードによる関門）を証明し、その周囲のハンドラーは信頼してテストする構成でした。PDD Kitもこれを推奨しましたが、開発者はさらに踏み込みました。ハンドラーは検索結果を待ち受けてトークンに署名する部分で、リファクタリングで2行が入れ替わるような事故が起きやすいためです。開発者はハンドラーにも非同期関数としての仕様を与え、その「つなぎ」も証明の対象にしました。その結果、リクエストのフィールドからトークンまたはHTTPエラーまでを契約で縛る新しい非同期関数login_flowが作られています。PDD Kitは改訂後の計画を改めて承認に回しました。意図に合っていることは証明ではなく、新たな信頼や範囲の拡大を承認したことにもならないためです。

Step 4: 証明が届かない場所と信頼境界

　原文は、プログラムについて証明できないことは多く、ログインはその大半に当てはまると述べ、次の5つを挙げています。

検証器から見えないコード: bcryptのハッシュ処理、sqlxのクエリ、jsonwebtokenの署名は別のクレートにあり、証明の外にある
外部世界に関する事実: SQLiteの現在の中身や時計の時刻はプログラムへの入力であり、コード自身が確定できるものではない
完了するかどうか、どれだけ速いか: 仕様は「ログインが応答したら何が返るか」を定めるもので、止まったクエリや遅いクエリは仕様に反しない
人が判断すべきこと: エラーメッセージが役に立つか、画面が分かりやすいかなど
誰も書かなかったこと: 証明は仕様の範囲しか保証せず、仕様外の要件については何も言わない

　ここで経験的検証の出番になります。PDD Kitは信頼境界を明示し、信頼する部品をそれぞれ小さな関数で包んで「仮定の契約」を付けます。Verusの#[verifier::external_body]またはexternal_fn_specificationを使い、開発者に部品ごとの承認を求め、仮定した条項ごとにテストを計画に書き込みます。ログインでは、開発者は次の6つを承認しました。

2つの検索処理 （Customer::find_by_emailとAdmin::find_by_username）: 成功した検索は、そのメールアドレスまたはユーザー名に対応する行をそのまま返すか、何も返さない
check_password: bcrypt::verifyの薄いラッパー。エラーになるのはbcryptが読めないハッシュの場合だけで、Ok(true)は正しいパスワードを意味する
generate_token: 与えられたクレームを設定済みの秘密鍵で署名し、署名の失敗は500として報告する
expiry_from_now: 時計を読み、ちょうど24時間後の有効期限を書き込む
database_error: 失敗した検索を、sqlxのメッセージを含む500に変換する
ログインハンドラーの外殻: リクエストを展開し、各フィールドをそのままlogin_flowに渡す

　以降のコードは参考記事のものをもとにしています。コメントは日本語に訳しています。また、取得した原文では一部の型引数（山括弧内）が表示上欠落しており、原文の表記のまま掲載しています。正確な型は参考記事で確認してください。

　次のコードは、検索処理のコードはそのままに、external_fn_specificationで外側から契約を与える例です。

/// メールアドレスの完全一致で顧客を検索する。
/// 信頼済みで、証明はしていない: SQLクエリはVerusが検査できないsqlxの中で実行される。
/// `login_flow` の顧客に関する約束はすべてこれに依存する。
#[verifier::external_fn_specification]
pub async fn ex_customer_find_by_email(pool: &sqlx::SqlitePool, email: &str)
    -> (r: Result, sqlx::Error>)
    ensures
        // クエリが成功した場合、このメールアドレスに完全一致する顧客の行を返し、
        // 該当がなければ None を返す。
        r matches Ok(found) ==> found == customer_on_file(email@),
{
    Customer::find_by_email(pool, email).await
}

　ensuresは関数の事後条件（結果が満たすべき性質）を書く節です。続いて、時計を読む小さなラッパーです。#[verifier::external_body]を付けると、Verusはensures節だけを使い、本体は読みません。

/// 時計を読み、トークンの有効期限を24時間後に計算する。
/// 信頼済みで、証明はしていない: chronoの時計は証明の外にある。
/// 現在のログインと同様に、時刻が範囲外ならパニックする。
/// そのパニックが起きないことは約束していない。
#[verifier::external_body]
pub fn expiry_from_now() -> (r: Expiry)
    ensures
        // 有効期限は、時計の読み取り値のちょうど24時間後（86,400秒後）である。
        r.exp as int == r.now as int + 86_400,
{
    ...
}

　原文はこの構造を3層で示しています。中心がVerusによってあらゆる入力で証明される部分（login_flow、login_core、lookup_target、decide_login、issue_token）、その外側が人が承認しテストで確認する信頼済みの層、さらに外側が誰も約束しない領域です。信頼に関する判断はそれぞれ1枚のカードになり、Verusが無条件に受け入れる条項、開発者が引き受けるもの、仮定が誤っていた場合に崩れる約束が示されます。仮定した条項にはGiven/When/Then形式のテストシナリオが、テストを書く前に用意されます。実行前は「planned」と表示され、実行後はコマンドの結果と対象コミットが記録されます。

　計画には、誰も約束しないことも明記されます。ログイン処理（Future）が必ず完了すること、範囲外の時刻でパニックしないこと、試行のタイミングや頻度、他のエンドポイントが役割をどう解釈するか、といった点です。

Step 5: 仕様の読み方

　チームがレビューするのは意図アーティファクトで、これはVerusの契約として書かれた形式仕様を平易な言葉で表した文書です。原文は「コードの代わりに証明を読むことになるのか」という疑問に対し、誰も証明を読む必要はないと答えています。証明はエージェントが書き、Verusがすべてのステップを検査するため、Verusが受け入れれば誰かが読んだかどうかに関係なく成り立つからです。人がレビューするのは証明が従う仕様で、数分で読めるようになる程度の分量だとしています。

　各関数にはensuresブロックがあり、結果rについてあらゆる入力で成り立つべき性質を書きます。Verusはビルド時にこれを検査し、1つの入力でも成り立たない可能性があればビルドが失敗し、該当の条項を指摘します。各条項は「もし〜ならば」の形で読めます。

　1つ目の要件に対応する条項では、同じアカウントaがすべての行に登場し、パスワードの確認とトークンを結びつけています。たとえば、ある利用者が自分の正しいパスワードでログインしたのに、別の利用者のアカウントのトークンが返ってくるバグを考えます。各ステップは単独では正しく見えますが、この条項はパスワード確認とトークンが同じアカウントを指すことを求めるため、こうした配線ミスを捉えられます。原文は、テストではなかなか想定されない種類のバグだと述べています。

　仕様は、SQLite、bcrypt、JWTを実行せずに、それらについて語る必要があります。そのために使われるのが「未解釈関数」で、本体を持たない名前だけの関数です。データベースの行を表すcustomer_on_file(email)とadmin_on_file(username)、bcryptの判定を表すbcrypt_verdict(password, hash)、トークンの中身を表すtoken_claims(token, secret)がこれにあたります。Verusはこれらについて、Step 4の信頼済み契約が約束すること以外は何も知りません。証明は「データベースの中身が何であれ、ログインはそれを正しく扱う」ことを示し、信頼済み契約が「検索はデータベースの中身を返す」ことを示す、という分担です。

/// ログイン時点でデータベースが保持している、
/// このメールアドレスに完全一致する顧客の行（あれば）。
/// 抽象のまま残す: その中身を述べるのは
/// `Customer::find_by_email` の信頼済み契約だけである。
pub uninterp spec fn customer_on_file(email: Seq) -> Option;
...
/// 保存された `hash` に対して `password` をbcryptがどう判定するか:
/// ハッシュの元になったパスワードなら Some(true)、
/// そうでなければ Some(false)、ハッシュを読めなければ None。
/// 抽象のまま残す: その意味はbcryptのもので、`check_password` を通じて信頼される。
pub uninterp spec fn bcrypt_verdict(password: Seq, hash: Seq)
    -> Option;

/// bcryptの判定により、保存されたハッシュに対して正しいパスワードであること。
pub open spec fn password_matches(password: Seq, hash: Seq) -> bool {
    bcrypt_verdict(password, hash) == Some(true)
}

　さらに、ログインがどのアカウントを指すかを定めるnamed_account(email, username)が定義されています。Rustのように書かれていますが、実行されることはなく契約の中にだけ現れる数学的な定義です。こうしたコードは「ゴーストコード」と呼ばれ、検証器は検査しますが、コンパイラはプログラムから取り除きます。

/// ログインが指すアカウント: メールアドレスが送られた場合はその顧客の行（役割 "customer"）、
/// そうでなければユーザー名に対応する管理者の行（役割 "admin"）、どちらもなければ none。
pub open spec fn named_account(email: Option, username: Option)
    -> Option {
    match email {
        Some(e) => match customer_on_file(e@) {
            Some(c) => Some(NamedAccount {
                id: c.id@, password_hash: c.password_hash@, role: customer_role() }),
            None => None,
        },
        None => match username {
            Some(u) => match admin_on_file(u@) {
                Some(a) => Some(NamedAccount {
                    id: a.id@, password_hash: a.password_hash@, role: admin_role() }),
                None => None,
            },
            None => None,
        },
    }
}

　これらを使って、開発者の2文の依頼はlogin_flowの8つのensures条項になりました。うち4つは現在の拒否時の挙動を維持するもので、ストアフロントや既存のAPIテストがそのまま動くようにしています。以下が契約の全体です（ドキュメントコメントは原文でも省略されています）。各条項の上のコメントは、意図アーティファクトでチームに示される平易な説明にあたります。

/// ログイン全体を最後まで待ち受ける: リクエストの
/// フィールドから、トークンまたはHTTPエラーまで。
/// ...
pub async fn login_flow(pool: &sqlx::SqlitePool, config: &Config,
    email: Option, username: Option, password: &str)
    -> (r: Result)
    ensures
        // メールアドレスもユーザー名もない場合: 現在と同じメッセージで400。
        email is None && username is None
            ==> (r matches Err(AppError::BadRequest(m))
                && m@ == missing_identity_text()),
        // トークンは、ログインが指すアカウントに正しいパスワードが
        // 与えられた場合だけ発行され、そのアカウントのIDとテーブルの役割を持つ。
        r matches Ok(t) ==> (named_account(email, username) matches Some(a)
            && password_matches(password@, a.password_hash)
            && token_claims(t@, config.jwt_secret@) matches Some(c)
            && c.sub@ == a.id && c.role@ == a.role),
        // 指定アカウントの正しいパスワードなら必ずトークンが得られる。
        // ただし検索や署名の失敗で500になる場合を除く。
        (named_account(email, username) matches Some(a)
            && password_matches(password@, a.password_hash))
            ==> (r is Ok || r matches Err(AppError::Internal(_))),
        // 存在しないアカウントを指すログインは401。
        // ただし検索の失敗で500になる場合を除く。
        ((email is Some || username is Some) && named_account(email, username) is None)
            ==> (r matches Err(AppError::Unauthorized)
                || r matches Err(AppError::Internal(_))),
        // bcryptが読めるハッシュを持つアカウントへの誤ったパスワードは401。
        // ただし検索の失敗で500になる場合を除く。
        (named_account(email, username) matches Some(a)
            && bcrypt_verdict(password@, a.password_hash) == Some(false))
            ==> (r matches Err(AppError::Unauthorized)
                || r matches Err(AppError::Internal(_))),
        // 保存されたハッシュをbcryptが読めないアカウントは500で、トークンは出ない。
        (named_account(email, username) matches Some(a)
            && bcrypt_verdict(password@, a.password_hash) is None)
            ==> r matches Err(AppError::Internal(_)),
        // 管理者の役割は、メールアドレスなしでユーザー名から
        // 見つかった管理者の行にだけ与えられる。
        (r matches Ok(t) && token_claims(t@, config.jwt_secret@) matches Some(c)
            && c.role@ == admin_role())
            ==> (email is None && username matches Some(u)
                && admin_on_file(u@) is Some),
        // メールアドレスでのログインのトークンは、常に顧客の役割を持つ。
        (r matches Ok(t) && email is Some)
            ==> (token_claims(t@, config.jwt_secret@) matches Some(c)
                && c.role@ == customer_role()),
{
    unimplemented!()
}

　信頼境界はコードにも現れます。check_passwordはVerusが本体を検査しない関数の1つで、その契約は公理を持たないbcryptの未解釈モデルbcrypt_verdictに結びつけられています。

/// `password` が保存された `hash` に一致するかをbcryptに問い合わせる。
/// 信頼済みで、証明はしていない: Verusはbcryptのハッシュ処理を検査できないため、
/// このラッパーの契約は仮定される。
/// `login_flow` のパスワードに関する約束はすべてこれに依存する。
#[verifier::external_body]
pub fn check_password(password: &str, hash: &str) -> (r: Result)
    ensures
        // bcryptが応答する（Ok）のは、保存されたハッシュを読めるときに限る。
        r is Ok <==> bcrypt_verdict(password@, hash@) is Some,
        // その応答は判定そのもの: 正しいパスワードなら true、それ以外は false。
        r matches Ok(b) ==> bcrypt_verdict(password@, hash@) == Some(b),
{
    bcrypt::verify(password, hash).map_err(|e| e.to_string())
}

　原文によれば、ログインの終わり方は400（識別情報なし）、401（アカウントなし・パスワード誤り）、500（検索やハッシュの失敗）など数通りで、トークンが出るのはそのうち1つだけです。証明はそのすべてを一度にカバーします。

　login_flowはデータベースのクエリを待つ非同期関数です。Verusは非同期関数にも契約を付けられますが、覚えておくべき規則が1つあります。requires（事前条件）は呼び出しでFutureが作られる時点で検査され、ensuresはそれを待ち受けて得られる値を記述します。Futureが完了することは約束されないため、止まったクエリはどの条項にも違反しません。login_flowのドキュメントコメントにも、そのことが明記されています。

/// ... Futureが完了することは約束しない。
pub async fn login_flow(...) -> (r: Result)

　login_flowが短く済むのは、小さな証明済みの部品で組み立てられているためです。lookup_targetがテーブルを選び、login_coreが検索を待ってパスワードの関門であるdecide_loginを呼び、issue_tokenがトークンに署名するか、拒否を現在のHTTPエラーに変換します。Verusは各部品の契約だけを使ってlogin_flowを証明し、本体を読み直しません。そのため、decide_loginの本体を変えた場合に再証明されるのはdecide_loginだけです。以下は最小の部品lookup_targetの全体と、パスワード関門decide_loginの冒頭と末尾です。

pub fn lookup_target(email: Option, username: Option)
    -> (r: Result)
    ensures
        // メールアドレスが送られた場合はそれが優先される: 顧客をそのメールアドレスの完全一致で検索する。
        email matches Some(e)
            ==> r == Ok::(LookupTarget::CustomerByEmail(e)),
        // メールアドレスがなければ、ユーザー名で
        // 管理者をその完全一致で検索する。
        email is None && username matches Some(u)
            ==> r == Ok::(LookupTarget::AdminByUsername(u)),
        // どちらもなければ、識別情報の欠如としてログインを拒否する。
        email is None && username is None
            ==> r == Err::(LoginError::MissingIdentity),

pub fn decide_login(target: &LookupTarget, found: Option, password: &str)
    -> (r: Result)
    ensures
        // 行が見つからない場合: パスワードの誤りと同じく
        // Unauthorized として拒否する。
        found is None
            ==> r == Err::(LoginError::Unauthorized),
        // クレームが返るのは、保存されたハッシュがパスワードに
        // 一致する行が見つかった場合だけである。
        r is Ok ==> found is Some
            && password_matches(password@, found->Some_0.password_hash@),
        // 見つかった行に対する正しいパスワードは、必ずクレームを得る。
        found matches Some(a) && password_matches(password@, a.password_hash@)
            ==> r is Ok,
        ...
        // 管理者テーブルの検索では、役割の文字列は "admin" になる。
        r matches Ok(c) && target is AdminByUsername ==> c.role@ == admin_role(),
        // 顧客テーブルの検索では、役割の文字列は "customer" になる。
        r matches Ok(c) && target is CustomerByEmail ==> c.role@ == customer_role(),

　仕様ファイルverified/src/login.rsは、上から順に4つの層で読めるよう構成されています。

ヘッダー・インポート・型: Verusが知る必要のある型の定義
外部世界の抽象的な見方: 契約の中にだけ現れる数学的な定義
信頼済み契約: その抽象と実際のコードをつなぐ部分
5つの契約: 証明が満たすべき関数の仕様

　分かりにくい部分の例として、原文は2つを抜粋しています。external_type_specificationは、Verusが定義していない型を導入します。コネクションプールは中身を隠したまま扱い、顧客の行はフィールドを見える状態にしています。

/// コネクションプール。証明からは中身が見えない:
/// 何を返すかを述べるのは検索処理の契約だけである。
#[verifier::external_type_specification]
#[verifier::external_body]
#[verifier::reject_recursive_types(DB)]
pub struct ExPool(sqlx::Pool);
...
/// 顧客の行。フィールドは証明から見える。
#[verifier::external_type_specification]
pub struct ExCustomer(Customer);

　また、LoginErrorは判断とHTTPレスポンスを分離しています。これにより、issue_tokenで各拒否を現在のステータスコードに対応づけられます。

/// ログインでトークンが得られない理由。
pub enum LoginError {
    /// メールアドレスもユーザー名も送られなかった: 400 Bad Request。
    MissingIdentity,
    /// アカウントが存在しない、またはパスワードが一致しない: 401 Unauthorized。
    Unauthorized,
    /// bcryptが保存されたハッシュを読めなかった（メッセージ付き）: 500 Internal。
    UnreadableHash(String),
    /// 検索クエリが失敗した: sqlxのメッセージ付きで 500 Internal。
    Database(sqlx::Error),
}

　計画が開発者に戻る前には、2つのレビュアーエージェントが、意図アーティファクトから導かれた形式仕様の穴を探します。仕様が依頼内容と一致しているか、証明で示せる以上のことを約束していないかを確かめるためです。この仕様の改善はバックグラウンドで進み、ユーザーからのフィードバックも受け付けながら、レビュアーが健全だと合意するまで繰り返されます。

Step 6〜7: 証明・検査・ギャップの解消と、PR・CIへの統合

　Step 6: 証明し、検査し、ギャップを埋める。 開発者のレビューは仕様の承認で終わり、その後の実装と証明は機械が検査します。承認後、「Build plan」段階で計画が「pdd-prove」に渡され、小さなタスクグラフに変換されます。ログインの場合は7つのタスクで、login.rsをバックエンドのクレート内でVerusでビルドできるようにすること、判断・トークン・フロー全体の証明、信頼済みラッパーとE2Eのログインのテスト作成が含まれます。最初のタスクは契約の意味を変えずにビルドを通すことで、契約を弱めるくらいなら作業を止めて質問するよう設計されています。

　各タスクは同じループを回します。

コーディングエージェントが実装と証明を書き、Verusが導出された形式仕様に照らして検査する
信頼境界にあるものには、計画で定めたテストを書く
LLMの検証役が計画・仕様・結果を並べて読み、証明も合格したチェックもない要件という「ギャップ」を探す。ギャップがなくなるまでコーディングエージェントに差し戻し、仕様自体に矛盾などのギャップがあれば、開発者に判断を求める

　原文は、証明は仕様以上に良くはならないと強調しています。モデルが自分で仕様を書いたり、証明を出すよう調整されていたりすると、検証は通るもののほとんど何も制約しない弱い条項に落ち着きがちです。原文はこれを「バイブ検証（vibe verification）」と呼んでいます。対策がミューテーションチェックで、pdd-proveはコードの作業用コピーにensures条項1つにつき1つのバグ（全員を拒否する、メールアドレスより先にユーザー名を確認する、など）を仕込み、Verusが狙った条項でそれを却下できるかを確かめます。却下されない変異体があれば、その条項は何も制約していないとみなされ、ギャップとして差し戻されます。

　また、このループは「ゴールを動かさない」ことに厳格です。固定したバージョンのVerusで非同期の構文を表現できない場合も、非同期でない補助関数に切り替えたり契約を弱めたりせず、作業を止めてチームに尋ねます。

　Step 7: 意図と検証済みコードを並べてレビューする。 タスクがすべて通ると、pdd-proveがプルリクエストを作成します。login_flowとその部品、証明、テスト付きの信頼済みラッパーを含むverified/クレートが追加され、本番のログインハンドラーは既存のHTTPステータスコードを保ったままlogin_flowを経由するようになります。コピーではなく、本番のログイン経路そのものが強化される形です。

　開発者は生成コードを1行ずつレビューすることなくマージできました。レビューは意図アーティファクトの上でずっと行われており、プルリクエストは「受領書」として機能します。その説明欄では、各要件が形式検証済みか経験的に確認済みかが示されます。

　マージ後は「pdd-ship」ワークフローがCIにVerusの検査を追加し、人でもエージェントでも、以後のログインへの変更は同じ仕様に対して証明を通し続ける必要があります。証明が壊れればテストの失敗と同じくビルドが失敗します。さらに、証明がすべての入力をカバーするため、パスワード関門の例示的なテストのように証明済みの内容を再確認するだけのテストは削除し、信頼境界を守るテストは残します。CIが強くなると同時に軽くなる、と原文は説明しています。

証明が言えること・言えないこと、そしてRustを選ぶ理由

　原文は「完全に検証済み」という言葉は誇張されやすいとして、主張の範囲を次のように明示しています。

証明済み: login_flow、login_core、lookup_target、decide_login、issue_tokenの本体は、あらゆる入力で契約を満たす。正しいテーブルを選び、指定アカウントの保存ハッシュとパスワードを照合し、そのアカウントのIDとテーブルに応じた役割でトークンを発行し、それ以外はトークンなしで現在の400・401・500を返す
信頼済み・テスト済み: 2つのデータベース検索、bcryptを使うcheck_password、時計、トークン署名、データベースのエラーメッセージ、ハンドラーのリクエスト展開は証明の外にあり、開発者が承認した仮定の契約の背後に置かれる。実際のbcrypt、SQLiteのスキーマ、ルーターに対するテストで確認する
仮定: Verus、Rustコンパイラ、Z3（SMTソルバー）からなるツールチェーンと、Verusの標準ライブラリvstd

　PDD Kitが現在検証できるのは、Verusが対象とするRustだけです。既存のコードがRustなら移行は不要で、他の言語のコードはRustに移植して同じ仕様で検査するか、非Rustのプロジェクトからバインディング経由で検証済みのRustを呼び出す方法が示されています。FAQでは、Verusを選んだ理由として、Rustのコードを直接検証でき、既存のRust開発ワークフローに組み込みやすい点を挙げています。Lean、F*、Rocqなど他の証明言語にもそれぞれのトレードオフがあり、PDD Kitの手法はそれらにも応用できる可能性があるとしています。

　原文はRustを使う利点として、あまり目立たない点も挙げています。1行ずつのレビューへの依存が減れば、読みやすさは言語選択の主な理由ではなくなり、速度や安全性で言語を選び、思い切って最適化できるようになります。仕様を壊す変更は証明の失敗として検出されるためです。

PDD Kitに期待できること・現時点の限界

　PDD Kitは研究用のプロトタイプです。原文は、証明には依然として相応の労力がかかり、その多くは証明そのものの作成に費やされると認めています。明確な仕様が労力を抑える鍵であり、PDD Kitの多くの部分が意図を正しく定めることに充てられているのはそのためだと説明しています。始めるなら、ログイン、決済、権限管理など、バグのコストが最も大きい部分からで、残りは1つずつ検証していくことを勧めています。

　弱点についても率直に述べられています。保証の強さは6つの信頼済み部品に依存し、特にcheck_password（パスワードに関するすべての約束）と2つの検索処理（トークンがどのアカウントを指すかに関するすべての約束）の比重が大きいとしています。これらはテストで支えられていますが、証明はされていません。Microsoft Researchは、この信頼境界は今後大きく縮小し、形式検証できるコードの割合が増えると見込んでおり、どこまで拡張できるかを確かめたいとしています。

　本稿としては、この研究の意義は形式手法の普及そのものよりも、「人が何をレビューするのか」を問い直した点にあると受け止めています。エージェントが大量のコードを書く時代に、人の役割を「意図を言葉で確かめ、信頼する範囲に署名すること」へ寄せていく方向性は、Rustを使わない現場にとっても考える手がかりになると思います。一方で、仕様の誤りや書かれなかった要件は証明では防げないという原文の注意書きは、導入を検討する際にも重く受け止めるべき点だと考えられます。

まとめ

　Microsoft ResearchのPDD Kitは、開発者の意図を形式仕様にし、エージェントのコードをVerusの証明とテストで縛る試みです。何を証明し何を信頼したかを明示する設計が特徴で、信頼境界をどこまで縮められるかが今後の焦点です。エージェントの大きな変更をどうレビューするかについては、スタックPRの活用術を紹介した記事もあわせてご覧ください。