Google DeepMind 发布 AlphaProof Code，形式化验证 Signal 密码协议实际代码

2026年11月10日研究

Pushmeet Kohli 和 Swarat Chaudhuri

Google DeepMind 研究人员如何构建一个全新的智能体框架，对 Signal 加密协议的代码——长期以来被视为一项重大安全挑战——进行了形式化验证

今天，我们分享软件安全领域的一个里程碑，它长期以来被视为一项重大安全挑战：Google DeepMind 研究人员引导 AI 智能体对 Signal 协议的实际底层代码进行了数学证明，验证了其关键安全属性。Signal 协议是在 Signal 和 Google Messages 等应用中保护数十亿条私密对话的技术。

这一突破性发现使用了 AlphaProof Code，这是一个前所未有的深度形式化验证智能体框架，将人类专业知识与 AI 智能体相结合。形式化验证——通过数学方法证明代码正确无误地运行——是安全保障的最高标准；然而，它非常困难，且往往耗费大量人力。

我们的工作标志着 AI 首次在这一深度上对一个广泛部署的加密协议进行形式化验证。这也是此类广泛部署的协议的实现首次通过任何方法（无论是否使用 AI）得到形式化验证。

我们如何验证 Signal

AlphaProof Code 是一个多 LLM 智能体框架，它像研究团队那样分工进行形式化验证工作：人类专家与 AI 共同决定要证明什么，然后由一组 AI 智能体来完成。

首先，我们的研究人员与多种模型协作，将 Signal 的安全目标转化为形式化的数学规范，并由人类专家逐一审查。随后，由 Gemini Carbon 驱动的智能体完成了证明，生成了超过 600 万行 Lean 代码。Lean 是一种通过数学方式证明代码正确性的计算机语言。

接着，智能体对证明进行了审计，并标出了需要人类再次审视的部分——仅占代码库的百分之一，这极大地节省了时间。由于 Lean 会自动检查其余部分，我们的专家可以把审查精力集中在人类判断最重要的地方。

加密协议支撑着几乎所有的数字通信，从网上银行到网页浏览，一个漏洞就可能一次性让数百万人暴露于风险之中。这就是为什么专家们数十年来一直对它们进行形式化分析。

但大多数协议验证都停留在设计层面。我们的智能体走得更远，证明编译后的代码满足关键安全属性——例如在设备被暂时入侵前后保持消息受保护——一直验证到设备上运行的确切代码。由于现实世界的漏洞往往隐藏在设计与实现之间的缝隙中，弥合这一鸿沟使这些证明的复杂度大幅增加。

即便如此复杂，我们的验证过程只用了四周——而这类任务历来需要专家团队耗费数年——证明了 Signal 的核心加密代码确实提供了我们专家所指定的安全保护。

为了确认 AlphaProof Code 能够区分正确代码与有缺陷的代码，我们将两个真实的、此前已修复的漏洞重新引入 Signal 代码的一个隔离版本中。在这两种情况下，系统都生成了机器验证的证明，表明含有缺陷的版本是不安全的。

虽然此前的形式化验证工作必然只能聚焦于较小的范围，但这一新方法实现了显著的扩展。传统上，验证生产代码是否严格符合其密码学设计需要大量的手工工作，因此利用 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 对该项目的支持。