2026 年 11 月 10 日，Google DeepMind 在官网介绍了 AlphaProof Code。这是一个把人类专家与 AI agent 结合起来、用于形式化验证的框架，不是新的聊天模型上架。

研究人员用它证明了 libsignal（Signal 协议参考实现）的选定关键安全性质，并把证明做到编译后的机器码／AArch64 层面。官网博文把所涉技术写成保护 Signal 与 Google Messages 中海量私密对话的技术。论文写明，结果针对本次 libsignal-cli 构建，不是 Signal 自家应用。

论文与产物页写，agents 生成了约 650 万行经机器检查的 Lean 证明代码；官网博文正文则写超过六百万行 Lean。

论文写，证明覆盖 Signal 的后量子 PQXDH 握手与 Triple Ratchet，并建立前向保密、认证、失陷后安全与握手保密。论文把这些结果表述为：把协议层安全保证连接到广泛使用的密码协议实现之未修改代码的首次证明。

证明由 Gemini Carbon（论文作 Gemini 4 Carbon）驱动的 agent 完成。规格由人类与模型协作起草，并由人类专家逐条审阅。论文还写，规格阶段使用了 Claude Opus 5.5，但证明是由 Gemini 4 Carbon 的 agent 团队写出的，作者没有手写证明代码。该模型的既有介绍发布于 2026 年 10 月 28 日；这并不构成 Carbon 的新一次 API 或价表发布。证明所用模型的既有介绍（不是今天发布）见：Google 发布 Gemini 4 Carbon：下一代前沿模型。

官网博文写，验证过程用了四周；论文补充为五人团队用四周完成证明工作。

官网把「首次」限定为：AI 首次在这一深度对广泛部署的密码协议做形式化验证；也是像这样广泛部署的协议实现首次被任何方法（无论是否使用 AI）形式化验证。这不是声称整个 Signal 应用，或全部可能的失败模式，都已得到验证。

为确认该框架能区分正确代码与有缺陷的代码，研究人员把两个此前已修复的真实漏洞再引入隔离版本。两种情况下，系统都给出了「有漏洞版本不安全」的机器检查证明。这是回归测试，不是发现 Signal 的新漏洞。

Signal 首席技术官 Ehren Kret 在官网博文中表示：「此前的形式化验证主要针对代码中较小的部分，Google DeepMind 的方法使范围得以显著扩展。用 AI agent 把实际运行的代码翻译成有效的 Lean 定理，是一项重大突破。随着 AI 驱动的安全威胁增加，严格验证 Signal 协议实现，让我们对其代码的隐私保证更有信心。」

验证产物与技术论文已公开。