研究論文を一般向けに解説するYouTubeチャンネルTwo Minute PapersがDeepMindのAlphaProof Codeを取り上げましたが、その元になった論文は注目に値します。主な主張は、AIエージェントがSignalプロトコルの重要なセキュリティ特性を、単純化したモデルではなく、実際にスマートフォンで動くマシンコードについて証明したというものです。Signal、WhatsApp、Google Messagesに頼る人にとって、実際のバグが潜みやすいのはまさにこの層です。
論文は報道よりも正確です。対象はRustで書かれたリファレンス実装libsignalで、標準のコンパイラでAArch64のマシンコードにコンパイルされ、プロセッサの形式モデルとともにLeanに読み込まれました。エージェントは機械検証済みの証明を約650万行生成し、その土台は約26,000行の信頼された仕様とプロセッサの意味論です。証明はポスト量子のPQXDHハンドシェイクとTriple Ratchetを対象とし、前方秘匿性、認証、侵害後の安全性、ハンドシェイクの秘匿性を確立しています。DeepMindのブログによると作業は4週間で、人間はすべての仕様と、エージェントが指摘したコードベースの約1%を確認しました。
主張を信頼できるものにしているのは設計です。証明を書くエージェントは信頼されない存在として扱われます。ゲートキーパー役のエージェントは、Leanのカーネルが証明を検査し、さらに比較ツールが承認済みの仕様の保管コピーをちょうど証明していると確認した場合にのみ証明を受け入れます。そのためエージェントが目標をこっそり弱めることはできません。比較として論文 は、seL4マイクロカーネルの検証に20人年、CompCertコンパイラに6人年かかり、どちらも最初から検証を前提に書かれていたと指摘しています。
同じ構図が普段の開発ツールにも広がっています。私たちがレビューしたLean LSP MCPは、検査器が受け入れる証明を書けるよう、エージェントにLeanの証明状態とエラーを渡すサーバーです。今回のエージェントはGemini 4 Carbonで動いていました。重要なコードにAIを使う人への教訓は、モデルと結果の間に言い逃れの通じない検査器を置くことです。
限界は論文自体に書かれています。結果は、Leanのカーネル、基盤となる暗号プリミティブの安全性、コードが呼び出す一部のルーチンの挙動を信頼しています。証明がカバーするのは仕様に書かれた内容だけなので、その26,000行の信頼された部分に抜けがあれば、保証にも抜けが生じます。成果物は検証のために公開されていますが、独立した精査はまだ行われていません。