AIに関するセキュリティのニュースの多くはバグを見つける話です。Google DeepMindのAlphaProof Codeは、少なくとも特定の特性について、何十億人もが使うコードにバグがないことを証明する話です。DeepMindによると、同社のエージェントはSignalプロトコルを支えるコンパイル済みコードについて重要なセキュリティ特性を証明しました。このプロトコルはWhatsApp、Messenger、Google Messagesの暗号化の基盤でもあります。同社は、このようなプロトコルの実装がいかなる方法であれ形式的に検証されたのは初めてだとしています。
作業の進め方は結果と同じくらい重要です。仕様を書くエージェントが研究者と協力して研究文献のセキュリティ目標をLeanに落とし込み、レビュー役のエージェントが草案を批評し、人間がすべての仕様を承認しました。その後、Gemini 4 Carbonで動く証明エージェントが証明を書きました。エージェントはコードベースの約1パーセントを人間による再確認の対象として指摘し、それ以外はすべてLeanのカーネルが検査しました。付随する論文によると、5人のチームが4週間でこの作業を行い、各自が自分のマシンでエージェントを休みなく走らせ、対象はlibsignalのバージョン0.105.4でした。
懐疑的な人を納得させるはずなのは、バグを使った確認です。チームは修正済みの実際のバグ二つを、隔離したコードのコピーに戻しました。どちらの場合も、システムはバグのあるバージョンが 安全でないことを示す機械検証済みの証明を出しました。そのうち一つは、古いセッションでのみ復号されるはずのメッセージの後で、libsignalが秘密鍵を含む新しいセッションの状態を保存してしまうものでした。SignalのCTOであるEhren Kret氏は、以前の検証はコードのより小さな部分しか対象にしていなかったとし、稼働中のコードを有効なLeanの定理に変換することは大きな進歩だと述べています。
開発者にとってより広い意味は、形式的な証明が手の届くものになりつつあることです。論文は、検証を目的に書かれたコードに専門家が何年もかけたseL4やCompCertと比較しています。私たちがレビューしたLean LSP MCPのようなツールはすでにコーディングエージェントがLeanの検査器を相手に作業できるようにしており、DeepMindも自らの検証成果物を公開しています。
限界も明記されています。検証の対象は1対1のセッションのコードで、Signal全体ではありません。記号的な保証は暗号が完全であることを前提とし、結果はLeanのカーネルと、コードが呼び出す一部のルーチンの契約を信頼しています。DeepMind自身も、この手法を拡大するにはさらなる研究が必要だとしています。そして証明の強さは証明対象の仕様次第であり、だからこそ人間が承認した仕様こそ外部の確認に最も値する部分です。