DeepMind 称，其研究团队利用一套名为 AlphaProof Code 的多模型智能体框架，在 4 周内对 Signal 协议的实际代码完成了关键安全性质的形式化验证——而这类工作过去需要专家团队花费数年。形式化验证指的是用数学方法证明代码的运行完全符合预期、不存在缺陷，这是最高等级的安全保障手段。这是首次有人用任何方法（无论是否借助 AI）对如此广泛部署的协议的实现做到这一深度的形式化验证。

它解决什么问题

据 DeepMind 官方博客，加密协议支撑着几乎所有数字通信，从网上银行到网页浏览，单个缺陷就可能同时暴露数百万用户。专家们已花费数十年对协议进行形式化分析，但大多数验证工作止步于设计层面。现实中的漏洞往往藏在设计与实现之间的缝隙里——协议的数学模型可能是安全的，但把它翻译成真正运行在设备上的代码时，错误就可能悄然引入。要跨越这一鸿沟、直接证明编译后的代码满足安全性质，证明的复杂度会大幅上升，这正是传统方法耗时数年的原因。

它怎么做

DeepMind 称，AlphaProof Code 是一个多大语言模型（LLM）驱动的智能体框架，将形式化验证的工作按研究团队的分工方式拆解为几个阶段。

第一步，人类专家与多个模型协作，把 Signal 的安全目标翻译成形式化的数学规约（specification，即用数学语言精确描述代码应满足的性质），每一条规约都由人类专家逐一审核。

据 DeepMind 介绍，第二步，由 Gemini Carbon（DeepMind 最新模型）驱动的智能体执行证明工作，生成了超过六百万行 Lean 代码。Lean 是一种计算机语言，能够对代码的正确性进行数学级别的自动检查。

DeepMind 在博客中称，第三步，智能体对证明进行自审，标记出需要人类二次审查的部分——仅占代码库的约 1%。其余部分由 Lean 自动完成检查，使专家可以把精力集中在最需要人类判断的地方。

DeepMind 还描述了一项对照测试：研究人员将两个此前已修复的真实漏洞重新植入 Signal 代码的隔离版本中，AlphaProof Code 在两种情况下都生成了机器可检查的证明，表明含漏洞的版本是不安全的。

和以前的做法有何不同

传统做法要求研究人员手动开发证明来验证软件，耗时远超此次的 4 周周期。

Signal 首席技术官 Ehren Kret 在 DeepMind 博客中表示：”此前的形式化验证工作聚焦于代码中较小的部分，而 Google DeepMind 的方法使验证范围得以显著扩展。使用 AI 智能体将实际运行的代码翻译为有效的 Lean 定理，是一项重大突破。随着 AI 驱动的安全威胁不断增长，对 Signal 协议实现进行严格验证，给我们对代码兑现隐私承诺带来了更大信心。”

DeepMind 称，AlphaProof Code 的智能体不仅停留在协议的抽象设计层，而是深入到设备上实际运行的代码，证明编译后的代码满足关键安全性质，例如在设备被临时入侵前后仍能保持消息的保护。

目前的边界

据 ZDNet 报道，DeepMind 并未验证 Signal 的全部代码，而是针对专家指定的关键安全性质进行了验证。ZDNet 指出，这一工作是迈向更强安全验证基础设施的一步，但并非对整个应用的完整覆盖。

DeepMind 称，其形式化验证产物已开源供社区使用，但未透露将其作为消费级产品发布的计划。验证 Signal 核心加密技术为保护其他关键系统奠定了基础，从医疗设备固件到电网软件，但将这些技术规模化仍需持续研究。

主题分类：AI 安全/形式化验证

参考资料

  1. Introducing AlphaProof Code: a breakthrough in verifying complex software at depth — Google DeepMind, 2026-11-10
  2. Google’s new AI tool just proved Signal encryption really works – here’s how — ZDNet, 2026-11-10