2026.11.08

PDD Kitとは？AIが書いたコードを証明で確かめる【2026年11月】

IT Picks編集部

「AI エージェントが書いた何万行ものコードを、人が1行ずつ読んで確かめるのはもう無理では？」——その問いに、数学的な証明で答えようとする試みが公開されました。

2026年11月2日、GitHub の研究チーム GitHub Next が、Microsoft Research と共同で作った研究用プロトタイプ 「PDD Kit」（Proof-Driven Development Kit、証明駆動開発）を公開しました。人は「何を作りたいか」という意図をレビューし、コードがその通りかどうかは Verus という検証ツールの証明とテストで確かめる——という仕組みです。

PDD Kit

2026年11月5日には Microsoft Research もブログで詳しい解説を出しています。エージェント時代のコードレビューを「行を読む」から「意図を確かめる」に移すための実験という位置づけです。

この記事はこんな人向けです

AI エージェントにコードを書かせているが、レビューが追いつかないと感じている
話題の「証明駆動開発（PDD Kit）」が何をするものか、公式の情報で確かめたい
形式検証（数学的な証明でコードを確かめる方法）に興味がある

PDD Kitとは？一言でまとめると
なぜ必要？エージェントのコードをレビューする4つの問題
仕組み：形式検証と実地の検証の2本立て
実例：Pet Storeのログインをどう証明したか
仕様からマージまで：証明のループと「レシート」のPR
対応言語・提供状況：今使える？
公式が認める限界
IT Picksで確認したこと
IT Picks的な所感
まとめ

PDD Kitとは？一言でまとめると

AI エージェントが書いたコードが、チームの決めた仕様どおりに動くことを、すべての入力について数学的に証明するための仕組みです。証明できない部分は、何を信頼したかを明示したうえでテストで確かめます。公式ページの内容をまとめます。

項目	内容
名前	PDD Kit（Proof-Driven Development Kit）
作ったところ	GitHub Next と Microsoft Research の共同
公開	2026年11月2日（GitHub Next）、11月5日に Microsoft Research のブログ
段階	研究用プロトタイプ（Research Prototype）
証明に使うツール	Verus（Rust 用の証明言語）
対応言語	Rust のみ
動く場所	GitHub Next の計画ツール Chopin の中
実例	Rust 製の Web アプリ「Pet Store」（約5,000行）のログインを検証

公式ページは、PDD Kit を「Spec Kit が仕様駆動開発にあたるものの、形式手法版」と説明しています。形式手法とは、テストのように例を試すのではなく、数学でソフトウェアを確かめる方法のことです。

GitHub Next の PDD Kit のプロジェクトページ — 2026年11月8日時点（出典: GitHub Next「PDD Kit」）

なぜ必要？エージェントのコードをレビューする4つの問題

公式ページは、エージェントが書いたコードをマージするときの問題を4つ挙げています。

① 計画に拘束力がない

どれだけ良い計画を立てても、エージェントがその通りに作る保証はありません。ある場合の扱いを変えたり、大事な例外のケースを飛ばしたりしても、何も警告されず、壊れてから気づくことになります。

② テストは「作ったもの」を確かめている

テストを書くのもエージェント自身です。そのため、テストは「頼んだもの」ではなく「作ったもの」に合わせて通りがちです。カバレッジは良く見えても、ずれは隠れたまま——と公式は指摘しています。

③ 行ごとのレビューは追いつかない

エージェントは1回で機能をまるごと作り、数万〜数十万行にのぼることもあります。人が全部を読むのは難しく、ざっと見て承認することになりがちです。

④ 「Vibe verification」の落とし穴

では AI に「自分のコードを証明して」と頼めばよいかというと、それもうまくいきません。モデルが自分で仕様を書くと、証明は通るのにほとんど何も保証しない弱い条件になりやすい、と公式は説明します。これを Vibe verification（雰囲気の検証）と呼び、「間違った仕様に付いた緑のチェックは、チェックが無いより悪い」としています。

仕組み：形式検証と実地の検証の2本立て

