Google DeepMind 11 月 10 日发布 AlphaProof Code，并用它证明了 Signal 协议参考实现 libsignal 的关键安全性质。证明对准用标准 rustc 1.98.1 编译、再与 musl 静态链接得到的 AArch64 机器码。技术报告写明，验证对象是未经改写的 libsignal v0.105.4 和 SPQR v1.6.0，外加一个只做收发封装的命令行工具 libsignal-cli。
团队把这项工作放在一个很具体的对比里：以往对 Signal 的形式化分析，多半停在抽象协议模型、为验证改写的实现，或更窄的性质；seL4 微内核花了二十人年，CompCert 编译器花了六年，而且源码本身就是为验证写的。DeepMind 在博客里称，这是首次把广泛部署的密码协议实现做到这一深度的形式化验证，也是首次用任何方法完成这类实现的验证。这是团队自己的判断，依据是上述对照，而不是第三方复审。
人先审定要证明什么，智能体再写证明
AlphaProof Code 把工作拆成两边。一边是规格：研究人员和模型一起，把文献里的安全目标改写成 Lean 定理和定义，审阅代理提出意见，最后由人批准。另一边是证明：一旦规格被钉下来，一队自动证明代理去写证明，只有 Lean 内核检查通过、并且比对工具确认定理语句与批准版本完全一致，才算完成。
博客写明，写证明的代理由 Gemini Carbon 驱动，生成了超过 600 万行 Lean。技术报告给的更细：约 650 万行经内核检查的证明，建立在仓库里约 1.8 万行需要阅读和信任的规格，再加上约 8000 行 AArch64 语义。博客还说，代理会标出大约 1% 的代码请人再看，其余由 Lean 自动检查。报告把人的时间主要花在“证明什么、假设是否过强”上，而不是逐行检查那几百万行证明。
时间口径要分开看。博客说全过程约四周，并把它和“历史上专家团队往往要数年”放在一起；技术报告写的是五人小组并行做了四周，各自在工作站上持续运行代理。四周是这次实验的日程，数年是团队对传统验证成本的对照，不是同一套工时统计。
两套模型各证明了什么
报告在两套标准模型里陈述结果。符号模型把底层密码原语理想化，证明每一次无碰撞的执行都满足一组性质，包括消息密钥的前向保密和设备失窃后的保密、握手认证，以及即便未来的量子攻击者后来打破了 Diffie-Hellman，握手密钥仍然保密。计算模型则给出经典攻击者优势的具体上界，把攻破协议的难度归约到 Gap-DH、签名不可伪造等假设；这一套不覆盖量子攻击者。
覆盖范围是一对一会话里的 PQXDH 握手和 Triple Ratchet。报告写明，该协议的变体还部署在 WhatsApp、Messenger 和 Google Messages 里，但这些产品并不在本次定理中。群聊被明确留作后续工作。底层哈希、密钥派生、加密和签名等例程以合同方式接入，它们的安全性本身没有被证明。符号侧对棘轮的定理还允许攻击者选择 SPQR 的密钥，因此它们说明的是 Triple Ratchet 不弱于 Double Ratchet，而不是 SPQR 所增加的后量子愈合。
为了检查规格会不会写成“怎么都成立”的弱定理，团队把两个此前已修复的 libsignal 漏洞重新注入隔离版本并重新编译。一个是把未确认会话状态存下来，从而留下签名预密钥的副本；一个是未检查发起方的 X25519 基密钥是否避开了小阶子群、编码是否在合法范围。报告称，对这两个带漏洞的二进制，他们完成了 Lean 证明：符号安全定理在这两份代码上不成立。
这些定理管不到整套 Signal 应用
定理针对的是团队自己编译的 libsignal-cli，在固定的内存、系统调用和挂钩合同下运行。报告写明，Android 和 iOS 上的 Signal 应用使用同一份 Rust 代码，但编译选项、链接方式和操作系统接口不同；只有当这些环境保持协议代码在本次实验中被行使的行为时，定理才能迁过去。计算模型的上界在会话规模变大时会变得没有意义：如果几乎每条消息都开启新的密钥世代，单会话大约 2.5 万条消息时，统计项就会把保证抽空。
Signal 首席技术官 Ehren Kret 在博客中说，以往的形式化验证往往只能覆盖更小的代码范围，用智能体把正在运行的代码转成有效的 Lean 定理是一项重要突破；在人工智能驱动的安全威胁上升时，严格验证 Signal 协议实现，让他们对代码的隐私保证更有信心。这句话评价的是方法，并没有扩大验证范围。
Lean 工件已经公开。读者现在可以核对的是：一份未改写的参考实现，在一对一会话和一组写明的假设下，被机器检查过。还不能从这里推出，手机里的 Signal、群聊，或那些被合同替换掉的底层原语，已经得到同样的保证。
