GitHub Next と Microsoft Research が、エージェントが書いたコードを、行ごとに全部読まずに信頼するための研究プロトタイプ「PDD Kit」を公開しました（2026年11月）。PDD は Proof-Driven Development（証明駆動開発）の略で、「専門家だけのものだった形式手法を、日常のソフトウェアに持ち込む」試みです。本記事は、公開ページの内容をもとに、その考え方と仕組みを整理します（動く実機の検証ではなく、公開情報の整理です）。
この話題の土台には、Vibe Codingとは？AIコーディングの始め方・ツール比較・実践ワークフロー2026 で扱った「AIにコードを書かせる開発」の広がりがあります。書く速さが上がったぶん、本番環境でVibe Coding｜Anthropic研究者が語る2.2万行PR成功の実践戦略 のように「出てきたコードをどう信頼するか」が次の課題になりました。PDD Kit は、その「信頼」を正面から扱います。
WHERE HUMAN TIME GOES人のレビューが向かう先
行ごとに全部読むから、意図を平易な言葉で読むへ
いまのエージェント開発
- 計画はエージェントを拘束しない
- 実装は短時間（エージェントが大量に書く）
- レビューは長時間：全行を人が読む
- エージェント製のテストを信じるしかない
PDD Kit を使う場合
- 計画は長め：意図レビューをチームが承認
- 実装は証明つき（Verus がチェック）
- マージは短時間：レシート（受領書）を読む
- 証明は全入力、残りはテストで裏づけ
30秒でわかる
- ・何の試みか：エージェントのコードを行ごとに全部読む代わりに、意図を平易な言葉でレビューし、コードが意図に合うことは機械（形式証明）に確かめさせる
- ・誰の：GitHub Next × Microsoft Research の研究プロトタイプ（2026年11月公開、Rust の証明言語 Verus を使用）
- ・肝：証明はエージェントが書き Verus が検証。人が読むのは仕様（意図）であって証明ではない
- ・正直な所：全部は証明できない。証明できない部分はテストで裏づけ、何を信頼しているかを明記する
なぜ「エージェントのコードのレビュー」が問題になるのか
PDD Kit が挙げる、エージェント製コードをマージする側の悩みは4つです。
| 問題 | 何が起きるか |
|---|---|
| 計画は拘束力を持たない | どれだけ良い計画でも、エージェントは必ずしも従わない。例外ケースを無視しても警告は出ず、壊れて初めて気づく |
| テストが何を保証するか曖昧 | エージェント製のテストは「意図したコード」ではなく「エージェントが書いたコード」に通りがち。カバレッジは良く見えても要求とのズレが隠れる |
| 行ごとのレビューは拡張しない | 一度に数万〜数十万行が出ると、レビューはざっと見て承認するだけになり、見落としを祈ることになる |
| 雰囲気の検証（vibe verification） | モデルに形式手法で正しさを証明させても、弱い不変条件（検証はするがほとんど何も排除しない仕様）を選びがち。間違った仕様の緑チェックは、無いより悪い |
4つ目は示唆的です。「AIが書いたコードをAIに証明させる」だけでは、vibe verification——もっともらしい緑チェックだが中身の薄い証明——に陥る、と PDD Kit は指摘します。保証のように見えてしまうぶん、かえって危ないという立場です。
なぜ「証明」なのか、そしてなぜ今なのか
形式手法は、例ではなく数学でソフトウェアを検証します。仕様（コードが何をすべきかの正確な記述）を作り、検証ツールが考えられるすべての入力に対してコードが仕様を満たすことを証明します。テストが「試した入力で正しかった」という証拠なのに対し、証明は「全入力で成り立つ」という保証です。
TESTS vs PROOFなぜ証明か
テストは一部の入力／証明は全入力
テスト（証拠）
- 試した入力でだけ正しさを示す
- 膨大な入力のごく一部をサンプリング
- 選ばれなかった入力のバグは見逃す
- PDD では「証拠」であって証明ではない
形式証明（保証）
- 考えられる全入力で仕様を満たすと示す
- 指定したプロパティは必ず成り立つ
- 弱い仕様は変異チェックで弾く（空証明対策）
- 証明できない所はテストで裏づけ・明記
かつて証明は、専門家・馴染みのない言語・コードより大きな証明・長い開発期間を要し、日常開発にはコストが高すぎました。PDD Kit は、ここが2つの点で変わったと述べます。ひとつは、コーディングエージェントの進歩で、明確な仕様から形式的な証明を生成するのが現実的になったこと。もうひとつは、エージェントが仕様づくり自体を助けられるようになったこと。残る難題は「自分の意図が、チームメイトやエージェントと一致しているか」という人間側の問題だ、という整理です。
PDD Kit の仕組み——人は意図を、機械はコードを
位置づけとして、PDD Kit は「形式手法に対して、Spec Kit が Spec-Driven Development に対して持つのと同じ役割」を狙う、とされています。GitHub Next の計画ツール「Chopin」の中で計画パートナーとして動き、コードを読み、注意深いレビュアーが尋ねるような質問を投げ、答えを意図アーティファクト（意図と形式仕様を橋渡しする文書）に記録します。流れはこうです。
THE PDD LOOP意図から、証明つきマージまで
人は意図を、機械はコードをチェックする
-
意図を平易な言葉で
「管理者アカウントだけが管理者トークンを得る」のように要件を書く。pdd-plan が決定カードで曖昧さを問い、意図アーティファクトに記録
-
形式仕様（Verus）＋承認
形式化できる部分を Verus の仕様にする。各節に平易な英語コメント付き。2人のレビュアーが仕様を承認（コードではなく仕様を読む）
-
pdd-prove（機械が証明）
エージェントが実装と証明を書き、Verus が全ステップを検証。信頼する部分はテストで裏づけ。LLM 検証がギャップを探す
-
PR＝レシート
何を証明し、何を信頼し、限界は何かを列挙。開発者は承認済みの意図と照合してマージ。CI で Verus チェックが継続
- 意図を平易な言葉で書く：PDD Kit は決定を求める前に、関連するコードを説明する決定カードを返す。たとえば「正しいパスワードのときだけトークンを出す」が、「正しいパスワードなら常にトークンを出す」のか「間違いは拒否する」だけなのか——という2つの別仕様の食い違いを、カードが先に問う。
- 形式仕様にして承認：形式化できる部分は Verus（Rust の証明言語）の仕様になる。各節には平易な英語コメントが付き、2人のレビュアーが「コードではなく仕様」をレビューする。
- 証明する（pdd-prove）：コーディングエージェントが実装と証明を書き、Verus が全ステップを検証する。弱い仕様を弾くため、節ごとに1つバグを仕込む変異チェックを行い、通ってしまう節（＝何も制約していない空の仕様）はギャップとして差し戻す。
- PR＝レシート：何が証明され、何が信頼され、何が約束されていないかを列挙する。開発者は生成コードを行ごとに読む代わりに、承認済みの意図とレシートを照合してマージする。
要点は、人が読むのは証明ではなく仕様だということです。証明はエージェントが書き、Verus が受理すれば誰が読んだかに関わらず有効になります。
何が証明され、何を「信頼」するか
PDD Kit は「全部は証明できない」ことを前提に置きます。証明の外側にあるもの——外部ライブラリ（bcrypt・SQLite・JWT 署名など）、データベースが今どんな値を持つか、処理が完了するか・速いか、画面やエラーメッセージの分かりやすさ——は、信頼できる境界（TCB）として切り出します。各要素を小さなラッパーで包み、想定する契約を書き、ひとつずつ承認させ、その契約をテストで裏づけます。
| 区分 | 扱い | 確かめ方 |
|---|---|---|
| 証明される部分 | 指定したプロパティ（例：正しいパスワードのときだけ、そのアカウントのトークンが出る） | Verus が全入力で証明 |
| 信頼する部分（TCB） | 外部ライブラリ・DB の中身・時計など、証明の外 | 想定契約を明記し、テストで裏づけ（証拠） |
| 約束しないこと | 処理が必ず終わる・速い、他エンドポイントの振る舞いなど | 計画に「約束しない」と明記 |
信頼する部分のテストは、仕様が返る前に「Given/When/Then」のシナリオとして計画に書かれ、実行されるまでは「予定」として記され、実行後にコマンドと対象コミットが記録されます。テストに通ることは証拠であって証明ではないので、PDD Kit はそう明示的にラベル付けする、という扱いです。そしてマージ後は、Verus のチェックが CI にテストと並んで入り、以降エージェントや人が加える変更も同じ仕様に対して証明され続けます。証明が壊れればテスト失敗と同じようにビルドが落ちます。証明が全入力を覆うぶん、すでに証明済みのものを再確認するだけの例ベースのテストは削られ、信頼境界を守るテストだけが残るので、CI はむしろ小さく強くなる、とされています。
公開ページの例では、Rust のフルスタックWebアプリ「Pet Store」（約5,000行）のログインを検証しています。「正しいパスワードのときだけトークン」「管理者だけが管理者トークン」という2文の要求が、最終的に8つの条項（ensures）になりました。途中で「正しいパスワードに必ずトークンが要るか？」という決定カードが出て、「拒否だけを証明すると、全員を拒否するログインでも仕様を満たしてしまう」という抜けを先に塞いだ、という具体例が示されています。テストでは滅多に捕まらない「パスワード照合と署名が別アカウントを指す配線ミス」も、同じアカウントを指すことを条項で縛って検出できる、としています。
限界と、これが変えようとしていること
PDD Kit は研究プロトタイプで、現時点の検証対象はRust のみ（Verus が Rust 用のため）。他言語は Rust に移植して検証するか、バインディング経由で検証済み Rust を呼ぶ形になります。証明づくりには依然として相応の労力がかかり、だからこそバグのコストが最も高い所（ログイン・支払い・権限）から始め、残りを1つずつ広げる方針です。保証の強さは「信頼する部分」の強さに依存し、公開ページも最も弱い部分（パスワード照合やDB参照の2つのルックアップ）を率直に挙げています。
要するに：PDD Kit が変えようとしているのは「人が何をレビューするか」です。エージェント製コードを行ごとに読むのをやめ、チームは意味（意図）を平易な言葉でレビューし、コードがそれに合うことは証明が確かめる。計画は本来「契約」であるべきで、今後はエージェントが実際にそれを守らねばならない——という主張です。
AIにコードを書かせる流れ自体は、本番環境でのVibe Coding でも、コスト面の TokenEconomizer（MS製） でも広がっています。PDD Kit はその中で「速く大量に書けるようになった世界で、何を根拠にマージするか」という問いに、形式手法で答えようとする試みだと言えます。研究プロトタイプである点、Rust 限定である点、証明の労力が残る点は割り引いて見つつ、「レビューの対象を行から意図へ移す」という発想は、エージェント開発の次の論点になりそうです。
参照ソース
- PDD Kit — Build trust in code your agents wrote（GitHub Next）（2026年11月時点。Proof-Driven Development の研究プロトタイプ。本記事はこの公開ページの内容に基づく）
- Verus — Rust 向けの検証ツール（GitHub）（PDD Kit が利用する Rust 用の証明言語・検証ツール）
