GitHub Next 介紹 PDD Kit，以形式化證明驗證 AI 智能體生成程式碼符合規格
GitHub Next、AI生成コードが仕様を満たすことを証明する「PDD Kit」を紹介
GitHub Next 與 Microsoft Research 共同開發 PDD Kit，透過與開發者對話把需求整理成可由機器驗證的規格，再以數學證明檢查 AI 智能體生成的程式碼是否符合規格。
GitHub Nextは2026年11月4日、Microsoft Researchと共同開発するProof-Driven Development Kit（PDD Kit）の仕組みと、ログイン処理への適用例を紹介した。PDD Kitは、開発者との対話を通じて要求を機械で検証できる仕様にまとめ、AIエージェントが生成したコードがその仕様を満たすことを数学的な証明で確かめる。現在はRustのコードを対象とする研究用プロトタイプで、提供は限定的な研究プレビューにとどまっている[1]。
How we can secure 50% of the world's software. Traditionally, formal methods have been mostly used for safety-critical systems like operating systems, hypervisors, and databases. We're extending this to formally and empirically verify code correctness and security for full-stack web apps, one of the most common types of applications*, using the Proof-Driven Development Kit (PDD Kit). Coding agents now write code faster than anyone can review effectively. PDD Kit turns what the developer meant into a Verus specification. It then proves the AI-generated code meets that spec for every input. Researchers @alexlavaee, @MatthaiP39719, @Mappletons, and @k_cieslak break down Proof-Driven Development x Chopin in the blog here: https://t.co/EwhqTx2OjT *44.4% of respondents work as full-stack (27.3%), back-end (13.5%), or front-end (3.6%) developers. Stack Overflow Developer Survey 2026, n = 25,767.
— GitHub Next (@GitHubNext) November 4, 2026
GitHub Nextは、AIエージェントのコード生成量が増えるにつれ、人が全行をレビューすることが難しくなる点を課題に挙げる。また、エージェントが要求を誤解すると、その誤解がコードとテストの両方に入り、テストを通過しても意図した動作にならないことがあると指摘する。PDD Kitでは、人がソフトウェアに求める動作を決め、その内容が仕様に反映されているかをレビューする。
開発者との対話で、曖昧な要求を仕様にする
PDD Kitは、GitHub Nextが開発するWebアプリChopinの中で動作する。Chopinは自分のPCやサーバーに設置し、ブラウザーから操作する[2]。チームで共有する開発計画の文書を直接編集できるほか、チャットでAIエージェントに調査や文書の修正を頼める。
PDD Kitは、この計画づくりの中で既存のコードを読み、処理の内容を説明しながら開発者に質問する。回答を基に、開発者が求める動作を文書に整理する。そのうち、機械で検証できる条件として表せる部分を、Rust向けの検証ツールVerusで扱える仕様に書き起こす[3]。
PDD Kitの公式ページでは、この仕様づくりの流れを、Rust製のWebアプリ「Pet Store」のログイン処理を例に説明している。このアプリは、ログインに成功すると、アカウントの識別情報や顧客・管理者といったロールを記録したトークンを発行する。開発者は、この処理について「正しいパスワードの場合だけトークンを発行する」「管理者アカウントだけに管理者用トークンを発行する」という要求をPDD Kitに与えた。
「正しいパスワードの場合だけトークンを発行する」という条件では、間違ったパスワードでトークンを発行してはいけない。しかし、すべてのログインを拒否してトークンを一切発行しない実装でも、この条件は満たせてしまう。そこでPDD Kitは、実装に入る前に「正しいパスワードなら必ずトークンを発行することも求めるか」と確認した。
開発者は、正しいパスワードならトークンを発行することも求めた。ただし、パスワードが正しくても、DB検索やトークンへの署名が失敗することはある。そのため、最終的な仕様では、これらの処理に失敗した場合は、トークンの代わりにサーバーエラーを返してもよいとした。
こうして、ログイン処理の仕様には8つの条件が盛り込まれた[4]。たとえば、パスワードの照合に使ったアカウントと、トークンが示すアカウントが一致することが条件になっている。この条件により、自分のパスワードで認証したのに、別人のトークンが発行されるようなバグを捉えられる。
実際の仕様づくりでは、PDD Kitは処理の流れを図で説明し、開発者による仕様の確認を助ける。Verus向けに書いた仕様にも、各条件を説明する英語のコメントを付ける。開発者は、要求が意図どおりに表されているかを確認し、仕様を承認する。
エージェントが証明を生成し、Verusが検査する
コーディングエージェントは、承認された仕様を基に実装を生成し、その実装が仕様を満たすことを示す証明も作る。Verusがこの証明を検査し、定めた前提の下で、仕様の対象となるすべての入力について条件が成り立つかを確かめる。このような形式検証は、個々の入力でコードを実行して結果を観察するテストとは異なる。
ただし、仕様の条件が緩すぎると、意図に反するコードでも証明が通ってしまう。そこでPDD Kitは、コードの作業用コピーに、仕様の各条件に違反するバグを一つずつ意図的に入れる。Verusがそのバグを、狙った条件への違反として検出することを確かめる。
証明の対象外となる処理は、テストで確かめる
今回のログイン処理では、DB検索、bcryptによるパスワード照合、時刻の取得、トークンへの署名などに、別のライブラリを使っている。ただし、これらのライブラリ内の処理自体は、今回の証明の対象に含まれない。そこで、それぞれの処理が仕様で想定したとおりに動くことを前提に、ログイン処理の正しさを証明する。
こうした証明の前提について、PDD Kitは実装前の計画段階で、各処理が満たすと仮定する条件を開発者に説明する。その条件が成り立たない場合にどの保証が失われるかも示し、処理ごとに承認を求める。あわせて、前提とした各条件を確かめるテストも計画する。
証明の対象となる処理でも、保証されるのは仕様に書いた範囲に限られる。今回の仕様では、ログイン処理が応答を返したときに、その結果が条件を満たすことを保証する。処理が必ず完了することや、どのくらいの時間で応答するかまでは保証しない。
検証結果を確認してマージし、変更後も検証する
レビュー用のLLMは、計画、仕様、検証結果を照らし合わせ、実装が各要求を満たすことを証明またはテストで確認できているかを調べる。証明とテストのどちらでも確認できていない要求があれば、コーディングエージェントに対応を求める。仕様自体に矛盾がある場合は、実装の修正だけでは解決できないため、PDD Kitは開発者に判断を求める。
証明の検査とテストを通過すると、PDD Kitは、実装・証明・テストを含むプルリクエストを作成する。そこには、証明できたこと、証明の対象外とした処理についての前提、テスト結果、保証の範囲も記載する。開発者は、求めていた動作と照らし合わせて内容を確認し、マージする。マージ後は、Verusによる検証とテストを継続的インテグレーション（CI）にも組み込み、コードの変更のたびに同じ仕様を満たすことを確かめる。
今回の事例は1つのアプリのログイン処理に限られる。GitHub Nextは、証明の作成には今も手間がかかるとしつつ、より広い範囲に適用できるかを探っている。
來源：gihyo.jp · gihyo.jp