AIエージェントが書いたコードを数学的に証明する「PDD Kit」、Microsoftが公開

2026/11/06

AIエージェントが書くコードは「行ごとのレビュー」でカバーできなくなってきた

AIコーディングエージェントが1回のセッションで数万〜数十万行のコードを生成する時代になり、プルリクエストを人間が行ごとにレビューすることはもはや現実的ではなくなりつつある。多くのチームは「計画（プラン）」と「テスト」に投資する方向へシフトしているが、エージェントは計画からこっそり逸脱し、自分が実装したものを通過させるテストを書いてしまうという問題がある、とMicrosoft Researchは指摘している。

CI（継続的インテグレーション）のテスト数は膨れ上がり、カバレッジ上は健全に見えても、「求めていたもの」と「実際にリリースされたもの」のギャップはバグレポートが届くまで表面化しないケースが多い。

「テスト」と「証明」の違い

Microsoft Researchが今回発表した PDD Kit（Proof-Driven Development Kit） は、この問題に対するアプローチとして「形式証明」を持ち込む。

テストが「特定の入力でコードが動いたか」を確認するのに対し、数学的証明は「あらゆる入力に対してコードが仕様を満たす」ことを示す。同社によれば、これまで形式証明は専門家が必要で、コードより何倍も大きな証明を書くのに数年かかることもあったが、AIエージェントが形式仕様の記述と証明生成を補助できるようになったことで、一般的な開発者にも現実的な手段になりつつあるという。

PDD Kitの仕組み

PDD Kitは、GitHub Nextのリアルタイム共同プランニング環境 Chopin の中でパートナーとして動作する。ワークフローは大きく2段階に分かれる。

pdd-plan（計画フェーズ）：開発者が自然言語で意図を伝えると、PDD Kitが丁寧な質問を返しながら「インテント・アーティファクト」と呼ばれる文書を生成する。形式化できる部分はVerusの仕様（ensures句など）に変換され、形式化が難しい部分はテスト用の非形式仕様に分類される。
pdd-prove（検証フェーズ）：生成された仕様に基づき、Verusの証明とテストを自動生成してコードの正しさを検証する。

検証の種類はPDD Kit内で明示的に区別される。

形式検証：検証ツール（Verus）があらゆる入力に対してコードが仕様を満たすことを数学的に証明する。
実証的検証：サードパーティの暗号ライブラリやUIなど証明が届かない部分はユニットテスト・E2Eテスト・ブラウザエージェントなどで補う。ただしPDD Kitは「これは証拠であって証明ではない」と明示するとしている。

形式証明が前提とするコード範囲は TCB（Trusted Computing Base） として明示され、開発者はその各要素を承認する形になる。

Verusとは

Verus はRust向けの証明言語で、Microsoft ResearchのほかCarnegie Mellon University、VMware Research、ETH Zurich、MPI-SWS、UNSW Sydney、テキサス大学オースティン校、ミシガン大学、ブリティッシュコロンビア大学、ウィスコンシン大学マディソン校、ワイツマン科学研究所が共同開発している、とMicrosoft Researchは紹介している。

実証：ECサイト「Pet Store」のログイン検証

PDD Kitの実証として、MicrosoftはRustで書かれたフルスタックWebアプリ Pet Store を構築した。バックエンドはAxumとSQLite、フロントエンドはLeptosをWebAssemblyにコンパイルした構成で、合計約5,000行のRustコードで構成されているという。

検証のデモとして取り上げられたのはログインロジックだ。開発者がChopinに送ったリクエストはわずか2文で、「正しいパスワードを持つ者だけがトークンを受け取れる」「管理者アカウントだけが管理者トークンを受け取れる」というものだった。

PDD Kitはコードを読み込んだうえで、コーディングに入る前に Decisionsタブ に質問を表示した。最初の質問の例として紹介されているのが「正しいパスワードを入力した場合、必ずトークンを受け取れなければならないか」という問いだ。

一見細かすぎる質問に見えるが、これには理由がある。「正しいパスワードのときだけトークンを発行する（token ⇒ right password）」という条件だけでは、全員を拒否するログインでも条件を満たしてしまう。「正しいパスワードなら必ずトークンが発行される（right password ⇒ token）」という逆方向の条件と合わせて初めて「if and only if」が成立する。エージェントに任せると片方だけで済ませてしまう恐れがあるが、PDD Kitがこの点を明示的に開発者に確認するという設計になっている。

検証の結果、VerusはPet Storeのコードを堅牢化し、既存のバグも発見した。開発者は生成されたコードを行ごとに読むことなく、ログインロジックに関するバグの不在を仕様の範囲で数学的に証明できたと報告されている。

形式検証を「特殊作業」から「日常作業」へ

Microsoft Researchは、PDD Kitが形式手法を専門家だけのものから形式手法のバックグラウンドを持たないエンジニアにも開放する試みだと位置づけている。コードの全行を読む代わりに「意図」をレビューするという考え方は、AIエージェントがコード生成のボリュームを押し上げ続ける中で、開発プロセスの信頼性を維持するための一つの方向性として注目される。

出典: Formally verifying agent-written full-stack web apps with PDD Kit