DeepMind 用 AI 智能体完成 Signal 代码形式化安全证明

Rohan Paul (@rohanpaul_ai) · 2026-11-10 15

Google DeepMind 取得重大成就，证明了一个 AI 系统能够以数学方式证明软件是安全的，而且无需信任这个 AI 本身。

他们刚刚利用 AI 智能体以数学方式证明了 Signal 实际运行的代码能够保证消息的机密性。

Google 的 AI 智能体编写了 650 万行数学证明，证明 Signal 编译后的代码能够保证聊天内容的私密性。

验证的层级是处理器实际执行的指令级别。该实验室表示，此前从未有任何人针对任何广泛使用的协议做到这一点。

常规测试会尝试大量输入，并寄希望于命中那个有问题的输入。而证明则表明安全规则在所有情况下都成立，并且 Lean 证明检查器会拒绝 AI 写出的任何错误步骤。

真正的缺陷往往是在设计被转化为代码的过程中悄然引入的，因此检查处理器级别的代码可以弥合这一缺口。Rust 编译器同样不被信任，因此编译器犯下的错误也会被捕获。

这项工作耗时 4 周，而过去专家团队需要数年时间。由 40 到 80 个 Gemini Carbon 智能体组成的团队编写了约 650 万行 Lean 代码，而人类负责设定安全目标，并审查智能体标记出的那 1%。

为了检验该系统不会随意批准任何代码，研究人员将两个早已修复的 Signal 旧缺陷重新放回一份代码副本中。两次它都产出了经过机器检查的证明，表明该代码是不安全的。

更大的转变在于成本：既然 AI 能在数周内产出经过机器检查的证明，而非耗时数年的项目，这类验证将成为设备固件、电网软件及其他关键代码的常规检查。

↳ 引用 @pushmeet (Pushmeet Kohli)： 宣布我的团队 @GoogleDeepMind 取得的一项重大里程碑：我们证明了 Signal 消息协议底层机器代码的关键安全属性。这是首次有广泛部署的协议的实际生产代码被形式化验证——无论采用何种方法，无论是否借助 AI——且达到如此深度。

这不仅是研究突破，更是前沿 AI 如何成为力量倍增器、以应对现代网络威胁的速度与规模的绝佳范例。

形式化验证提供了更高标准的安全性；然而，它极其复杂且耗时，这也是许多情况下它被认为不切实际的原因。类似的工作可能需要团队数十年的合力才能完成。我们在一个月内就做到了。

借助 AlphaProof Code——Google DeepMind 全新的形式化验证智能体框架，运行于包括 Gemini Carbon 在内的 LLM 之上——我们将 Signal 协议验证到了设备上实际运行的代码层面。这一里程碑为未来奠定了基础：从医疗设备固件到电网软件等关键系统，都将附带其防护措施有效的数学证明。

要实现这一未来，需要我们社区持续的研究。本着这一精神，我们开源了形式化规范和验证产物，以便他人能在此基础上继续构建。

就个人而言，这一刻对我意义深远。二十多年前，我作为一名实习生开始了自己的研究之旅，从事复杂软件系统一致性检查的工作。看到这一宏大挑战在现代 AI 的助力下变得切实可行，实在非同寻常。

我为我的团队成员感到无比自豪：Swarat Chaudhuri、Andrew Ferraiuolo、Anton Kovsharov、Tej Chajed、Sam Schlesinger、Karn Seth、Jonathan Katz 和 Charles Sutton，他们承担了这一宏大挑战并交付了成果；也感谢 Signal 团队的合作。