メインコンテンツにスキップ

エージェントが書いたコードを証明で縛る──Microsoft Research「PDD Kit」の仕組み

AIエージェントと開発
概要 PDD Kit は、コーディングエージェントが書いたコードを人が1行ずつ読む代わりに、人は「意図（仕様）」だけをレビューし、コードがその仕様を満たすことを形式検証ツール Verus に数学的に証明させる開発ツールキットである。Mi…
作者

obelos

公開

2026年11月8日

更新日

2026年11月8日

概要

PDD Kit は、コーディングエージェントが書いたコードを人が1行ずつ読む代わりに、人は「意図（仕様）」だけをレビューし、コードがその仕様を満たすことを形式検証ツール Verus に数学的に証明させる開発ツールキットである。Microsoft Research が2026年11月5日に研究プロトタイプとして公開した。

  • 問題：AI エージェントが書くコードは量が多すぎて、人が1行ずつレビューできない。テストもエージェント自身が書くため、要求とのずれを見逃す
  • 解決：人は「何を満たすべきか（仕様）」だけを確認し、コードがそれを満たすことは数学的な証明で保証させる。証明が届かない外部ライブラリ・データベース・時計などは「信頼する境界」として明示し、テストで補う
  • 結果：Rust 製 Web アプリ Pet Store（約5,000行）のログイン処理に適用し、2文の要求を8つの事後条件に展開して証明した。開発者は生成コードを読まずにマージした

この開発手法を Microsoft Research は Proof-Driven Development（PDD）と呼ぶ。Spec-Driven Development を支える GitHub の Spec Kit に対し、PDD を支えるのが PDD Kit という位置づけである。

人と機械の分担

PDD Kit で人がやること、機械がやること

人　機械

1. 要求を書く

ログイン処理の要件を2文だけ

↓

2. 曖昧な点を質問する

コードを書く前に確認

↓

3. 答えて、仕様を承認する

人のレビューはここで終わり

↓

4. コードと証明を書く

コーディングエージェント

↓

5. Verus が証明を検査する

全入力で仕様どおりか

↓

6. マージする

生成コードは読まない

仕様の曖昧さの例

開発者の要求は「正しいパスワードでのみトークンを出す」だった。この文は、誰にもトークンを出さないログインでも満たせてしまう。誤ったパスワードでトークンが出ることはないからである。

意図どおりにするには「正しいパスワードなら必ずトークンを出す」という逆向きの条件も必要になる。PDD Kit はこの種の曖昧さをコードを書く前に質問として示し、人に決めさせる。人が決めた仕様に対して、機械が証明を組み立てる。

用語

用語 意味
形式検証 コードが仕様を満たすことを、数学的な証明で確かめること。テストと違い、すべての入力について成り立つ
仕様（事前条件・事後条件） 関数が満たすべき約束。事前条件は呼び出す側が守る条件、事後条件は関数の結果について常に成り立つ条件
Verus Rust のコードに仕様と証明を書き、自動で検査するツール。Microsoft Research などが開発
信頼境界 証明できず「正しく動く」と仮定する部分。外部ライブラリ、データベース、時計など。テストで確認する
ミューテーション検査 わざとバグを仕込み、仕様がそれを検出できるか確かめること。何も縛っていない仕様を見つける

記事の構成

節 内容
背景 コードレビューとテストだけでは足りない理由
基礎：形式検証と Verus 証明の仕組みと、証明できない部分の扱い方
PDD Kit のワークフロー 計画・証明・CI 組込みの3段階
事例：Pet Store 2文の要求が8つの条件になるまでの実例
仕様の品質 仕様自体の誤りを防ぐ方法
何が証明され、何が信頼されているか 保証の範囲と限界
他の手法との違い・まとめ テスト駆動開発などとの比較と結論

概要だけをつかむなら「背景」と「まとめ」で足りる。仕組みまで理解するなら「事例」までを読むとよい。

背景：エージェント生成コードのレビューは行単位では成立しない

