# DeepMind用AI形式化验证Signal加密代码

> AlphaProof Code用四周证明了Signal的核心安全属性，这是AI首次对广泛使用的协议进行形式化验证。

Oossa · 2026-11-10 · https://oossa.com/zh/deepmind-uses-ai-to-formally-verify-signal-s-cryptographic-code

事件日期: 2026-11-10

Google DeepMind于2026年11月10日宣布，其新AI框架AlphaProof Code已用于对Signal协议的实际代码进行形式化验证。形式化验证是通过数学证明，确认软件严格按照预期运行，不存在隐藏漏洞。研究团队引导AI代理生成并检查证明，验证编译后的Signal代码能够实现关键安全保障，例如即使设备暂时遭到入侵，也能保护消息安全。整个过程耗时四周，而通常这类工作需要专家团队花费数年。

## AlphaProof Code的工作原理

AlphaProof Code是一套由多个大语言模型（LLM）驱动的智能体系统。人类研究人员先将Signal的安全目标转化为形式化规约，并逐步审核。随后，由DeepMind的Gemini Carbon模型驱动的一组智能体用Lean语言编写证明；Lean可用于检验数学定理。智能体生成了超过六百万行Lean代码，并将代码库中仅约1%的部分标记出来供人工审核。系统还在两个此前已修复的漏洞被重新引入时，正确识别出它们，表明它能区分安全代码与存在漏洞的代码。

## 这为何重要

此次验证针对的是编译后的实际实现，而不只是设计，从而弥补了一个缺口——许多现实中的漏洞正藏身于此。Signal首席技术官Ehren Kret表示，这一成果让团队“对代码的隐私保障更有信心”。专家认为，这是利用AI为银行、医疗设备、电网软件及其他关键系统提供高水平安全保障的一步。

## 事实

- DeepMind于2026年11月10日发布AlphaProof Code。
- AI代理生成了超过六百万行Lean代码。
- 人工审核人员只需检查Signal代码库中约1%的内容。
- 验证过程耗时四周，而人工完成通常需要数年。
- 两个已知漏洞被重新引入后，AlphaProof Code生成了证明，表明存在漏洞的版本并不安全。

## 为什么重要

对日常用户而言，这项工作意味着，保护Signal和Google Messages中数十亿条消息的加密机制已在实现层面经过数学验证，从而降低了隐藏缺陷的风险。对开发者而言，这展示了一条切实可行的路径：借助AI辅助形式化验证，加快安全审查；不过，这种方法能否大规模推广以及相关成本仍不明朗。

## 来源与参考

1. [Introducing AlphaProof Code: a breakthrough in verifying complex software at depth](https://deepmind.google/blog/introducing-alphaproof-code/) – Google DeepMind, 2026-11-10
2. [A New AI Tool From Google DeepMind Proved the Signal Protocol Is Secure](https://www.wired.com/story/a-new-ai-tool-from-google-deepmind-formally-verified-the-signal-protocol/) – WIRED, 2026-11-10

最后更新: 2026-11-10