Google DeepMind的研究人员说，他们用一套叫AlphaProof Code的智能体框架，在四周里生成了超过600万行Lean证明，去核验Signal协议真正编译后跑在设备上的代码。

这篇文章由Pushmeet Kohli和Swarat Chaudhuri撰写，2026年11月10日发布。Signal协议保护着Signal和Google Messages等应用里数十亿次私人对话。作者把形式化验证称为安全保证的最高标准：用数学证明代码会按预期运行、没有漏洞。他们也写到，这种方法很难，而且往往非常费人力。

他们给出了两项自己的定位。这是第一次用AI，把一个广泛部署的密码协议形式化验证到这种深度。不论有没有用AI，这也是第一次有人把这类广泛部署的协议实现，形式化验证到这种深度。这是作者的判断，不是第三方审计结论。

人先决定证明什么，Gemini Carbon再去写证明

AlphaProof Code被写成一个多模型智能体框架，分工接近一支研究团队：人类专家和AI一起决定要证明什么，再由一组AI智能体去做证明。

第一步，研究人员和一组模型一起，把Signal的安全目标翻译成形式化的数学规范，每一条都由人类专家审过。随后，由Gemini Carbon驱动的智能体去写证明，生成了超过600万行Lean。Lean是一种用来数学证明代码正确性的计算机语言。文中写的是Gemini Carbon，没有在这篇里写成Gemini 4 Carbon。

智能体随后审计这些证明，并标出需要人再看一遍的地方，作者说只占代码库的1%。其余部分由Lean自动检查。这样专家可以把复核集中在最需要人类判断的位置。

密码协议托住了几乎所有数字通信，从网上银行到浏览网页。作者写到，一个漏洞就可能同时让数百万人暴露，这也是专家几十年来持续形式化分析这些协议的原因。

大多数协议验证停在设计层。这次智能体走得更远：证明编译后的代码满足关键安全属性，一直到设备上实际运行的那份代码。文中举的例子包括，设备被临时攻破之前和之后，消息仍然受到保护。作者认为，真实漏洞常常藏在设计和实现之间的缝隙里，补上这层会让证明复杂得多。

即便如此，他们说整个验证过程只用了四周。按他们的对照，这类工作过去常要专家团队花上数年。结论被表述为：Signal的核心密码代码，达到了专家所规定的那些安全保护。

为了确认这套系统分得清正确代码和有缺陷的代码，他们把两个真实、此前已被修复的漏洞，重新放进一份隔离的Signal代码里。两次结果都是：系统给出了机器可检查的证明，说明有缺陷的版本并不安全。文中没有写出这两个漏洞的名称或细节。

文中的流程图把流程分成三步：先起草并批准Lean规范，再让编译后的机器代码在Lean的处理器模型上运行，然后由证明团队生成证明，并由门卫检查。图注写的是：智能体先帮助用户写规范，再自主证明实现符合规范，每份证明都由Lean检查。

Signal的CTO怎么看，以及作者自己的后续表述

Signal首席技术官Ehren Kret在文中被引用说，以往的形式化验证往往只覆盖代码里较小的部分，Google DeepMind的方法使显著扩展成为可能；用AI智能体把正在使用的代码翻译成有效的Lean定理，是一项重大突破。他说，AI驱动的安全威胁在增加，严格验证Signal协议的实现，让他们对代码的隐私保证更有信心。

紧接着，页面上还有一段未再标注发言人的表述，意思接近，但用词不完全相同。那段话写到，以往工作的范围必然更小；传统上要验证生产代码严格符合密码设计，需要大量手工；用AI智能体自动把正在使用的代码翻译成有效Lean定理，是很大的突破。它也写到，在AI驱动的安全威胁增加时，用自动定理证明严格验证Signal核心协议，让他们更有信心认为代码兑现了隐私保证。这段是页面正文，不宜直接当成Kret的另一句原话。

作者把这看成可扩展的安全方法，材料和论文已经公开

在展望里，作者认为做成这件事表明，AI可以把很高标准的安全保障带给企业、政府和关键基础设施，用来抵御由智能体驱动的网络威胁。他们说，验证Signal的核心密码学，也为保护其他关键系统打下基础，举例包括医疗设备固件和电网软件。

他们也写到，要把这些技术做大，还需要继续研究。文中提到，如果和CodeMender这类自动防御智能体一起用，形式化验证可以帮助应对现代网络威胁的速度和规模，做出带有数学证明的软件保护。CodeMender是Google方面的自动防御工具，这篇没有展开它的评测细节。

他们已经把形式化验证产物开源，供社区使用。技术论文在 https://deepmind.google/documents/36/Formal_Verification_of_Signal_4.pdf ，开源材料在 https://google-deepmind.github.io/code-verification 。这篇改写依据的是博客正文，没有把论文里的额外数字写进来。

这项研究的开发者是Swarat Chaudhuri、Andrew Ferraiuolo、Anton Kovsharov、Tej Chajed、Sam Schlesinger、Karn Seth、Jonathan Katz、Charles Sutton和Pushmeet Kohli。他们感谢Eric Wieser帮助开源代码，Owen Jones提供项目管理支持，并向Martín Abadi、Christopher Henson、Katerina Hristova、Henryk Michalewski、Jonathan Protzenko和George Tsoukalas致谢讨论。Signal方面，Rolfe Schmidt、Michael Rosenberg和Ehren Kret为方法提供了反馈。文中还感谢Tulsee Doshi、Four Flynn、Kate Olszewska、Alicia Huang、Andy Liu、Benoit Schillings、Raluca Ada Popa、Melvin Johnson、Koray Kavukcuoglu、Demis Hassabis和Sundar Pichai对项目的支持。