エージェント開発の基本用語

  • コーディングエージェント：自然言語の指示を受け、複数ファイルにまたがるコード変更を自律的に作る AI。Claude Code や GitHub Copilot のエージェント機能が該当する。成果物はプルリクエスト（PR）として提出され、人がレビューしてから本体のコードに取り込む（マージ）
  • CI（継続的インテグレーション）：コードを push するたびにビルドとテストを自動で実行する仕組み。テストが失敗した PR はマージできないように設定できる
  • カバレッジ：テストで実行されたコード行の割合。高くても「要求どおりに動くか」は示さない。実行された行が正しい結果を返したかは、テストの書き方次第だからである
  • Spec-Driven Development（SDD）：実装の前に自然言語で仕様書・計画・タスク一覧を作り、それをエージェントに渡して実装させる手法。GitHub が公開している Spec Kit が代表的なツールである。仕様書は文書にすぎず、コードが仕様どおりかを機械的に確かめる仕組みは持たない

行単位のレビューが破綻する理由

コーディングエージェントは1回のセッションで数万〜数十万行の機能を出力する。この規模の PR を人が全行読むことは現実的ではない。そのため多くのチームは、レビューの重心を計画（自然言語の仕様）とテストに移している。

しかし計画書はエージェントを拘束しない。エージェントは計画から少しずれた実装を書き、その実装が通るテストを自分で書く。テストは「頼まれたもの」ではなく「作ったもの」を検査するため、CI はテストの量だけが増え、カバレッジは健全に見え、要求との乖離はバグ報告が来るまで表に出ない。

エージェント生成コードの典型的な失敗は2種類ある。必要なものが抜けていることと、明らかに誤ったことをしていることである。テストは入力空間のごく一部しか実行しないため、どちらも取りこぼす。この穴を埋める手段として PDD Kit が採るのが、全入力について性質を保証する数学的証明である。

形式検証が従来日常のソフトウェアに使われなかった理由は、専門家・専用言語・コード本体の数倍の証明量・数年単位の工数が必要だったことにある。この前提を変えたのは次の2点である。

  1. コーディングエージェントが、明確な仕様から形式的な証明を生成できるようになった
  2. エージェントが、形式仕様そのものを書く作業も支援できるようになった

基礎：形式検証と Verus

テストと証明の違い

テストと証明の違いを、2つの数の大きい方を返す関数で示す。Verus では次のように書く。

fn max(a: u64, b: u64) -> (r: u64)
    ensures
        r >= a,
        r >= b,
        r == a || r == b,
{
    if a >= b { a } else { b }
}

ensures の下の3行が仕様で、「戻り値 r は a 以上」「b 以上」「a か b のどちらか」を意味する。テストは max(3, 5) のような組み合わせを数個試すだけだが、Verus は u64 同士のすべての組み合わせ（約3.4×10³⁸通り）でこの3行が成り立つことを証明する。

3行目を書き忘れると、常に u64::MAX を返す誤った実装も前の2行を満たしてしまい、証明が通る。仕様が弱いと、証明は誤りを見逃す。後の節で出てくる「ミューテーション検査」は、この種の書き忘れを見つける仕組みである。

SMT ソルバー・論理記号・Rust の用語

  • SMT ソルバー：論理式がどんな値でも成り立つかを自動で判定するプログラム。Verus はコードと仕様から「この条件は常に真か」という式（検証条件）を作り、SMT ソルバーの Z3 に解かせる。成り立たない値（反例）が存在しないと判定されれば、全入力で証明できたことになる
  • 含意と同値：「A ⇒ B」（A ならば B）は、B が成り立てば A は必ず成り立つという意味ではない。両方向「A ⇒ B かつ B ⇒ A」が揃ったものを同値（A ⇔ B）と呼ぶ。事例の節では、この区別によって仕様の欠陥が見つかる
  • Rust の用語：crate は Rust のライブラリやプログラムの単位。async fn は非同期関数で、呼び出すとすぐに結果ではなく Future（後で完了する処理）を返し、.await で完了を待って結果を受け取る

形式検証と経験的検証

PDD Kit はすべての検証結果に、どちらの種類に基づくかのラベルを付ける。

