谷歌 DeepMind 依靠自研多智能体框架 AlphaProof Code，让 AI 参与撰写数学证明，完成了 Signal 加密协议 libsignal 参考实现的形式化验证，这次验证不再只停留在纸面协议模型，直接对编译后的 AArch64 机器码做数学证明，AI 一共产出大约 650 万行 Lean 证明代码，整个项目只用四周就跑完，而传统人工形式化验证同等规模的密码协议，往往需要专家团队耗费数年时间；验证范围覆盖后量子 PQXDH 握手、Triple Ratchet 棘轮机制，确认前向保密、身份认证、遭入侵后安全、握手保密性这几项核心安全属性，也是业内首次把广泛商用密码协议的安全保证，和未经修改的实际落地代码打通绑定，这套方案由人类专家把控安全规范，Gemini Carbon 驱动的证明智能体承担证明生成、自查筛选，最后只留下大约 1% 的内容交给人工复审，大幅压低形式化验证的门槛和周期，对即时通讯、端到端加密、隐私通信领域意义很大，但它不是对整个 Signal 客户端全部代码的审计，群组消息、侧信道攻击等场景不在本次证明覆盖范围内。过去密码学形式化验证最大痛点就是成本极高，形式化语言门槛高、证明分支繁多，一点点代码改动就会导致大量证明失效，绝大多数商用加密项目只能做到协议抽象模型层面，很难下沉到编译后的机器指令，纸面安全和真实代码之间一直存在缺口；AlphaProof Code 的思路是分工协作，人类定安全目标、撰写并审核可信规约，AI 智能体自动拆解定理、补全证明步骤，再由 Lean 内核机械校验每一条证明是否合规，避免 AI 给出看起来合理但不成立的伪证明。整套验证流程分成明确的阶段，先锁定 libsignal 版本，把安全需求翻译成严格的数学规约，再启动 AI 证明智能体批量生成 Lean 证明，之后自动审计、筛选高风险片段交给研究者复核，最后把全部证明、规约开源，供外部社区独立复核。
本次 Signal 协议形式化验证核心信息表
| 项目 | 详情 |
|---|---|
| 验证框架 | AlphaProof Code（多智能体协同） |
| 基座模型 | Gemini Carbon |
| 目标代码 | libsignal v0.105.4、SPQR v1.6.0 |
| 验证层级 | Rust 源码编译后的 AArch64 机器码 |
| 证明语言 | Lean |
| 证明代码总量 | 约 650 万行 Lean 证明 |
| 可信规约基础 | 约 2.6 万行规约与机器语义定义 |
| 耗时 | 四周（五人研究团队） |
| 覆盖模块 | PQXDH 后量子握手、Triple Ratchet |
| 已证明安全属性 | 前向保密、身份认证、入侵后安全、握手保密性 |
| 公开材料 | Lean 证明工程、论文、说明文档全部开源 |
AlphaProof Code 分工与执行流程清单
- 人类密码学专家联合 AI，将 Signal 的安全需求翻译成形式化规约，所有规约必须人工审核确认，这一步是整个证明的信任根基；
- 启动 Gemini Carbon 驱动的证明智能体，自动拆解安全定理，生成 Lean 证明脚本；
- Lean 内核自动校验每一段证明，不通过的分支直接退回智能体重试；
- AI 自主完成一轮审计，标记高风险、复杂的证明片段，仅把约 1% 的内容提交给人类复核；
- 反向测试：植入历史已知漏洞的旧版本代码，框架可以识别出证明无法通过，验证这套体系的检出能力；
- 打包全部规约、证明、机器语义材料对外开源，交由独立研究者复现、审计。
核心优势与验证边界
✅ 优势
- 首次将广泛部署的加密协议，从协议模型下沉验证到未经修改的编译机器码，补上 “纸面安全” 和真实程序之间的缝隙；
- AI 承担绝大部分枯燥、分支庞大的证明书写工作，周期从数年压缩到数周，大幅降低形式化验证成本；
- 证明由 Lean 内核独立校验，不是单纯靠大模型输出，规避大模型容易产出虚假证明的风险；
- 整套成果开源，密码社区可以独立复现、检查，符合密码学安全审计的透明原则；
- 这套框架具备迁移潜力，未来可以用来验证其他端到端加密、密码库。
⚠️ 本次验证不包含的范围
- 没有覆盖完整 Signal App，只针对 libsignal 核心密码实现；
- 群组通信逻辑不在本次证明范围内；
- 无法防护时序侧信道、物理攻击、密钥泄露、上层业务配置错误；
- 只针对指定版本，代码后续迭代之后，原有证明会失效，需要重新生成证明。
技术影响与落地意义
这次 AI 参与 Signal 协议形式化验证，最大价值不是立刻让 Signal “绝对无漏洞”，而是证明了 AI 可以把形式化验证从少数顶尖团队才能触碰的奢侈品，推向主流密码组件；对于端到端加密通信来说，前向保密、入侵后安全是底线，如果底层密码库在编译环节引入隐性缺陷，哪怕协议设计没问题，用户聊天记录依然存在泄露风险；AlphaProof Code 相当于提供一套流水线，让安全团队在更新加密库的时候，同步生成数学证明，持续守住安全承诺。同时这套方案也给可信软件、区块链密码原语、支付加密组件提供新路线，未来高安全等级软件，有可能逐步把机器码层级的形式化验证纳入常态化流程。
总的来说，谷歌 DeepMind 这次用 AlphaProof Code 完成 Signal 协议形式化验证，是人机协作密码安全验证的里程碑：人类守住安全目标和可信规约，AI 承担繁重的证明撰写工作，再依靠证明助手 Lean 做刚性校验；它解决了过去形式化验证落地难、周期长、停留在模型层面的痛点，但它依然是定向的数学证明，不是万能的全盘安全审计，使用、评估这套成果时，要分清它覆盖的安全边界。
【相关 FAQ】
问题 1：谷歌 DeepMind 这次 AI 参与写证明，完成的 Signal 协议形式化验证是到哪一层？
回答 1：这次 Signal 协议形式化验证不是只验证纸面协议模型，而是直接对 libsignal 编译后的 AArch64 机器码做数学证明，打通协议安全承诺和真实运行代码。
问题 2：参与 Signal 协议形式化验证的 AI 框架叫什么，靠什么模型驱动？
回答 2：这套用于 Signal 协议形式化验证的框架叫 AlphaProof Code，由 Gemini Carbon 驱动多智能体，AI 负责生成 Lean 数学证明代码，人类专家把控安全规约。
问题 3：DeepMind 完成 Signal 协议形式化验证，一共产出多少证明代码，耗时多久？
回答 3：在 Signal 协议形式化验证项目中，AI 生成大约 650 万行 Lean 证明代码，整个验证工作由五人团队在四周内完成，传统人工方案通常需要数年。
问题 4：Signal 协议形式化验证，已经证明了哪些安全特性，哪些不在覆盖范围？
回答 4：本次 Signal 协议形式化验证证明了 PQXDH、Triple Ratchet 的前向保密、身份认证、入侵后安全、握手保密性；群组消息、侧信道攻击、完整客户端应用不在本次证明覆盖。
问题 5：AI 参与 Signal 协议形式化验证，会不会出现 AI 自己写出假证明骗过审核？
回答 5：不会，AI 写出的全部证明都要交给 Lean 证明内核机械校验，只有通过 Lean 内核核验的证明才被采信，AI 只负责生成证明，最终判定权在独立的证明检查器。
【参考资料】
[2026-11-10]（Formal Verification of Signal’s Protocol with Gemini）Google DeepMind 官方博客
[2026-11-10]（AlphaProof Code：Verifying Signal’s Security at the Machine-Code Level）DeepMind 技术论文
[2026-11-10]（DeepMind 使用 AI 智能体完成 Signal 核心机器码验证）Unite.AI
[2026-11-10]（AlphaProof Code 完成 Signal 加密协议形式化验证）Wired
[2026-11-10]（AI 辅助形式化验证，Signal 密码库通过机器码级数学证明）机器之心
【免责声明】
本文为 DeepMind Signal 协议形式化验证技术科普；本次验证仅针对指定版本 libsignal，验证成果不代表 Signal 全应用无任何安全风险；形式化证明存在明确边界，不能抵御侧信道、密钥管理失误、上层业务漏洞；证明有效性依赖 Lean 内核、规约假设与编译环境，代码版本变更后原有证明失效；本文不构成安全背书，产品上线仍需要独立安全审计。