DeepMind 推出 AlphaProof Code 多智能体验证框架，只用 4 周时间，AI 自动生成约 650 万行 Lean 证明代码，完成对 Signal 协议底层 libsignal 真机编译代码的数学形式化证明，确认 PQXDH 后量子握手、Triple Ratchet 棘轮机制满足前向保密、入侵后自愈、身份认证等核心安全特性，这次验证不是只检查纸上的协议设计，而是直接落地到设备上跑的真实机器码，过去这类深度形式化验证往往要专家团队耗费数年，这次靠 AI 把周期压缩到短短一个月，同时团队还做了对照测试，把两个已经修复的历史漏洞放回代码里，系统能准确识别出不安全，验证方案本身具备判别能力，但要说明，验证范围只覆盖加密核心模块，不等于整个 SignalAPP 完全没有任何安全风险。
项目核心信息清单
| 项目 | 详情 |
|---|---|
| 验证主体 | Signal libsignal 参考实现（AArch64 机器码） |
| 使用框架 | AlphaProof Code（Gemini Carbon 驱动 AI 智能体） |
| 证明代码总量 | 约 650 万行 Lean 证明代码，可信规范代码 2.6 万行 |
| 耗时 | 4 周，5 人研究团队配合 AI 智能体完成 |
| 验证模块 | PQXDH 后量子握手协议、Triple Ratchet 棘轮机制 |
| 验证安全属性 | 前向保密、入侵后安全、握手密钥保密、身份认证 |
| 人工复核范围 | 仅约 1% 证明内容需要人工审核，其余由 Lean 内核自动校验 |
| 测试对照 | 植入 2 个历史旧漏洞，系统可判定代码不安全 |
验证完整流程
- 定义规范：安全专家和 AI 一起，把 Signal 的安全目标翻译成 Lean 语言的数学规范，每一条规范都经过人工审核确认；
- AI 自动生成证明：多个 AI 证明智能体并行工作，针对真机机器码生成对应的 Lean 证明脚本；
- Lean 内核自动校验：证明全部交给 Lean 证明内核做机器核验，自动排除逻辑矛盾；
- 人工重点复核：AI 标记出高风险、需要人工判断的片段，只复核 1% 内容；
- 反向对照测试：把已知旧漏洞注入代码，验证系统能不能识别不安全状态，确认验证方法有效。
本次验证的边界与局限
- 只验证 libsignal 核心加密代码，不包含 Signal 整个 APP、群聊逻辑、密钥生成、侧信道攻击防护；
- 只针对 AArch64 架构编译版本，其他架构没有纳入本次证明；
- 形式化证明是满足预设安全规范，不代表可以抵御所有攻击方式；
- 底层依赖的操作系统、硬件、第三方库不在本次证明覆盖范围内。
行业意义
- 首次用 AI 完成主流大规模加密协议真机机器码级别的形式化验证，打通协议设计和真实运行代码之间的验证缺口；
- 大幅降低形式化验证成本，以前高成本、高门槛的安全验证，未来有机会用到更多通信、支付类加密软件；
- 给端到端加密通讯提供更强的数学安全背书，Signal 协议支撑 Signal、谷歌消息等数十亿用户的加密聊天。
【相关 FAQ】
问题 1：DeepMind 验证 Signal 真机代码，一共生成多少行证明、耗时多久？
回答 1：DeepMind 依靠 AlphaProof Code 框架，4 周时间生成约 650 万行 Lean 证明代码，完成 Signal 真机 libsignal 加密代码的形式化安全证明。
问题 2：DeepMind 这次证明 Signal 真机代码安全，都验证了哪些安全特性？
回答 2：DeepMind 针对 Signal 真机代码验证了 PQXDH 握手、Triple Ratchet 棘轮机制，证明满足前向保密、入侵后自愈、握手密钥保密、身份认证这些核心安全属性。
问题 3：DeepMind 证明 Signal 真机代码安全，是不是代表 Signal 软件完全不会被攻破？
回答 3：不是，DeepMind 只证明了 libsignal 核心加密模块的指定安全属性，Signal 真机代码之外的系统、硬件、侧信道、群聊模块不在本次证明范围，不能等同于整个 Signal 无漏洞。
问题 4：DeepMind 用什么工具完成 Signal 真机代码的形式化验证？
回答 4：DeepMind 自研 AlphaProof Code 多智能体框架，基于 Gemini Carbon 驱动 AI 智能体，搭配 Lean 证明语言与 Lean 内核，完成 Signal 真机机器码的数学安全证明。
【参考资料】
[2026-11-10]（Formal Verification of Signal’s Protocol with Gemini）DeepMind 官网
[2026-11-10]（AlphaProof Code: Verifying Signal’s Security at the Machine-Code Level）DeepMind 技术论文
[2026-11-10]（DeepMind AI agents formally verified Signal encryption code in four weeks）Wired
[2026-11-10]（DeepMind 4 周 600 万行证明，Signal 真机加密代码完成形式化验证）IT 之家
【免责声明】
本文内容仅为技术资讯整理，DeepMind 对 Signal 真机代码的形式化验证范围、安全边界、证明结论以 DeepMind 官方论文、项目仓库说明为准；形式化证明属于在指定模型下的数学验证，不代表产品在所有环境、所有攻击场景下绝对安全，本文不构成安全评估、产品选型的权威结论。