推出 AlphaProof Code：深度验证复杂软件的一项突破

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 驱动的智能体完成证明，生成了超过六百万行 Lean 代码。Lean 是一种能从数学上证明代码正确性的计算机语言。

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

加密协议几乎支撑着所有数字通信，从网上银行到网页浏览，一个缺陷就可能同时让数百万人暴露在风险之下。正因如此，专家们几十年来一直在对它们做形式化分析。

但大多数协议验证都停留在设计层面。我们的智能体更进一步，证明了编译后的代码满足关键安全属性——例如在设备被临时攻破之前和之后都能保护消息——一直验证到设备上实际运行的代码。由于真实世界的漏洞往往藏在设计和实现之间的缝隙里，跨越这道缝隙让证明变得复杂得多。

即使复杂度这么高，我们的验证过程也只用了四周——这类任务过去需要专家团队花上数年——证明了 Signal 的核心加密代码确实提供了我们的专家所规定的安全保护。

为了确认 AlphaProof Code 能区分正确代码和有缺陷的代码，我们把两个真实存在、此前已修复的 bug 重新引入到一个隔离版本的 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 对本项目的支持。