マイクロソフト、AI製ログインコードを数学で証明

マイクロソフトリサーチは11月5日(現地時間)、AIエージェントが書いたRust製Webアプリのログイン処理が、あらゆる入力で仕様を満たすことを研究試作ツール「PDD Kit」で機械的に検証したと発表した。対象は約5000行のアプリの一部で、開発者は生成コードを1行ずつ読まず、意図の確認だけを担った。

要点

• PDD Kitは開発者の自然言語の意図を形式仕様に変換し、検証器Verusでエージェント製のRustコードと照合する。
• デモアプリPet Storeでは2文の依頼が8個の証明条項となり、5個の関数を証明、6個の要素は信頼対象としてテストで確認した。
• 現時点ではRust専用の研究試作であり、発見したバグの件数や証明コストは公表されていない。

AI生成コードの形式検証、PDD Kitの仕組み

PDD KitはGitHub Nextの共同計画環境Chopin上で動作する。計画段階でコードを読み、実装前に質問を投げかけ、回答をチームが確認する文書にまとめる。その後コーディングエージェントが実装と証明を書き、VerusがZ3ソルバーを使って結果を検査する。

マイクロソフトリサーチのブログは「レビューは『正しそうか』を問い、証明は『正しいか』に答える」と説明する。仕様、コード、証明を書くのはモデルだが、合否を決めるのは決定論的なVerusの実行である。

検査時間は小規模なモジュールで通常数秒、大規模なコードベースで数分程度だという。この検査をCIに組み込めば、証明が崩れた時点でビルドが失敗する。

Pet Storeのログインで証明された内容

開発者の依頼は「正しいパスワードのときだけトークンを発行する」「管理者アカウントだけに管理者トークンを発行する」の2点だった。PDD Kitは、正しいパスワードなら必ず通すべきかを問い返した。全員を拒否するログインでも、第1の規則だけなら満たしてしまうためだ。

こうして8個のensures条項と7タスクの構築計画が生まれ、5個の関数があらゆる入力について証明された。何も排除しない空疎な条項、いわゆる「バイブ検証」を防ぐため、条項ごとにバグを1つ埋め込んだ複製をVerusが拒否するかも確かめる。

証明が及ばない範囲

データベース検索2件、bcryptによるパスワード確認、トークン署名、時計、データベースのエラーメッセージ、ハンドラーのリクエスト展開の6要素は証明の外にある。いずれも開発者が個別に承認し、テストで確認した。

研究チームは「保証の強さは信頼する6要素の強さまでだ」と記している。ログインが必ず完了することや、応答時間、試行頻度も保証の対象外である。既存のバグを発見したとするが一覧は示しておらず、AI Newswayは第三者による評価を確認できなかった。

形式検証が再び注目される背景

エージェントが生み出すコード量が人間のレビュー能力を上回りつつあり、証明が代替手段として浮上している。アンソロピックは10月22日、Claudeでオープンソースライブラリ123個がクラッシュしないことを証明したと発表した。AlphaSignalによれば、PDD Kitは10月21日に研究プレビューとして初めて紹介された。

今後の展望

マイクロソフトは、ログインや決済、権限管理などバグの代償が大きい箇所から適用するよう勧めている。信頼に頼る範囲は今後縮小するとみており、手法がどこまで拡張できるかを見極めるとしている。

よくある質問

証明されたコードにバグはないのか。 そうではない。明示した前提のもとでコードが仕様を満たすという意味であり、仕様自体が誤っている可能性は残る。

Rust以外の言語でも使えるのか。 直接は使えない。Rustへ移植するか、バインディング経由で検証済みのRustを呼び出す必要がある。

参考資料

• Formally verifying agent-written full-stack web apps with PDD Kit — Microsoft Research(2026年11月5日)
• GitHub - verus-lang/verus: Verified Rust for low-level systems code — Verusプロジェクト
• Chopin — GitHub Next
• Microsoft's PDD Kit Makes Formal Math Proofs a Gate for AI Rust Code — AlphaSignal(2026年10月21日)