種類 方法 保証の範囲
形式検証 検証器が、コードが仕様を満たすことの証明を機械的に確認する 仕様に書いた性質について、すべての入力で成立
経験的検証 単体テスト、E2E テスト、ブラウザエージェント、コンピュータ操作エージェントで実際に動かす 試した入力でのみ成立。PDD Kit は「証明」ではなく「証拠」と表示する

Verus

Verus は Rust プログラムを検証する SMT ベースのツールで、Microsoft Research、CMU、ETH Zurich など11機関の共同開発である。仕様と証明を Rust の構文で書き、SMT ソルバー Z3 が検証条件を解く。論文は OOPSLA 2023 で発表されている（Verus: Verifying Rust Programs using Linear Ghost Types）。

Verus のコードは3つのモードに分かれる。

  • spec：仕様を書くための数学的な定義。実行されない
  • proof：証明の補題。実行されない
  • exec：通常の実行コード。コンパイルされて動く

spec と proof はゴーストコードと呼ばれ、検証器は検査するがコンパイラは最終バイナリから消去する。ゴーストコードでは int や nat といった上限のない数学的整数を使えるため、仕様を実行時の型制約から切り離して記述できる。

事前条件・事後条件

関数の契約は requires（呼び出し側が満たすべき条件）と ensures（戻り値 r について常に成り立つ条件）で書く。cargo build 相当の検証時に、いずれかの ensures 条項がたった1つの入力でも破れる可能性があれば、Verus はその条項を指してビルドを失敗させる。証明は LLM が書くが、合否を決めるのは決定的な Verus の実行であり、モデルは判定に関与しない。検査時間は小さいモジュールで数秒、大きなコードベースで数分である。

信頼境界（TCB）

証明が「こう振る舞う」と仮定しているコードの集合を Trusted Computing Base（TCB）と呼ぶ。外部 crate（bcrypt、sqlx、jsonwebtoken）、DB の中身、時計は証明の外にある。Verus ではこれらを次の2つの仕組みで契約だけ与えて扱う。

  • #[verifier::external_body]：本体を Verus が読まず、ensures だけを信じるラッパー関数
  • #[verifier::external_fn_specification]：既存の関数のコードは元の場所に置いたまま、外から契約を付ける

さらに、DB の行や bcrypt の判定結果のように実体を持ち込めない概念は、本体を持たない未解釈関数（uninterp spec fn）として仕様上に名前だけ置く。証明は「DB が何を保持していても、ログインはそれに対して正しく振る舞う」ことを示し、信頼された契約が「検索は DB が保持する行を返す」ことを担う。

PDD Kit のワークフロー

PDD Kit は GitHub Next の Chopin 上で動く。Chopin はチームとエージェントが1つの共有ドキュメントでリアルタイムに計画を作る、マルチプレイヤーの計画環境である。ワークフローは「人が意図を確定する前半」と「機械がコードを意図に縛る後半」に分かれ、3つの段階で構成される。

  1. pdd-plan（意図の確定）：コードを読み、実装前に判断が必要な点を Decisions タブに質問カードとして出す。回答は intent artifact（意図と形式仕様を橋渡しする文書）に記録され、形式化できる部分は Verus 仕様に、形式化できない部分はテスト用の非形式仕様になる。最後に開発者が計画全体を承認する
  2. pdd-prove（証明と検査）：承認済みの仕様を小さなタスクグラフに分解し、タスクごとに「実装と証明を書く → Verus が検査 → 信頼境界のテストを書く → LLM 検証器が証明もテストもない要件を探して差し戻す」を繰り返す。完了すると PR を開く
  3. pdd-ship（CI への組込み）：Verus 検査を CI に追加する。以後、人やエージェントによるログイン処理の変更はすべて同じ仕様に対して再証明され、証明が壊れればテスト失敗と同様にビルドが落ちる

pdd-prove はゴールを動かさない。たとえば非同期の構文が固定バージョンの Verus で表現できない場合、同期ヘルパーへの置き換えや契約の弱体化で逃げず、タスクを止めてチームに判断を求める。仕様自体に矛盾（2つの要件が両立しないなど）が見つかった場合も、開発者への決定事項として差し戻される。

