谷歌 DeepMind 推出 AlphaProof Code 多智能体框架，依靠 Gemini 驱动的 AI 智能体生成 650 万行 Lean 证明代码，首次把 Signal 的 libsignal 加密库从协议规范一直验证到 AArch64 编译后的机器码，不是只验证理论协议或者源代码，而是直接证明设备上实际运行的二进制指令满足安全属性，整个验证周期仅 4 周，过去这类深度形式化验证往往要耗费数年人力，这次验证覆盖 PQXDH 后量子握手、Triple Ratchet 双棘轮机制，验证了前向保密、身份认证、后入侵安全等核心安全特性，是商用加密协议验证领域的重要里程碑。传统形式化验证门槛极高，需要密码专家、形式化方法专家手动写大量证明脚本，工程量巨大、成本昂贵，很多成熟加密项目只能停留在纸面协议建模，没法落地到机器码层面；AlphaProof Code 这套方案把工作拆分，人类负责定义安全规范、审核假设，AI 智能体负责自动构造海量数学证明，再由 Lean 证明内核做机器校验，把绝大多数机械证明工作交给智能体，只留下约 1% 的复杂分支交给人工复核。
AlphaProof Code 验证 Signal 核心信息清单
- 验证框架：AlphaProof Code，多 AI 智能体协作，基于 Gemini 4 Carbon
- 证明代码总量：约 650 万行 Lean 证明代码
- 可信基础代码：2.6 万行，包含安全规范、AArch64 机器码语义
- 验证对象：libsignal v0.105.4、SPQR v1.6.0，未修改原版代码，AArch64 Linux 二进制
- 覆盖机制：PQXDH 后量子握手、Triple Ratchet 双棘轮
- 已证明安全属性：前向保密、身份认证、后入侵安全、握手保密性
- 耗时：5 人团队，4 周完成
- 未覆盖范围：群聊、密钥生成、侧信道攻击防护
验证范围边界对照表
| 项目 | 纳入本次机器码验证 | 不在本次验证范围 |
|---|---|---|
| 一对一消息 PQXDH 握手 | ✅ | ❌ |
| 一对一 Triple Ratchet 棘轮 | ✅ | ❌ |
| 群聊加密逻辑 | ❌ | ✅ |
| 密钥生成模块 | ❌ | ✅ |
| 侧信道、时序攻击 | ❌ | ✅ |
AlphaProof Code 智能体验证 Signal 的完整步骤
- 专家联合模型，把 Signal 的安全需求翻译成 Lean 语言的形式化数学规范，全部内容人工审核定稿
- 搭建 AArch64 指令集形式化语义，建立机器码和数学模型之间的对应关系
- 调度多个 AI 证明智能体并行生成 Lean 证明，每一段证明提交给 Lean 内核自动校验
- 智能体自动标记无法自证、逻辑复杂的分支，集中交给人类专家排查
- 注入历史上已经修复的已知 bug，用来测试这套证明体系能不能识别安全违规
- 汇总全部证明工件，对外开源规范与证明代码，供外部同行复核
综合来看，这次 AI 智能体写 650 万行证明代码的价值，不在于直接找出新漏洞，而是证明 AI 可以把高成本的机器码级形式化验证变得可落地；它不能替代密码专家做规范定义，但是可以承接海量、重复的证明构造工作，未来有机会用到更多加密库、安全底层组件的审计中，不过它有明确边界，群聊、侧信道这类风险不在本次验证覆盖之内。
【相关 FAQ】
问题 1：AI 智能体写下 650 万行证明代码，DeepMind 这次 Signal 验证验证到了哪一层？
回答 1：AI 智能体产出 650 万行 Lean 证明代码，DeepMind 这次 Signal 验证突破到机器码层级，验证的是编译之后、设备上实际跑的 AArch64 二进制，而不是只验证协议文档或者源代码。
问题 2：DeepMind 用 AI 智能体做 Signal 机器码级验证，有没有发现新安全漏洞？
回答 2：DeepMind 本次 AI 智能体完成的 Signal 机器码级验证没有发现新漏洞，但测试时可以识别曾经修复的历史 bug，证明这套证明体系可以抓到对应的安全违规。
问题 3：AI 智能体生成 650 万行 Lean 代码，是不是意味着 AI 可以完全独立完成加密验证？
回答 3：并不是，AI 智能体负责构造证明脚本，Signal 的安全规范、底层假设、高风险分支复核都由人类密码专家把控，AI 只是辅助证明的工具。
问题 4：DeepMind 这套 AlphaProof Code，Signal 机器码级验证覆盖了群聊加密吗？
回答 4：本次 AI 智能体完成的 Signal 机器码级验证只覆盖一对一消息的 PQXDH 握手和 Triple Ratchet 棘轮，群聊加密逻辑不在本次验证范围内。
【参考资料】
[2026-11-11]（AI 智能体写下 650 万行代码证明：谷歌 DeepMind 把 Signal 的加密实现验证到了机器码级）量子位
[2026-11-10]（AlphaProof Code: Verifying Signal’s Security at the Machine-Code Level）Google DeepMind
[2026-11-11]（650 万行数学证明，4 周交卷，Gemini 4 Carbon 啃下加密协议验证硬骨头）36 氪
[2026-11-10]（Google DeepMind Uses AI Agents to Verify Signal’s Core Machine Code）Unite.AI
【免责声明】
本文仅为 DeepMind Signal 机器码级形式化验证资讯整理，不构成加密产品安全背书；本次验证有明确边界，不覆盖群聊、侧信道攻击等场景；证明结果、规范文件、约束条件以 DeepMind 官方论文和开源仓库为准，形式化验证不等于绝对无漏洞，安全评估仍需要结合多维度审计。