Google DeepMind 于 2026 年 11 月 10 日公布 AlphaProof Code，称研究人员借助这一 AI agent 框架，用数学方法证明了 Signal 协议实际代码的关键安全属性。该协议用于保护 Signal、Google Messages 等应用中的私密对话。此次工作的关注点是将验证从协议设计推进到设备上实际运行的代码，验证其是否满足专家指定的安全要求。
据 DeepMind 介绍，AlphaProof Code 是一个多大语言模型 agent 框架：人类专家与 AI 共同决定要证明什么，再由一组 AI agent 完成证明。其采用的形式化验证，是通过数学证明检查代码是否符合规定要求的方法。
研究人员首先与多个模型合作，把 Signal 的安全目标转化为形式化数学规范，每一条规范都经过人类专家审核。随后，由 Gemini Carbon 驱动的 agent 编写证明。据发布方披露，这一步生成了超过 600 万行 Lean 代码，每个证明都由 Lean 自动检查。
agent 还会审计证明，标出需要人类再次检查的部分。DeepMind 称，这些部分仅占代码库的 1%，专家因此可以集中审核需要人类判断的内容。
DeepMind 在博文中指出，多数协议验证止步于设计层面，而实际漏洞往往藏在设计与实现之间。此次 agent 验证的是编译后的代码是否满足关键安全属性，并深入到设备实际运行的代码。例如，设备被临时攻破前后的消息仍受到保护，就是此次验证涉及的安全属性之一。
据发布方披露，整个验证过程用了 4 周；DeepMind 表示，这类任务以往需要专家团队耗费数年。该结果对应的是 Signal 核心密码代码是否实现了专家所指定的安全保护。
为确认 AlphaProof Code 能区分正确代码与存在漏洞的代码，研究人员将两个此前已修复的真实漏洞，重新植入一个隔离版本的 Signal 代码。DeepMind 称，在这两种情况下，系统都生成了经过机器检查的证明，表明带有漏洞的版本不安全。
DeepMind 将这项工作称为首次借助 AI，以这一深度形式化验证广泛部署的密码协议；同时称，无论是否使用 AI，此类协议的实现此前也未被任何方法验证到这一深度。这两项「首次」均为发布方自己的表述。
DeepMind 已宣布开源相关形式化验证成果，并提供技术论文供进一步查阅。博文同时指出，要扩大这些技术的应用规模，仍需要继续研究。
