DeepMind 形式化验证 Signal 加密协议：650 万行证明

发生了什么

DeepMind 11 月 10 日在官方博客发布 AlphaProof Code：一个多 LLM 智能体框架，把人类专家的形式化验证经验与 AI 智能体结合，验证对象是 Signal 加密协议 libsignal 的实际编译代码，而非设计文档。DeepMind 称，这是首次由 AI 在此深度形式化验证已广泛部署的加密协议，也是首次以任何方法形式化验证此类协议的实现。

验证覆盖 libsignal v0.105.4 与 SPQR v1.6.0，用标准 rustc 编译成单一 AArch64 Linux 可执行文件，在命令行环境运行；覆盖后量子 PQXDH 握手与三重棘轮，证明的性质包括前向保密、事后泄露安全、发起方与响应方保密、认证与握手保密，共 10 条符号定理。验证只覆盖一对一会话，不含群聊、服务器、密钥生成与手机系统；底层密码原语假定成立，未予证明。

智能体由 Gemini Carbon 驱动，四周写出约 650 万行机器核查的 Lean 证明（博客正文称逾 600 万行），过去同类工作需专家团队数年；智能体审计后约 1% 代码交人工复核，其余由 Lean 内核核查；可信基约 2.6 万行。验证方法包括把两个已修复的 libsignal 漏洞重新引入隔离副本，系统两次都给出机器核查的“不安全”证明。相关产物已开源，技术论文已发布；Signal 首席技术官埃伦·克雷特在博客中称其为重大突破。

关键事实

1. 系统：AlphaProof Code：多 LLM 智能体框架，结合人类专家与 AI 智能体，验证实际编译代码而非设计文档
2. 对象：libsignal v0.105.4 与 SPQR v1.6.0，标准 rustc 编译的 AArch64 可执行文件；覆盖后量子 PQXDH 握手与三重棘轮
3. 规模：约 650 万行机器核查的 Lean 证明，四周完成；过去同类工作需专家团队数年
4. 复核：智能体审计后约 1% 代码交人工复核，其余由 Lean 内核核查；可信基约 2.6 万行
5. 验证方法：把两个已修复的 libsignal 漏洞重新引入隔离副本，系统两次都给出机器核查的“不安全”证明
6. 范围：只覆盖一对一会话；不含群聊、服务器、密钥生成与手机系统；底层密码原语假定成立，未予证明