11月10日、Google DeepMindが「Formal Verification of Signal's Protocol with Gemini」と題した記事を公開した。AIエージェントを活用してSignalプロトコルの実装コードを形式検証することに初めて成功した研究について詳述されている。
暗号プロトコルの「設計」を数学的に証明する研究はこれまでにも存在したが、実際にユーザーが使うプロダクションコードの「実装」まで証明の範囲を広げた事例は、AIの有無を問わず世界初だという。SignalはWhatsAppやGoogle Messagesにも採用されており、数十億人の会話を守る基盤技術だ。その実装の安全性が数学的に保証されたという事実は、ソフトウェアセキュリティの検証アプローチそのものを塗り替えうる出来事といえる。
「設計の証明」から「実装の証明」へ——長年の壁を破った理由
形式検証（Formal Verification）とは、プログラムが仕様を満たすことを数学的に証明する手法だ。バグや脆弱性の「見落とし」が原理的に起こらないことを保証でき、テストとは本質的に異なる。しかしその難易度から、実際のプロダクションコードに適用された事例は極めて少ない。
これまで暗号プロトコルの形式検証は、プロトコルの設計レベルで止まることがほとんどだった。設計と実装の間には必ずギャップが存在し、現実の脆弱性はそこに潜むことが多い。設計を証明できても、実装コードに同じ保証が及ばなければ意味は半減する。しかし実装レベルへの検証適用は、扱う状態空間が爆発的に増大するため、専門家でも現実的に完遂できないとされてきた。
Google DeepMindはその壁をAlphaProof Codeという新しいエージェントフレームワークで突破した。「AlphaProof」という名称はDeepMindの数学定理証明AI（AlphaProof）と共通しているが、AlphaProof Codeはそのアプローチをコードの形式検証に特化・拡張したフレームワークと位置づけられている。
AlphaProof Codeの仕組み——600万行のLeanコードを4週間で
AlphaProof Codeは複数のLLMを組み合わせたマルチエージェント構成で、検証作業を「何を証明するか」と「どう証明するか」に分割し、人間とAIが役割分担する設計になっている。
- 仕様の策定: 研究者がAIと協力して、Signalのセキュリティ目標を形式的な数学仕様に変換する。すべての仕様は人間の専門家がレビューする。
- 証明の実行: GeminiをベースとするAIエージェント群が証明を実行。生成したLeanコードは600万行以上に達した。Leanは定理証明支援系と呼ばれるプログラミング言語で、コードの数学的な正確性をコンパイラレベルで検証できる。
- 監査と人間のレビュー: エージェントが証明を自己監査し、人間による確認が必要な箇所をピックアップ。その量はコードベース全体のわずか1%にとどまり、残りはLeanが自動でチェックする。
このプロセス全体にかかった時間はわずか4週間。従来、同等の作業に専門家チームが取り組めば数年を要するとされてきた作業量だ。検証では「デバイスが一時的に侵害される前後もメッセージが保護される（Forward SecrecyおよびPost-Compromise Security）」といった主要なセキュリティ特性が証明された。
バグ検出能力を実証——過去の実在バグで試験
AlphaProof Codeが「正しいコード」と「バグのあるコード」を実際に区別できるかどうかを確認するため、過去に実際に存在し修正済みのバグ2件を意図的にSignalコードの隔離環境に再導入して検証を行った。
いずれのケースでも、システムはバグのあるバージョンが安全でないことを機械検証済みの証明として出力した。偽陰性（バグを見逃す）がなかったことで、手法の信頼性を実証的に裏付けた形だ。
オープンソース公開と今後の応用
形式検証の成果物はすでにオープンソースとして公開されており、コミュニティが検証アーティファクトを参照・利用できる状態だ。
- 形式検証アーティファクト: google-deepmind.github.io/code-verification
今後は医療機器のファームウェアや電力グリッドソフトウェアなど、他の重要インフラへの応用も視野に入っているという。設計の証明にとどまらず実装コードまで保証の範囲を広げたことは、ソフトウェアセキュリティの検証がどこまで自動化できるかという問いに対して、一つの明確な答えを示した。
詳細はFormal Verification of Signal's Protocol with Geminiを参照していただきたい。
