2026年11月10日、Google DeepMind は公式サイトで AlphaProof Code を発表した。AlphaProof Code は、人間の専門家と AI エージェントを組み合わせた形式検証フレームワークである。新しいチャットモデルの投入ではない。

研究者はこのフレームワークを用い、Signal プロトコルの参照実装である libsignal の選定された重要なセキュリティ特性を証明し、その証明をコンパイル後のマシンコード／AArch64 まで通した。公式ブログは、対象の技術を Signal や Google Messages のようなアプリで私的な会話を保護する技術として述べている。論文は、結果が今回の libsignal-cli ビルドに関するものであり、Signal 自身のアプリケーションではないと記している。

技術論文と成果物ページは、エージェントが約 650 万行のマシン検査済み Lean 証明コードを生成したと記している。公式ブログ本文は、エージェントが600 万行を超える Lean を生成したと記している。

論文によれば、証明は Signal のポスト量子 PQXDH ハンドシェイクと Triple Ratchet を対象とし、前方秘匿性、認証、危殆化後の安全性、ハンドシェイクの秘匿性を確立している。論文は、広く使われている暗号プロトコル実装の未改変のコードに、プロトコル水準のセキュリティ保証をつなぐ初めての証明だと述べている。

証明は Gemini Carbon（論文では Gemini 4 Carbon）を搭載したエージェントが作成した。研究者は複数のモデルと協力して形式仕様を起草し、人間の専門家がすべてを逐一確認した。論文は仕様段階で Claude Opus 5.5 にも言及し、著者は証明コードを一切書いていないとしている。証明は Gemini 4 Carbon のエージェントチームが作成した。これらの証明に用いたモデルの既存の紹介（2026年10月28日、本日の発表ではない）は、次を参照：Google、次のフロンティアモデル「Gemini 4 Carbon」を発表。今回の AlphaProof Code の発表は、Carbon の新たな API や料金の発表ではない。

公式ブログは、検証プロセスにわずか 4 週間を要したとしている。論文は、証明作業を5 人のチームが 4 週間で行ったと補足している。

Google DeepMind は、広く展開された暗号プロトコルを AI がこの深さで形式検証したのは初めてだとし、このように広く展開されたプロトコルの実装が、AI の有無を問わず何らかの方法で形式検証されたのも初めてだとしている。これは、Signal アプリケーション全体、あるいは起こり得るすべての失敗モードが検証済みだという主張ではない。

フレームワークが正しいコードと欠陥のあるコードを区別できるかを確認するため、研究者は、以前に修正済みの実際の欠陥を 2 件、隔離した版のコードに再導入した。いずれの場合も、欠陥のある版が安全ではないことを示す、マシン検査済みの証明が得られた。これは回帰確認であり、Signal の新しい脆弱性を報告したものではない。

「従来の形式検証はコードのより狭い部分に焦点を当てていたが、Google DeepMind の手法は大幅な拡張を可能にする」と、Signal の最高技術責任者 Ehren Kret は述べている。「稼働中のコードを妥当な Lean 定理へ翻訳する AI エージェントの利用は、大きなブレークスルーだ。AI を用いたセキュリティ上の脅威が増すなか、Signal プロトコル実装を厳格に検証することで、コードのプライバシー保証に対する確信はさらに高まる。」

形式検証の成果物と技術論文は公開されている。