谷歌 DeepMind 推出 AlphaProof Code 多智能体框架，依靠 AI 智能体配合 Lean 证明器，完成了 Signal 协议 libsignal 参考实现的机器码层面形式化验证，这是业界首次用 AI 把广泛落地的加密协议从协议安全规范一直证明到编译后的实际运行代码，不再只停留在纸上模型验证；Signal 协议是全球主流端到端加密底层，Signal、WhatsApp、Google Messages 都在使用，这次验证重点覆盖 PQXDH 后量子握手、Triple Ratchet 棘轮机制，用数学方式证明前向保密、入侵后安全、身份认证这些核心安全属性成立，整个项目耗时大约四周，AI 产出 650 万行 Lean 证明代码，但是本次验证范围有限，不包含侧信道攻击、群聊、密钥生成全部逻辑，也不等于 Signal 整个 APP 全盘安全审计，这套方式算力成本很高，暂时没法快速批量套用在其他大量软件上，研究团队已经开放对应的规约与证明材料供外部复核。
一、项目基础信息
| 项目 | 详情 |
|---|---|
| 验证框架 | AlphaProof Code（Gemini Carbon 智能体 + Lean 证明内核） |
| 验证对象 | libsignal v0.105.4，AArch64 架构机器码 |
| 验证覆盖模块 | PQXDH 后量子握手协议、Triple Ratchet 棘轮协议 |
| 产出物 | 约 650 万行 Lean 机器可校验证明代码，2.6 万行基础规约与机器码语义定义 |
| 耗时 | 约 4 周 |
| 验证结论 | 目标模块满足：前向保密、身份认证、握手保密性、入侵后安全 |
| 排除范围 | 侧信道漏洞、群聊协议、完整密钥生成流程、上层应用逻辑 |
二、AlphaProof Code 验证流程
- 人工引导 AI 智能体，把 Signal 安全需求翻译成 Lean 形式化规约，由密码专家审核确认规约无误。
- 多 AI 证明智能体并行自动生成数学证明脚本，用来证明机器码满足前面的安全规约。
- Lean 内核独立校验全部证明，只有通过 Lean 校验的证明才会被采信，AI 生成内容不能直接说了算。
- 团队做对照测试，把带有已知历史漏洞的旧版本 libsignal 放入流程，系统成功判定不满足安全条件。
- 完成后公开全部规约与证明仓库，交给密码社区独立复查。
三、这项验证的价值亮点清单
- 打通设计和实现的鸿沟：传统形式化验证大多只验证纸上协议模型，很多漏洞藏在代码实现里，这次直接验证编译后的机器码。
- AI 大幅降低人力门槛：传统手工写这类密码学形式证明往往要数年专家工作量，这次四周完成核心部分。
- 面向后量子安全：验证的 PQXDH 握手是为抵抗量子计算机破解而设计的方案，对长期加密通信很关键。
- 可复现校验：证明交给 Lean 自动核验，不是黑盒 AI 结论，密码学者可以自行复核。
- 具备漏洞检出能力：对照测试中，历史已知漏洞版本会被这套验证体系拦截。
四、明显局限和误区提醒
- 不是 Signal APP 全盘安全证明，只验证了选定的密码协议模块，APP 的网络层、存储、UI 代码不在范围内。
- 不防御侧信道攻击，时序攻击、功耗攻击这类不在本次证明保障里。
- 算力消耗巨大，成本高昂，现阶段很难直接拿来给普通 APP、中小型密码库批量做验证。
- 证明是针对特定版本 libsignal、特定编译目标 AArch64，升级代码、换编译器、换 CPU 架构都要重新验证。
- 不能理解为 “Signal 再也不会出任何漏洞”，只是限定范围内的数学安全保证。
【相关 FAQ】
问题 1：谷歌 DeepMind 这次用 AI 完成的 Signal 协议安全验证，和普通漏洞扫描、渗透测试有什么区别？
回答 1：谷歌 DeepMind 对 Signal 协议做的是形式化验证，用数学证明满足安全属性，是穷尽条件下的证明；漏洞扫描、渗透测试只是找已经能触发的样本，没法证明不存在其他隐藏漏洞。
问题 2：谷歌 DeepMind AI 验证 Signal 协议之后，是不是 Signal 所有聊天功能都绝对安全无漏洞？
回答 2：不是，谷歌 DeepMind AI 只验证了 Signal 协议里 PQXDH 握手、Triple Ratchet 部分代码，群聊、侧信道、上层应用逻辑不在验证覆盖范围，不能保证 Signal 整体完全没有漏洞。
问题 3：AlphaProof Code 这套 AI 框架除了 Signal 协议，现在可以随便拿去验证别的加密程序吗？
回答 3：暂时不行，谷歌 DeepMind 的 AlphaProof Code 算力开销大，还需要密码专家人工编写、审核安全规约，成本很高，现阶段还属于研究原型，不适合大规模商用批量验证。
问题 4：Signal 协议被 DeepMind 的 AI 验证通过，代表 WhatsApp、Google Messages 对应的加密部分也自动被证明安全吗？
回答 4：仅代表对应 libsignal 核心密码实现满足本次限定的安全属性，WhatsApp、Google Messages 还有各自上层业务代码、配置、实现差异，不能直接等同于这些应用整体安全。
【参考资料】
[2026-11-10]（Introducing AlphaProof Code，用 AI 完成 Signal 协议形式化验证）Google DeepMind 官网博客
[2026-11-10]（AlphaProof Code: Verifying Signal’s Security at the Machine-Code Level）google-deepmind.github.io
[2026-11-10]（谷歌 DeepMind 用 AI 完成 Signal 协议形式化验证，数学证明其端到端加密可靠性）新浪科技
[2026-11-10]（AI 参与写证明 谷歌 DeepMind 完成 Signal 协议形式化验证）ZAKER 新闻
【免责声明】
以上谷歌 DeepMind Signal 协议 AI 安全验证内容仅为技术科普，不构成安全担保；本次验证有明确版本、架构、模块边界限制，证明结果不覆盖侧信道、上层应用、群聊等内容；形式化证明不等于绝对无漏洞，通信安全还受密钥管理、设备环境、版本更新影响；项目属于研究成果，AlphaProof Code 框架能力、算力成本、适用范围以 DeepMind 官方论文与仓库说明为准。