PDD Kit は、GitHub Next の計画ツール Chopin の中で「計画のパートナー」として動きます。流れを図にまとめました。

PDD Kit の流れ — GitHub Next「PDD Kit」、Microsoft Research ブログ（2026年11月8日確認）をもとに IT Picks 編集部が作成

① 決定カードで「意図」を固める

PDD Kit はコードを読み、注意深いレビュー担当が聞くような質問を「決定カード」で出します。コードの仕組みが関係する質問では、先にその部分を説明してくれるので、ソースを開かずに答えられるのが特徴です。答えは意図の文書（intent artifact）に記録されます。

② 証明できる部分は Verus で証明

意図のうち形式化できる部分は Verus の仕様になり、エージェントのコードがすべての入力について仕様を満たすことを証明します。Verus は、Microsoft Research やカーネギーメロン大学などが共同で開発した Rust の証明言語です。公式は「形式手法の知識は要らない」としています。

③ 証明できない部分はテストで「証拠」に

外部の暗号ライブラリや画面のように証明が届かない部分は、単体テスト・E2E テスト、ブラウザやコンピュータを操作するエージェントなどで確かめます。ただし、テストの合格は試した入力で動いたことを示すだけなので、「証明」ではなく「証拠」と区別して表示します。

実例：Pet Storeのログインをどう証明したか

公式は、Rust で書いた Web アプリ Pet Store（バックエンドは Axum と SQLite、画面は Leptos、合わせて約5,000行）で試しています。最初に選んだのは、バグが起きると被害が大きいログインです。

① 依頼はたった2文

開発者の依頼は「正しいパスワードのときだけトークンを渡す」「管理者アカウントだけが管理者のトークンを得る」の2文でした。PDD Kit はコードを書く前に質問を返し、最初のカードでは「正しいパスワードなら必ずトークンが出る、という意味も含むか？」と聞いています。

「正しいときだけ」だけを証明すると、全員を拒否するログインでも条件を満たしてしまうためです。開発者は両方を選び、最終的に2文の依頼は8つの条件（ensures）になりました。

② 証明した部分と、信頼した部分を分ける

結果として、5つの関数を証明し、データベースの検索や bcrypt によるパスワードの確認など6つの部品は「信頼する部分」として人が1つずつ承認し、テストで確かめる形になりました。

Pet Store のログインで証明した範囲 — GitHub Next「PDD Kit」、Microsoft Research ブログ（2026年11月8日確認）をもとに IT Picks 編集部が作成

Microsoft Research のブログによると、この検証で Verus はコードを固め、既存のバグも見つけたとのことです。開発者は意図をレビューし、生成されたコードを行ごとには読まなかったと書かれています。

③ 「何を約束しないか」も書く

計画には、誰も約束していないことも明記されます。たとえばログインの処理が必ず終わるか・どれだけ速いかは、この仕様の対象外です。

仕様からマージまで：証明のループと「レシート」のPR

開発者のレビューは、仕様に承認した時点で終わりです。その後の実装と証明は機械が確かめます。

証明のループ：コーディングエージェントがコードと証明を書き、Verus が検査。LLM の検証役が「証明もテストも無い要件」を探して差し戻す
ゴールを動かさない：仕様どおりに書けないときは、条件を弱めずに作業を止めてチームに聞く
ミューテーション検査：条件1つごとにバグを1つ仕込み、Verus がそれを見つけられるか確かめる。見つけられない条件は「何も保証していない」として差し戻す
レシートになる PR：要件ごとに「証明済み」か「テストで確認」かを書き、信頼した部品とそのテストを並べる
CI に組み込む：Verus の検査を CI に入れ、後で人やエージェントがコードを変えて証明が壊れたらビルドが失敗。証明で足りるテストは削り、CI は強く・小さくなる

Microsoft Research のブログは、証明の検査は Z3 ソルバーを使う決定的な処理で、AI モデルは関わらないと説明しています。検査にかかる時間は、小さなモジュールなら数秒、大きなコードベースで数分とのことです。

