Google DeepMindがAIでコードを検証する「AlphaProof Code」を使ってSignalプロトコルの安全性の形式的検証に成功

Our teams put Gemini 4 Carbon to work on a major security challenge: mathematically proving the code underlying the Signal protocol.

Using AlphaProof Code, @GoogleDeepMind researchers guided agents to verify the protocol down to compiled device code, closing the gap where real bugs hide. The result:

- Gemini 4 Carbon generated over 6M lines of machine-checked Lean proofs
- years of expert manual verification compressed to just weeks
~1% of the codebase required human review (Lean automatically checked the rest)

This is helping unlock scalable formal verification for building secure software, laying the groundwork to fundamentally shift the advantage to defenders. We’re open sourcing the results for the security community.

— Sundar Pichai (@sundarpichai) November 10, 2026

形式的検証とは、ハードウェアやソフトウェアのシステムについて、形式手法や数学などを利用してシステムの正しさ、あるいは間違いを証明することです。AlphaProof Codeは複数の大規模言語モデル(LLM)を用いたエージェント型フレームワークであり、これまでにない深度で形式的検証を可能にするために開発されました。

AlphaProof Codeは実際の研究チームが行うように形式的検証の作業を分割し、何を証明するべきなのかを決定して、証明作業をAIエージェントと人間の専門家が協力して実行するのを助けるとのこと。今回DeepMindの研究チームは、さまざまなメッセンジャーアプリで採用されているエンドツーエンド暗号通信プロトコルの「Signalプロトコル」について、AlphaProof Codeを用いた形式的検証に取り組みました。

Signalプロトコルの形式的検証では、複数のAIモデルを駆使してプロトコルのセキュリティ目標を正式な数学的仕様に変換し、そのすべてを人間の専門家がレビューしました。その後、最先端のサイバーセキュリティと長期的な運用能力を備えたAIモデル「Gemini 4 Carbon」を搭載したエージェントが証明を行い、コードの正確性を数学的に証明するプログラミング言語・Leanを利用して、600万行にわたる証明を生成したとのこと。

続いてAIエージェントがLeanの証明を調査し、人間の目視による再確認が必要な箇所を特定しました。この箇所は全体のわずか1％に過ぎず、大幅な時間短縮につながったとされています。これにより、本来であれば専門家による数年間の作業が必要な形式的検証が、わずか4週間で完了したと報告されています。

さらに研究チームは、正しいコードとバグがあるコードを区別するAlphaProof Codeの能力を確かめるため、すでに修正済みのバグを2つコードに組み込んで再評価させました。その結果、AlphaProof Codeはバグのあるバージョンが安全ではないことを示す検証結果を生成したとのことです。

Signalプロトコルをはじめとする暗号プロトコルは、オンラインバンキングからウェブブラウジングまで、ほぼすべてのデジタル通信の基盤となっています。たった1つの脆弱(ぜいじゃく)性があるだけで膨大な数の個人情報が危険にさらされることから、専門家らは長年にわたりこれらのプロトコルの形式的検証に取り組んできました。

しかし、ほとんどのプロトコル検証は設計段階で終了しており、実際にコンパイルされたコードの検証はあまり進んでいません。AlphaProof Codeを用いた今回の取り組みは、Signalプロトコルが重要なセキュリティ要件を満たしていることを、デバイス上で実行される正確なコードレベルまで検証した点に意義があります。

Signalのエーレン・クレットCTOは、「従来の形式的検証は必然的に小規模な範囲に絞られていましたが、この新しいアプローチにより大幅な拡張が可能になります。従来、本番コードが暗号設計と厳密に一致していることを検証するには、膨大な手作業が必要でした。そのため、AIエージェントを使用してライブコードを自動的に有効なLean定理に変換することは、大きなブレイクスルーとなります。AIによるセキュリティ脅威が増大する中、コアとなるSignalプロトコルを自動定理証明によって厳密に検証することで、コードがプライバシー保証を確実に履行しているという確信がさらに高まります」とコメントしました。

DeepMindのヴァイスプレジデントを務めるプシュミート・コーリ氏は、「研究としてのブレイクスルーを超えて、これは最先端AIが現代のサイバー脅威の速度と規模に対抗するための増幅器となり得ることを示す、典型的な例となります」と述べました。

Announcing a major milestone achieved by my team @GoogleDeepMind: we have proven key security properties of the machine code underlying the Signal messaging protocol. This is the first time the actual production code of a widely deployed protocol has been formally verified – by any method, with or without AI – and at this depth.

More than a research breakthrough, it’s a prime example of how frontier AI can be a force multiplier to counter the speed and scale of modern cyber threats.

Formal verification offers a higher standard of security; however, it’s extremely complex and time consuming, which is why in many cases it’s considered to be impractical. Similar efforts could take teams decades of combined effort. We did it in a month’s time.

Using AlphaProof Code, Google DeepMind's new agentic framework for formal verification that runs on LLMs including Gemini Carbon, we verified the Signal protocol down to the actual code running on devices. This milestone lays the groundwork for a future in which vital systems, from medical device firmware to power grid software, ship with mathematical proof that their protections work.

Reaching that future will take continued research from our community. In that spirit, we're open-sourcing our formal specifications and verification artifacts so others can build on this work.

On a personal note, this moment is of deep significance to me. I started my own research journey more than two decades ago as an intern working on checking the consistency of complex software systems. Seeing this grand challenge made practical with modern AI is extraordinary.

I'm extremely proud of my team members: Swarat Chaudhuri, Andrew Ferraiuolo, Anton Kovsharov, Tej Chajed, Sam Schlesinger, Karn Seth, Jonathan Katz, and Charles Sutton for taking on this grand challenge and delivering, and grateful to the Signal team for their partnership.

https://t.co/kN1eRYQ8fF

— Pushmeet Kohli (@pushmeet) November 10, 2026