事例：Pet Store のログイン処理を証明する

ログイン処理の仕組み

ログイン処理は次の流れで動く。

  1. 利用者がメールアドレス（または管理者ユーザー名）とパスワードを送る
  2. サーバーがデータベースからアカウントを探す。パスワードそのものは保存せず、bcrypt という方式で変換したハッシュ値だけを保存している
  3. 送られたパスワードを bcrypt でハッシュと照合する
  4. 一致すれば JWT（JSON Web Token）を発行する。JWT は「誰か（sub：ユーザーID）」「権限（role：customer か admin）」「有効期限」を書き、サーバーの秘密鍵で署名した文字列である。以後のリクエストは JWT を添えて送り、サーバーは署名を確かめて本人と権限を判定する

ログイン失敗時は HTTP ステータスコードで理由を返す。

コード 意味 このアプリでの使い方
400 Bad Request リクエストの形式が不正 メールもユーザー名もない
401 Unauthorized 認証に失敗 アカウントがない、パスワードが違う
500 Internal Server Error サーバー側の障害 データベースエラー、ハッシュが読めない

使用技術

使っている技術は次のとおり。

名前 役割
Axum Rust の Web サーバー用フレームワーク
SQLite ファイル1つで動くデータベース
sqlx Rust からデータベースに問い合わせるライブラリ
bcrypt パスワードのハッシュ化と照合
jsonwebtoken JWT の発行と署名
Leptos / WebAssembly Rust で画面を作り、ブラウザで動く形式に変換する仕組み

対象アプリと要求

対象は全編 Rust の Web アプリ Pet Store である。バックエンドは Axum と SQLite で在庫・プロモーション・注文・決済を扱い、フロントは Leptos を WebAssembly にコンパイルしている。合計約5,000行。PDD Kit は「バグの損失が大きい箇所から段階的に検証する」ことを推奨しており、トークンの誤発行がアカウントの乗っ取りにつながるログインが最初の対象になった。

開発者が Chopin に書いた要求は次の2文だけである。

  1. 正しいパスワードでのみトークンを得られる
  2. 管理者アカウントだけが管理者トークンを得る

Step 1：コードを書く前に曖昧さを潰す

pdd-plan が最初に出した質問は「正しいパスワードなら必ずトークンが出るべきか」である。要求1は「トークン ⇒ 正しいパスワード」という含意であり、全員を拒否するログインもこれを満たす。逆向きの「正しいパスワード ⇒ トークン」を加えると「同値」になる。エージェントに任せるとどちらかを黙って選ぶ箇所であり、開発者は両方向を選択した。

Step 2：意図マップ

計画の先頭には、ログインのフローチャート、証明する部分と信頼する部分の一覧（spec landscape）、要件ごとの意図マップが常に最新の状態で置かれる。意図マップの各項目は開発者の元の文言に紐づき、対応する形式仕様の節とテストへリンクする。

Step 3：証明範囲を広げる判断

PDD Kit の初期案は、ログインの判定ロジック（参照テーブルの選択とパスワードによる関門）だけを証明し、それを包むハンドラは信頼してテストする構成だった。開発者は、DB 検索の await とトークン署名をつなぐハンドラ部分こそリファクタリングで2行入れ替わる危険があると判断し、ハンドラにも非同期の仕様を与えることを選んだ。これにより新しい非同期関数 login_flow が、リクエストのフィールドからトークンまたは HTTP エラーまでの契約を一貫して担う。範囲を広げると信頼するラッパーも増えるため、PDD Kit は改訂版の計画を再承認に回した。

Step 4：証明が届かない部分を信頼境界として明示する

開発者は次の6つを信頼部品として個別に承認した。それぞれ契約付きのラッパーで包まれ、契約の各条項にテストが計画される。

信頼部品 仮定している契約
Customer::find_by_email / Admin::find_by_username 成功時、そのテーブルが保持する該当行をそのまま返すか、なければ None
check_password bcrypt::verify の薄いラッパー。読めないハッシュでのみエラー、Ok(true) は正しいパスワードのときだけ
generate_token 渡されたクレームをそのまま設定済みの秘密鍵で署名。失敗は 500
expiry_from_now 時計を読み、ちょうど24時間後（86,400秒）を有効期限にする
database_error 検索失敗を sqlx のメッセージ付き 500 に変換
ログインハンドラの外殻 リクエストを展開し、値を変えずに login_flow へ渡す

