Google DeepMind于11月10日宣布，其AI智能体已从数学层面证明Signal加密背后的代码实现了主要安全承诺。与此同时，该实验室发布了名为AlphaProof Code的新框架及相关技术论文。
Signal协议支撑着Signal、WhatsApp、Messenger和Google Messages等应用的聊天加密。DeepMind研究人员对libsignal（Signal加密的开源库）进行了审查，验证范围一直延伸至设备上运行的机器码。DeepMind在博客文章中称，这是业界首次通过任何手段——无论是否借助AI——对如此广泛使用的协议代码进行形式化验证。
Signal首席技术官Ehren Kret表示：“随着AI驱动的安全威胁日益增长，利用自动化定理证明对核心Signal协议进行严格验证，让我们更有信心确信代码能够兑现隐私保证。”
AI智能体如何执行验证
形式化验证利用数学方法证明软件按预期工作，旨在排除整类漏洞而非逐个查找。此前，这类工作往往缓慢且昂贵，例如验证seL4微内核曾耗费20个人年。
AlphaProof Code将任务拆解：人类专家选择待证明内容，AI智能体协助将Signal的安全目标转化为形式化规范，并经人类逐一审核。随后，由40至80个智能体组成的团队在Gemini 4 Carbon上运行，使用用于机器检查数学的语言Lean编写证明过程。
在四周内，智能体为五人研究团队生成了约650万行证明代码。论文指出，没有任何作者手动编写证明代码。运行在Gemini 4 Carbon和Anthropic Claude Opus 5.5上的智能体负责起草并审核规范。
这些证明覆盖了Signal的后量子握手及其三重棘轮（Triple Ratchet）机制，后者为每条消息提供新鲜密钥。验证结果展示了前向保密性（即即使手机密钥后续被盗，旧消息依然安全），以及身份验证和后妥协安全性（协议在被破坏后的恢复能力）。
为测试该方法，团队将两个Signal已修复的libsignal旧漏洞重新植入代码。系统成功证明包含漏洞的代码不安全。媒体报道指出，系统在检查部分中未发现新缺陷。
验证范围的局限
此次保证的范围窄于“Signal整体是安全的”。论文仅涵盖研究人员自行构建库中的一对一聊天，而非Signal应用程序本身；群聊验证留待未来，且未验证密钥生成。此外，证明假设底层密码例程按规范工作。
论文指出，当前证明并未展示Signal最新棘轮层旨在添加的后量子恢复能力。成本方面，Google拒绝透露项目费用，也未说明是否计划推出商业验证产品。
DeepMind研究科学家Swarat Chaudhuri表示：“我们对结果感到兴奋，但在将其扩展到全球所有软件之前，仍有长路要走。”他进一步指出，当前的难点不在于检查本身，而在于决定检查什么，“下一个前沿领域不会是证明，而是规范。”
这项工作朝着“Signal Shot”挑战迈出了一步。今年4月，有益人工智能基金会、Signal和Lean FRO设立该挑战，旨在用Lean验证Signal协议和应用。DeepMind已在GitHub发布其规范和证明供公众审查。此外，Google本周已向付费开发者开放Gemini 4 Carbon。