谷歌 DeepMind 推出 AlphaProof Code 多智能体框架，依靠 AI 智能体生成约 650 万行 Lean 证明代码，首次将广泛商用的 Signal 加密协议核心实现，验证到编译完成后的 AArch64 机器码层级，只用 4 周就完成了过去专家团队需要数年的形式化验证工作。过去密码协议验证大多停留在纸面协议模型或者源码层面，很难覆盖编译后机器指令里潜藏的漏洞，这次直接验证未经修改的 libsignal 库二进制代码，确认 PQXDH 后量子握手、Triple Ratchet 双棘轮机制的安全属性，包括前向保密、身份认证、事后泄露安全、握手保密性。整套验证体系中，真正需要人工审核的可信规范代码仅 2.6 万行，AI 自动完成绝大多数证明撰写，还自动标记仅 1% 的代码段留给人类复核。研究团队还把曾经修复的两个真实 libsignal 漏洞重新注入测试，AlphaProof Code 成功检出这两处缺陷，证实这套验证方法可以抓到真实安全问题，但本次验证只覆盖一对一会话核心模块，不代表整个 Signal App 全部功能完全无漏洞。
一、项目核心信息一览
| 项目项 | 详情 |
|---|---|
| 验证目标 | libsignal v0.105.4，Signal 协议底层加密库 |
| 验证层级 | 编译后的 AArch64 机器码（64 位 ARM） |
| AI 框架 | AlphaProof Code，Gemini Carbon 驱动 AI 智能体 |
| 证明代码规模 | 约 650 万行 Lean 证明代码 |
| 可信基础代码 | 约 26000 行规范与机器码语义定义 |
| 耗时 | 4 周（5 人研究团队） |
| 覆盖安全模块 | PQXDH 后量子握手、Triple Ratchet |
| 验证安全属性 | 前向保密、身份认证、事后泄露安全、握手保密 |
二、为什么这次 Signal 机器码级验证意义重大
- 填补协议设计与机器码之间的验证缺口：很多加密协议理论上安全，但编译器、底层指令会引入隐藏 bug，传统验证很难触及。
- AI 大幅降低形式化验证成本：传统形式化验证门槛极高、周期漫长，AI 智能体自动生成海量数学证明，只保留少量代码交给人类专家审核。
- 覆盖真实上线代码：直接使用未经修改的 libsignal 源码编译出的可执行文件，不是简化改造后的测试版本。
- 验证成果开源：所有规范、证明材料以 Apache2.0 协议对外公开，供行业审计复核。
三、AlphaProof Code 整套验证执行步骤
- 人工定义安全规范：密码学专家把 Signal 需要满足的安全规则，翻译成 Lean 形式化数学规范，这部分内容需要人工审核确认。
- AI 智能体批量生成证明：多组 AI 证明智能体基于规范，自动撰写 Lean 证明代码，生成总计 650 万行证明内容。
- Lean 内核自动校验证明：所有 AI 产出的证明代码，交给 Lean 定理证明器内核自动检查，只有通过校验的证明才算有效。
- 自动筛选待人工复核内容：AI 识别高风险片段，仅标记约 1% 的内容交由人类专家二次审查。
- 漏洞回灌测试验证能力：将历史已知漏洞重新放进被测代码，测试框架能否发现安全违规，检验整套验证体系有效性。
四、本次验证的边界与局限
- 验证范围仅限一对一会话核心加密逻辑，不包含 Signal 群组聊天、完整 APP 客户端代码。
- 不覆盖侧信道攻击、硬件漏洞、操作系统层面的安全风险。
- 只针对特定编译环境、特定版本 libsignal，更换编译器、版本后结论不能直接沿用。
- 验证成功不等于绝对永不被攻破，只是在预设安全模型内证明满足约定安全特性。
五、总结
谷歌 DeepMind 的 AI 智能体产出 650 万行 Lean 证明代码，实现 Signal 加密实现的机器码级形式化验证，是密码安全领域的里程碑。AI 把原本数年的验证压缩到 4 周，打通从加密协议理论到设备上实际运行机器指令的证明链路，但大家也要分清验证覆盖范围，不能理解成 Signal 全功能彻底无安全隐患。
【常见问题】
问题 1：AI 智能体写出 650 万行证明代码，DeepMind 完成的 Signal 机器码级验证是什么意思？
回答 1：AI 智能体生成 650 万行 Lean 数学证明代码，DeepMind 把 Signal 底层加密库验证到机器码层级，不再只验证源码或者理论协议，直接证明编译后的机器指令满足预设加密安全特性。
问题 2：650 万行证明代码，DeepMind Signal 机器码级验证，是不是证明 Signal 软件完全没有漏洞？
回答 2：不是，DeepMind 的 Signal 机器码级验证仅覆盖一对一聊天的 PQXDH 握手、Triple Ratchet 模块，不包含群组功能、侧信道攻击等场景，不能保证 Signal 整个 APP 不存在任何漏洞。
问题 3：AI 生成 650 万行代码完成 Signal 机器码验证，AlphaProof Code 是什么？
回答 3：AlphaProof Code 是 DeepMind 打造的多 AI 智能体形式化验证框架，依靠 Gemini Carbon 智能体自动写出 650 万行 Lean 证明代码，完成 Signal 加密库从源码到机器码的安全数学证明。
问题 4：DeepMind Signal 机器码级验证，650 万行证明代码是直接写 Signal 聊天程序吗？
回答 4：不是，650 万行是 Lean 语言的数学证明代码，不是 Signal 聊天软件本身代码，用来数学证明 libsignal 机器码满足加密安全要求。
【参考资料】
[2026-11-13]（Google DeepMind Uses AI Agents to Verify Signal’s Core Machine Code）Unite.AI
[2026-11-11]（650 万行数学证明，4 周交卷，Gemini 4 Carbon 啃下加密协议验证硬骨头）36 氪
[2026-11-11]（谷歌 DeepMind 用 AI 证明 Signal 协议端到端加密可靠性）虎嗅网
[2026-11-10]（AlphaProof Code: Verifying Signal’s Security at the Machine-Code Level）Google DeepMind 官网
[2026-11-10]（谷歌 DeepMind 用 AI 完成 Signal 协议形式化验证，数学证明其端到端加密可靠性）IT 之家
【免责声明】
本文内容仅为前沿技术资讯科普，不构成网络安全、密码产品的选型与安全担保建议。本次 DeepMind Signal 机器码级验证存在明确的覆盖边界，实际通信安全还受操作系统、硬件、使用环境等多重因素影响，相关技术细节以 DeepMind 官方论文及开源仓库为准。