如果要判断这些证明到底覆盖了哪些定理、信任了哪些规范，下一步应直接读他们公开的论文和Lean产物，而不是只停留在这篇介绍。

Introducing AlphaProof Code: a breakthrough in verifying complex software at depth

Pushmeet Kohli and Swarat Chaudhuri

November 10, 2026
Research
URL: https://deepmind.google/blog/introducing-alphaproof-code/

How Google DeepMind researchers built a new agentic framework that formally verified the code of Signal’s cryptographic protocol — long considered to be a grand security challenge

Today, we’re sharing a milestone in software security long considered to be a grand challenge: Google DeepMind researchers guided AI agents to mathematically prove key security properties of the actual code underlying the Signal protocol, the technology that protects billions of private conversations in apps like Signal and Google Messages.

This breakthrough discovery was made using AlphaProof Code, a novel agentic framework for formal verification at unprecedented depth that combines human expertise with AI agents. Formal verification—mathematically proving code runs correctly without flaws—is the highest standard of security assurance; however, it is difficult and often labor-intensive.

Our work marks the first time AI has been used to formally verify a widely deployed cryptographic protocol at this depth. It's also the first time the implementation of a widely deployed protocol like this has been formally verified by any method, with or without AI.

How we verified Signal

AlphaProof Code is a multi-LLM agentic framework that splits the work of formal verification the way a research team would: human experts work with AI to decide what to prove, and a group of AI agents does it.

First, our researchers collaborated with a mix of models to translate Signal’s security goals into formal mathematical specifications, with human experts reviewing every one. From there, agents powered by Gemini Carbon did the proofs, generating over six million lines of Lean, a computer language that mathematically proves the accuracy of code.

Next, the agents audited the proof and highlighted areas that needed a second look by a human – just one percent of the codebase, a massive time savings. Because Lean automatically checks the rest, our experts could focus their review where human judgment matters most.

Cryptographic protocols underpin nearly all digital communication, from online banking to web browsing, and a single flaw can expose millions of people at once. That's why experts have spent decades formally analyzing them.

But most protocol verification stops at the design level. Our agents went further, proving that the compiled code fulfills the key security properties – such as keeping messages protected before and after a device is temporarily compromised – down to the exact code running on devices. Because real-world vulnerabilities often hide in the gap between design and implementation, bridging this gap makes these proofs vastly more complex.

Even at this complexity, our verification process took just four weeks – a task that historically takes expert teams years – proving that Signal's core cryptographic code delivers the security protections our experts specified.

To confirm that AlphaProof Code can tell correct code from buggy code, we reintroduced two real, previously fixed bugs into an isolated version of Signal's code. In both cases, the system produced a machine-checked proof that the buggy version was insecure.

In AlphaProof Code, AI agents help users write a specification, then autonomously prove that the implementation meets it. Every proof is checked by Lean to verify the agents' work.

While prior formal verification focused on smaller portions of the code, Google DeepMind's approach enables significant expansion,” said Ehren Kret, Chief Technology Officer of Signal. “Using AI agents to translate live code into valid Lean theorems is a major breakthrough. As AI-driven security threats grow, rigorously verifying the Signal protocol implementation gives us even greater confidence in our code's privacy guarantees.

Ehren Kret, Chief Technology Officer of Signal

While prior formal verification work has necessarily focused on smaller scopes, this new approach enables a significant expansion. Traditionally, verifying that production code strictly matches its cryptographic design required extensive manual effort, making the use of AI agents to automatically translate live code into valid Lean theorems a great breakthrough. As AI-driven security threats grow, having the core Signal protocol rigorously verified with automated theorem proving gives us even greater confidence that our code delivers on its privacy guarantees.

The future of security

Achieving this long-standing challenge demonstrates how AI can bring elite security assurance to businesses, governments, and critical infrastructure, helping defend against agent-driven cyber threats.

Verifying Signal's core cryptography lays the groundwork to secure other vital systems, from medical device firmware to power grid software.

Scaling these techniques requires continued research. Paired with automated defense agents like CodeMender, formal verification can help counter the speed and scale of modern cyber threats to create software with mathematical proof that its protections work.

We are open-sourcing our formal verification artifacts for community use. Read the technical paper below.

• Formal verification artifacts: https://google-deepmind.github.io/code-verification
• Technical paper: https://deepmind.google/documents/36/Formal_Verification_of_Signal_4.pdf

Acknowledgements

This research was developed by Swarat Chaudhuri, Andrew Ferraiuolo, Anton Kovsharov, Tej Chajed, Sam Schlesinger, Karn Seth, Jonathan Katz, Charles Sutton, and Pushmeet Kohli.

We thank Eric Wieser for help with open-sourcing our code, Owen Jones for program management support, and Martín Abadi, Christopher Henson, Katerina Hristova, Henryk Michalewski, Jonathan Protzenko and George Tsoukalas for helpful discussions. We thank Signal's Rolfe Schmidt, Michael Rosenberg, and Ehren Kret for their feedback on our methodology. We also thank Tulsee Doshi, Four Flynn, Kate Olszewska, Alicia Huang, Andy Liu, Benoit Schillings, Raluca Ada Popa, Melvin Johnson, Koray Kavukcuoglu, Demis Hassabis, and Sundar Pichai for their support of the project.