計画には「誰も約束しないこと」も明記される。ログインの Future が完了すること、範囲外の時刻で panic しないこと、試行のタイミングや回数、他のエンドポイントがロールをどう読むか、である。

Step 5：2文の要求が8つの事後条件になる

2文の要求と「両方向」の決定は、login_flow の8つの ensures 条項に展開された。要旨は次のとおりである。

  1. メールもユーザー名もなければ 400
  2. トークンが返るのは、リクエストが指すアカウントが存在し、そのハッシュとパスワードが一致し、トークンの subject とロールがそのアカウントのものである場合だけ
  3. 指すアカウントに正しいパスワードなら、必ずトークンが返る（検索・署名の失敗による 500 を除く）
  4. 存在しないアカウントは 401（検索失敗の 500 を除く）
  5. 読めるハッシュに対する誤ったパスワードは 401
  6. 読めないハッシュは 500 で、トークンは出ない
  7. 管理者ロールは、メールなしでユーザー名により admins テーブルから見つかった場合だけ
  8. メールでのログインのトークンは常に customer ロール

条項2では、パスワード照合とトークンの両方に同じアカウント変数が現れる。これにより「ボブが自分の正しいパスワードでログインし、アリスのトークンを受け取る」という配線バグが証明段階で排除される。各ステップは単独では正しく見えるため、テストスイートが想定しにくい種類のバグである。4〜6は既存の拒否時の挙動をそのまま保つ条項で、既存のストアフロントと API テストは変更なしで動き続ける。

login_flow は小さな証明済み関数の合成である。lookup_target が参照テーブルを選び、login_core が検索を await して decide_login（パスワードの関門）を呼び、issue_token が署名または HTTP エラーへの変換を行う。Verus は login_flow を各部品の契約だけを使って証明し、本体を読み直さない。decide_login の本体を変更した場合、再証明されるのは decide_login だけである。

async 関数の契約の意味

login_flow は DB 検索を await する非同期関数である。Verus では、requires は呼び出しで Future を生成した時点で検査され、ensures は await して得た値について成り立つ。Future が完了することは何も約束しないため、検索がハングしても条項は破れない。PDD Kit はこの点を doc コメントに明記している。

Step 6〜7：証明、PR、CI

承認後、pdd-prove はログインを7タスクに分解した。login.rs をバックエンド crate 内で Verus 下でビルドできる状態にし、判定・トークン・フロー全体を証明し、信頼ラッパーと E2E ログインのテストを書く。完了すると PR が開かれ、実際のログインハンドラは login_flow を経由するよう置き換わる。証明はコピーではなく本番のログイン経路を補強する。PR の説明は各要件を「形式検証済み」か「経験的に確認済み」のどちらかでマークした受領証になっている。

pdd-ship はさらに、証明済みの性質を再確認するだけのテスト（パスワード関門の例示的なテストなど）を削除し、信頼境界を守るテストだけを残す。CI は強くなると同時に軽くなる。検証の過程で Verus は既存のバグも検出した。

仕様の品質をどう担保するか

不変条件とミュータント

  • 不変条件：処理の前後で常に成り立つべき性質。仕様の各条項はこの一種である
  • ミュータント：元のコードに意図的に小さなバグを1つ入れた変種。仕様がミュータントを検出できなければ、その仕様は対応するバグを防げていない

3重の検査

