GitHub NextとMicrosoft Researchは、AIエージェントが生成したコードを仕様に照らして検証する「Proof-Driven Development Kit（PDD Kit）」を紹介しました。開発者が要求を確認して機械で検証できる仕様にまとめ、エージェントが実装と証明を作成し、Rust向け検証ツールのVerusが証明を検査します。
PDD KitはChopin内で動作する研究用プロトタイプで、現在の対象はRustです。GitHub Nextは、コード生成が速くなる一方、人がすべての変更を行単位でレビューするのは難しくなっていると説明しています。
実例は、Rust製Webアプリ「Pet Store」のログイン処理です。PDD Kitは開発者との対話で曖昧な要求を具体化し、形式化できる部分を仕様にします。
要求を仕様にする対話
開発者が最初に与えた要求は、「正しいパスワードの場合だけトークンを発行する」「管理者アカウントだけに管理者用トークンを発行する」という内容でした。
「正しいパスワードの場合だけ」という条件では、すべてのログインを拒否する実装も条件を満たします。そこでPDD Kitは、正しいパスワードならトークンを必ず発行する条件も必要か質問し、開発者はその条件を加えました。
一方、データベース検索やトークン署名に失敗した場合は、サーバーエラーを返す仕様になりました。ログイン処理には最終的に8つの条件が設けられ、パスワード照合に使ったアカウントとトークンが示すアカウントの一致も含まれます。
VerusがRustの仕様を検査
Verusでは、実行するRustコードに加えて、関数が満たす条件を「requires」や「ensures」などで記述します。Verusは仕様と証明をRustの構文で扱い、実行可能なコードが仕様を満たすか静的に検査します。
検査では、プログラムの仕様やアサーションから「検証条件」と呼ばれる論理式を生成し、SMTソルバーのZ3で確かめます。検証時に実行時チェックを追加するのではなく、仕様が定める範囲で、可能な実行について条件が成り立つかを調べます。
ただし、条件が正しくても、ソルバーが自動で証明できない場合があります。量化子を含む論理式や帰納的な不変条件、証明に時間がかかる場合などは検証に失敗することがあり、追加の証明記述が必要になる場合もあります。
証明の対象と前提を確認
ログイン例では、データベース検索、bcryptによるパスワード照合、時刻取得、トークン署名に使う外部ライブラリ内の処理は証明の対象外です。それらが仕様で想定したとおりに動くことを前提として、ログイン処理の正しさを証明します。
PDD Kitは実装前に、こうした前提と、前提が成り立たない場合に失われる保証を開発者に示し、処理ごとの承認を求めます。前提を確かめるテストも計画し、証明できない処理にはテストを組み合わせます。
検証が保証するのは仕様に書いた範囲です。このログイン例では、処理が応答を返した場合に結果が条件を満たすことを対象とし、処理の完了や応答速度までは保証しません。
バグを仕込み、変更後も検証
仕様が弱いままでも証明が通る問題に対し、PDD Kitは作業用コピーに仕様の条件に違反するバグを一つずつ入れ、Verusが狙った違反を検出するか確かめます。仕様と証明が同じ誤解を共有していないかを調べる手順です。
証明とテストの結果はレビュー用LLMが計画や仕様と照合します。確認できていない要求があればコーディングエージェントに対応を求め、仕様に矛盾がある場合は開発者に判断を促します。
検査とテストを通過すると、PDD Kitは実装、証明、テストを含むプルリクエストを作成します。マージ後も継続的インテグレーションにVerusの検証とテストを組み込み、コード変更のたびに同じ仕様を満たすか確認します。
適用例はログイン処理の1件で、GitHub Nextは証明の作成には現在も手間がかかるとしています。PDD Kitは限定的な研究プレビューで、より広い範囲への適用が探られています。
