原标题：Introducing AlphaProof Code: a breakthrough in verifying complex software at depth
Google DeepMind 发布 AlphaProof Code，一个多 LLM 智能体形式化验证框架，数学化证明了 Signal 协议实际代码的关键安全属性。Agent 由 Gemini Carbon 驱动，生成超过六百万行 Lean 证明，仅 1% 代码需人工复查，全程用时四周；团队还向隔离版本中重新引入两个已修复的真实 Bug，系统均证明其不安全。官方称这是首次对广泛部署的密码协议实现进行形式化验证，并将开源验证工件。
原文给出了从规格到 Lean 证明的完整验证流程、四周期限和 Bug 复现检验，可帮助读者评估 AI 形式化验证的适用边界。
本页的摘要、推荐理由与解读出自 AIsa Studio 的 AI 风向智能体，原文版权归原作者所有。
Google DeepMind 于 2026 年 11 月 10 日发布 AlphaProof Code，这是一个结合人类专家与 AI 智能体的形式化验证框架。研究人员用它在数学层面证明了 Signal 协议实际代码的关键安全属性——Signal 协议是保护 Signal 与 Google Messages 等应用中数十亿条私人对话的技术。官方称这一工作「long considered to be a grand security challenge」。
密码学协议支撑几乎所有数字通信，从网上银行到网页浏览，单一缺陷可能同时暴露数百万人。传统的生产级代码与密码学设计严格匹配的验证需要大量人工，此前形式化验证工作往往只能覆盖较小范围；用 AI 智能体自动把实际代码翻译成有效的 Lean 定理，使验证范围显著扩展。在 AI 驱动的安全威胁增长的背景下，对核心协议的严格验证为隐私承诺提供了更强的依据。DeepMind 还指出，该技术与 CodeMender 等自动防御智能体配合，可用于应对现代网络威胁的速度与规模，并为医疗设备固件、电网软件等其他关键系统铺路。
直接受益者是 Signal 与 Google Messages 的用户——其底层核心密码代码的隐私保证现在有了数学证明。更广层面，企业、政府和关键基础设施运营方可能借助这类方法获得此前昂贵的「精英级」安全保证；安全研究者与形式化验证社区则获得了开源的验证工件与技术论文。
2026年11月10日 研究
普什米特·科利（Pushmeet Kohli）和斯瓦拉特·乔杜里（Swarat Chaudhuri）
Google DeepMind 研究人员如何构建一个新的智能体框架，对 Signal 加密协议的代码进行形式化验证——这长期以来被视为一项重大的安全挑战
今天，我们分享了一项在软件安全领域长期被视为重大挑战的里程碑式成果：Google DeepMind 的研究人员引导 AI 智能体对 Signal 协议底层实际代码的关键安全属性进行了数学证明。Signal 是保护 Signal 和 Google Messages 等应用中数十亿次私密对话的技术。
这一突破性发现是利用 AlphaProof Code 完成的，这是一个新颖的智能体框架，用于以前所未有的深度进行形式化验证，结合了人类专家与 AI 智能体的优势。形式化验证——即通过数学方法证明代码运行正确且无缺陷——是最高级别的安全保障标准；然而，它既困难又往往耗时费力。
我们的工作首次利用 AI 以这种深度对广泛部署的加密协议进行了形式化验证。这也是首次通过任何方法（无论是否使用 AI）对像这样广泛部署的协议的实现进行形式化验证。
AlphaProof Code 是一个多大型语言模型（LLM）智能体框架，它将形式化验证的工作拆分得像一支研究团队那样运作：人类专家与 AI 合作决定 要证明什么，而一组 AI 智能体负责执行证明。
首先，我们的研究人员与多种模型协作，将 Signal 的安全目标转化为正式数学规范，并由人类专家逐一审查。在此基础上，由 Gemini Carbon 驱动的智能体执行证明工作，生成了超过六百万行的 Lean 代码。Lean 是一种计算机语言，用于从数学上证明代码的准确性。
接下来，智能体会审计这些证明，并标出需要人类再次审视的区域——仅占整个代码库的百分之一，极大地节省了时间。由于 Lean 会自动检查其余部分，我们的专家可以将精力集中在最需要人类判断力的地方。
加密协议支撑着几乎所有的数字通信，从在线银行到网页浏览，一个漏洞就可能同时暴露数百万人的信息。这就是为什么专家们花费数十年时间对其进行形式化分析的原因。
但大多数协议验证仅停留在设计层面。我们的智能体更进一步，证明了编译后的代码能够满足关键的安全属性——例如，在设备暂时被攻破前后保持消息受保护——直至设备运行的确切代码。由于现实世界中的漏洞往往隐藏在设计与实际实现之间的差距中，弥合这一差距使得这些证明变得极其复杂。
即便面对如此高的复杂度，我们的验证过程仅用了四周时间——而历史上这需要专家团队花费数年——这证明了 Signal 的核心加密代码确实提供了我们专家所指定的安全保护。
为了确认 AlphaProof Code 能够区分正确代码和有缺陷的代码，我们将两个真实存在、此前已修复的漏洞重新引入到一个隔离版本的 Signal 代码中。在这两种情况下，系统都生成了一个由机器检查的证明，表明有缺陷的版本是不安全的。
在 AlphaProof Code 中，AI 智能体帮助用户编写规范，然后自主证明实现符合该规范。每个证明都由 Lean 进行检查，以验证智能体的工作。
虽然之前的形式化验证工作必然聚焦于较小的范围，但这种新方法实现了显著的扩展。传统上，验证生产代码是否严格匹配其加密设计需要大量人工努力，因此利用 AI 智能体自动将实时代码转换为有效的 Lean 定理是一个巨大的突破。随着基于 AI 的安全威胁日益增长，对核心 Signal 协议进行严格的自动化定理证明验证，使我们对其代码兑现隐私保证的信心更加增强。
实现这一长期存在的挑战展示了 AI 如何将精英级的安全保障带给企业、政府和关键基础设施，帮助抵御由智能体驱动的网络安全威胁。
验证 Signal 的核心密码学为保护其他重要系统奠定了基础，从医疗设备固件到电网软件。
扩展这些技术需要持续的研究。结合如 CodeMender 这样的自动化防御智能体，形式化验证可以帮助应对现代网络威胁的速度和规模，从而创建具有数学证明其保护机制有效的软件。
我们正在开源我们的 形式化验证工件 供社区使用。请阅读下方的技术论文。
本研究由 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 对该项目的支持。
November 10, 2026 Research
Pushmeet Kohli and Swarat Chaudhuri
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.
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 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.
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.
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.
原文版权归 Google DeepMind 及原作者所有，本站转载仅供阅读。如需删除，请联系 support@aisa.one。
2026-11-10，Google DeepMind 发布 AlphaProof Code，一个由 Gemini Carbon 驱动的多 LLM 智能体形式化验证框架，宣布首次对 Signal 协议的实际生产代码完成关键安全属性的数学证明。官方称智能体生成了超过六百万行 Lean 证明代码，约 1% 代码需人工复核，整个项目耗时四周（DeepMind 博客称'一个月内完成'）。团队还向隔离版本中重新引入两个已修复的真实漏洞，系统均给出机器检查的不安全证明；报道 6 称系统'立即发现两个刻意植入的测试 bug'，与报道 1、2 的表述（重新引入已修复的真实 Bug 后证明其不安全）略有出入。验证规范与工件已开源。Ars Technica（11-11）指出，这项工作独立验证了 Signal 应用、Google Messages 和 WhatsApp 等平台所依赖的加密技术，Signal 系统每天保护数十亿条私人消息；但 AI 辅助形式化验证能否大规模用于保障大量代码安全仍不明确。The Decoder 报道称 DeepMind 计划通过 CodeMender 等系统将该方法扩展到电网和医疗设备领域。
Studio