証明はコードが仕様を満たすことしか示さない。仕様が誤っていれば、誤ったコードが「検証済み」になる。PDD Kit が工程の大半を意図の確定に割くのはこのためであり、仕様側に3重の検査を置いている。

  • 人による承認：開発者が読むのは証明ではなく、intent artifact と仕様である。各関数の ensures は「〇〇なら△△」という if-then の条項の並びで、条項ごとに平易な英語のコメントが付き、数分で読み方を習得できる粒度になっている
  • レビュアーエージェント2体：計画が開発者に戻る前に、2体のエージェントが intent artifact から導いた形式仕様の穴を突く。仕様が要求と一致しているか、証明で示せる以上のことを約束していないかを、ユーザーのフィードバックを受けながら合意まで反復する
  • ミューテーション検査：pdd-prove は作業用のコピーに ensures 条項1つにつき1つのバグ（全員を拒否する、メールより先にユーザー名を確認する、など）を仕込み、Verus がその条項で各ミュータントを拒否することを確認する。通過したミュータントがあれば、その条項は何も制約していないことになり、ギャップとして差し戻される

モデルが自分で仕様を書く場合や、証明を通すことに最適化されている場合、検証は通るがほとんど何も排除しない弱い不変条件に落ち着きやすい。Microsoft Research はこれを「vibe verification」と呼んでいる。ミューテーション検査はこの現象に対する直接の防御である。

何が証明され、何が信頼されているか

Pet Store のログインについて主張できることは、次の3層に分かれる。

ログイン処理の証明・信頼・保証外の3層

保証しない（計画に明記）

完了するか・速度・試行回数

信頼して承認＋テストで確認

DB検索2つ・bcrypt・時計・JWT署名・DBエラー変換・ハンドラ外殻

Verus が全入力で証明

login_flow / login_core
lookup_target / decide_login
issue_token

  • 証明済み：login_flow、login_core、lookup_target、decide_login、issue_token の本体が、すべての入力で契約を満たす。ログインは正しいテーブルを選び、指すアカウントの保存済みハッシュとパスワードを照合し、そのアカウントの ID とテーブルに対応するロールでトークンを発行し、それ以外は既存の 400・401・500 でトークンなしに拒否する
  • 信頼＋テスト：DB 検索2つ、bcrypt を包む check_password、時計、トークン署名、DB エラーメッセージ、ハンドラのリクエスト展開は、開発者が承認した仮定の契約の裏にあり、実際の bcrypt・SQLite スキーマ・ルーターに対するテストで確認する
  • 前提：Verus・Rust コンパイラ・Z3 のツールチェーンと、Verus 標準ライブラリ vstd

保証の強さは6つの信頼部品で決まる。特に check_password はすべてのパスワードに関する保証を、2つの DB 検索はトークンがどのアカウントを指すかに関するすべての保証を支えている。これらはテストで裏づけられているが、証明はされていない。Microsoft Research は、この信頼境界が今後大きく縮み、形式検証できるコードの割合が増えると見込んでいる。

他の手法との違い

違いは「何がコードを計画に縛るか」にある。

手法 コードを検査するもの
Spec-Driven Development（例：Spec Kit） 何も仕様を強制しない。仕様は慣習として機能する
Test-Driven Development 入力の一部に対するテスト。作ったものに合わせて書かれやすい
エージェントの自己チェック コードを書いたのと同じモデル
Proof-Driven Development（PDD Kit） 承認した仕様をコードが満たすという証明を、Verus が自動で検査する

PDD は SDD の計画ループを引き継ぎ、証明が届かない箇所ではテストを使い続ける。置き換えではなく、計画とテストの上に証明の層を足す構成である。

まとめ

PDD Kit が変えるのは「人が何をレビューするか」である。生成コードを1行ずつ読む代わりに、チームは平易な言葉で書かれた意図と、証明の外に置いた信頼境界をレビューし、コードがその意図を守ることは証明が保証する。計画は本来エージェントとの契約であり、PDD Kit はその契約をエージェントに守らせる仕組みである。

  • 現時点の対象は Rust のみ。他言語は Rust への移植か、検証済み Rust をバインディング経由で呼ぶ形になる
  • 証明の作成には今も工数がかかる。明確な仕様がその工数を抑える
  • 適用はログイン、決済、権限など、バグの損失が大きい箇所から1つずつ進める
  • 行単位レビューへの依存が下がると、言語選定の基準が可読性から速度と安全性に移る。仕様を壊す最適化は証明が拒否するため、積極的に最適化できる

参考

次に読む