推出 AlphaProof Code：深度验证复杂软件的重大突破
本文目录
2026 年 11 月 10 日 研究
作者：Pushmeet Kohli 与 Swarat Chaudhuri
阅读技术论文
Google DeepMind 研究人员如何构建新的智能体框架，对 Signal 加密协议的代码进行形式化验证——这长期以来被视为一项重大安全挑战
今天，我们分享软件安全领域一个长期被视为重大挑战的里程碑：Google DeepMind 研究人员引导 AI 智能体，用数学方法证明了 Signal 协议底层实际代码的关键安全属性；Signal 协议是保护 Signal 和 Google Messages 等应用中数十亿私密对话的技术。
这一突破性发现使用了 AlphaProof Code——一个用于史无前例深度形式化验证的新型智能体框架，它将人类专业知识与 AI 智能体结合起来。形式化验证（formal verification）——用数学证明代码正确运行、没有缺陷——是最高标准的安全保证；然而它很困难，而且往往劳动密集。
我们的工作标志着 AI 首次被用于在这种深度上形式化验证一个广泛部署的加密协议。这也是一个广泛部署协议的实现首次被任何方法（无论是否使用 AI）形式化验证。
我们如何验证 Signal#
AlphaProof Code 是一个多 LLM 智能体框架，它像研究团队那样拆分形式化验证工作：人类专家与 AI 合作决定要证明什么，然后由一组 AI 智能体完成。
首先，我们的研究人员与混合模型合作，把 Signal 的安全目标转化为形式化数学规格，并由人类专家逐一审查。随后，由 Gemini Carbon 驱动的智能体完成证明，生成了超过 600 万行 Lean 代码——Lean 是一种用数学方法证明代码准确性的计算机语言。
接下来，智能体审计证明，并标出需要人类二次查看的区域——仅占代码库的百分之一，大幅节省时间。由于 Lean 会自动检查其余部分，我们的专家可以把审查集中在人类判断最重要的地方。
加密协议支撑着几乎所有数字通信，从网上银行到网页浏览，一个缺陷就可能同时暴露数百万人。这就是专家们花费数十年对其进行形式化分析的原因。
但大多数协议验证止步于设计层面。我们的智能体更进一步，证明编译后的代码满足关键安全属性——例如在设备暂时被攻破前后保持消息受保护——一直深入到设备上运行的确切代码。由于真实世界漏洞往往隐藏在设计实现之间的差距中，弥合这一差距使这些证明复杂得多。
即使在这种复杂度下，我们的验证过程也只用了四周——这项任务历来需要专家团队花费数年——证明 Signal 的核心加密代码提供了我们专家指定的安全保护。
为了确认 AlphaProof Code 能区分正确代码和有缺陷代码，我们在 Signal 代码的隔离版本中重新引入了两个真实存在、此前已修复的缺陷。在这两种情况下，系统都生成了机器检查的证明，表明有缺陷版本不安全。
在 AlphaProof Code 中，AI 智能体帮助用户编写规格，然后自主证明实现满足规格。每个证明都由 Lean 检查，以验证智能体的工作。
“此前的形式化验证工作必然聚焦于较小的范围，而这种新方法实现了显著扩展。传统上，要验证生产代码严格匹配其加密设计需要大量人工工作，因此使用 AI 智能体自动把实际代码转化为有效的 Lean 定理是一项重大突破。随着 AI 驱动的安全威胁增长，用自动定理证明严格验证 Signal 核心协议，让我们更有信心代码兑现了隐私保证。” —— Ehren Kret，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 对本项目的支持。