AI にコードをレビューさせる仕組みは、Claude Code Review の解説でも紹介しています。

対応言語・提供状況：今使える？

PDD Kit は研究用プロトタイプで、今は Rust だけが対象です。2026年11月8日時点の公式情報をまとめます。

項目	公式の情報
段階	研究用プロトタイプ
対応言語	Rust のみ（Verus が Rust 用のため）
他の言語	Rust に移植して同じ仕様で確かめるか、バインディングで検証済みの Rust を呼ぶことはできる
動く場所	GitHub Next の計画ツール Chopin の中
料金	記載なし
導入手順・配布	GitHub Next のページにも Microsoft Research のブログにも記載なし
ライセンス	記載なし

PDD Kit が動く Chopin は、2026年9月の公開時にオープンソース化されています（リポジトリ）。ただし Chopin のページ自体も、公開時点で「製品でも完成したプロトタイプでもなく、今は使うことを勧めない」と説明していました。

つまり現時点では、すぐに自分のプロジェクトで使える道具というより、研究の方向性を示した発表として読むのがよさそうです。

公式が認める限界

公式は、「完全に検証済み」と言いすぎないようにと、限界をはっきり書いています。

保証は信頼する部品の強さまで：ログインの例では6つの部品が前提で、特にパスワードの確認とアカウントの検索が多くの約束を支えている。テストで支えているが、証明はされていない
仕様が間違っていれば意味がない：証明が示すのは「コードが仕様を満たす」ことで、「仕様があなたの意図どおり」なことではない。だから人が仕様を確かめることを重視している
証明には手間がかかる：特に証明そのものを作るところ。明確な仕様が手間を減らすカギ
始めるなら被害の大きい所から：公式はログイン・決済・権限などから始め、残りを少しずつ検証することを勧めている

IT Picksで確認したこと

2026年11月8日時点の公式ページ「PDD Kit」で、ページ内のログインの図（login explorer）を操作して、8つの条件の働き方を確認しました。

「Run a login」で間違ったパスワードの例を選ぶと、結果は「401 Unauthorized」。8つの条件のうち「間違ったパスワードには401を返す」の1つだけが当てはまり、満たされていると表示されました。

PDD Kit のページのログインの図（間違ったパスワード） — 2026年11月8日時点（出典: GitHub Next「PDD Kit」）

「Plant a bug」に切り替えると、わざとバグを仕込んだ場合を試せます。最初の「全員を拒否する」バグでは、正しいパスワードでも401になり、「正しいパスワードなら必ずトークンが出る」の条件が「Fails」になって、Verus がビルドを拒否すると表示されました。仕込めるバグは6種類ありました。

PDD Kit のページのログインの図（バグを仕込んだ場合） — 2026年11月8日時点（出典: GitHub Next「PDD Kit」）

これは説明用の図で、実際の Verus の実行結果ではありませんが、「片方の条件だけでは全員拒否のバグを見逃す」という最初の決定カードの話が、具体的に分かる作りになっていました。

IT Picks的な所感

PDD Kit の面白さは、AI にコードを書かせる時代のレビューの役割分担を組み替えようとしている点だと思います。人は「何を作るべきか」の判断に集中し、「その通りに書けているか」は数学に任せる——という分け方は、エージェントが大量のコードを書くほど意味が増していきそうです。

特に、証明できない部分を隠さず「信頼する境界」として並べ、人に1つずつ承認させる作りは、「緑のチェックが付いているから安心」という思い込みを避けるうえで誠実な設計だと評価しています。AI 同士にレビューさせる仕組みが増えるなか、決定的な検査（Verus）を最後の関門に置く発想は、ほかのツールにも広がる可能性があります。

一方で、Rust だけ・研究用プロトタイプ・導入手順なしという段階で、すぐに現場で使えるものではありません。GitHub Universe で発表された Copilot の新機能のような製品とは違い、数年先の開発のやり方を占う研究として、今後どこまで規模を広げられるかを待ちたいところです。