DeepMind 推出 AlphaProof Code 多智能体框架，只用 4 周时间生成 650 万行 Lean 证明代码，完成 Signal libsignal 库真机 AArch64 机器码层面的形式化安全证明，这件事最大的意义是突破了传统形式化验证只能验证协议文档、很难落地到编译后真机代码的老问题，过去同等规模的密码协议形式化验证，专家团队往往要耗费数年时间，而这次是直接针对未经修改的真机运行代码，验证 PQXDH 后量子握手、Triple Ratchet 棘轮机制，确认前向保密、后妥协安全、身份认证这些核心安全特性成立；但要分清边界，本次只覆盖核心密码模块，不是整个 Signal APP 全部代码，也不包含侧信道攻击、群聊、密钥生成等范围，不能理解成 Signal 已经绝对无懈可击。
一、AlphaProof Code 验证覆盖范围清单
- 验证对象：libsignal 参考实现，编译后的 AArch64 真机机器码，不是纸上协议文档
- 核心模块：PQXDH 后量子密钥交换握手、Triple Ratchet 消息棘轮算法
- 证明安全属性：前向保密、消息认证、握手保密性、后妥协安全
- 工具栈：Gemini Carbon 驱动 AI 智能体 + Lean 证明器内核 + AArch64 机器码形式语义
- 产出规模：约 650 万行 Lean 证明代码，可信基础规格代码约 2.6 万行
- 人工参与：AI 自动完成大部分证明，仅约 1% 内容需要人工复核
二、传统形式化验证 vs 本次 AlphaProof Code 方案对比
| 验证方式 | 验证层级 | 周期 | 主要短板 |
|---|---|---|---|
| 传统人工形式化验证 | 大多停留在协议数学模型、伪代码 | 数年 | 很难对齐真机编译代码，设计和实现之间容易出现漏洞断层 |
| 常规安全审计 | 源码人工审计、模糊测试 | 数周～数月 | 只能找已知类型漏洞，无法数学证明安全属性一直成立 |
| AlphaProof Code 本次方案 | 直接到 AArch64 机器码 | 4 周 | 验证范围有限，有明确假设边界，不覆盖侧信道、操作系统漏洞 |
三、完整落地验证流程
- 定义安全规格：密码专家和 AI 一起，把 Signal 的安全目标翻译成数学形式化规范，所有规范都经过人工审核确认。
- AI 智能体生成 Lean 证明：Gemini Carbon 驱动的证明智能体自动构造证明脚本，生成海量 Lean 证明代码。
- Lean 内核自动校验：证明交给 Lean 内核做机器检查，排除逻辑错误，筛出存疑片段。
- 人工重点复核：仅 AI 标记的 1% 高风险部分交给密码专家人工审查，其余由证明器自动确认。
- 对照漏洞样本复测：灌入两个历史已知漏洞版本，框架可以识别出版本不满足安全条件，验证工具本身有效。
- 开源交付证明工件：把规格、语义、Lean 证明材料对外开源，供社区复现、审计。
四、本次验证的价值与边界风险
价值
- 打通协议安全到真机机器码的证明链路，解决 “协议安全，代码实现翻车” 的常见痛点。
- 大幅压缩形式化验证周期，让高成本的密码数学证明有机会普及到更多商用加密组件。
- 为后量子加密协议提供可复用的机器码验证范式，适配未来后量子迁移需求。
- 证明结果由 Lean 内核自动核验，比纯人工审计更不容易漏掉逻辑漏洞。
风险与局限
- 验证范围是限定子集，不包含 Signal 完整客户端、群聊、密钥生成、随机数源、侧信道防护。
- 依赖 AArch64 机器码语义假设，操作系统、内存、硬件侧信道不在本次证明范围内。
- 形式化证明只能证明 “在预设模型假设下满足安全属性”，不等于所有攻击路径全部封死。
- 目前还没有第三方独立复现验证结果，属于 DeepMind 的研究成果，不是标准化安全认证。
【常见问题】
问题 1：DeepMind4 周狂写 600 万行证明，Signal 真机代码这次验证到底证明了什么？
回答 1：DeepMind4 周生成 650 万行 Lean 证明，证明 Signal libsignal 库 AArch64 真机代码里 PQXDH 握手、Triple Ratchet 棘轮机制在设定模型下满足前向保密、后妥协安全等核心安全特性，验证直达机器码，不只是纸上协议。
问题 2：DeepMind 这次 Signal 真机代码形式化验证之后，是不是 Signal 软件就完全不会被攻破？
回答 2：不是，DeepMind 本次 Signal 真机代码验证只覆盖核心密码模块，不覆盖侧信道、操作系统漏洞、群聊模块等，只能证明限定范围内的安全属性，无法保证软件绝对不会被攻破。
问题 3：AlphaProof Code 做 Signal 真机代码安全证明，和普通代码审计、模糊测试有什么区别？
回答 3：普通审计、模糊测试是找漏洞，DeepMind 针对 Signal 真机代码的形式化证明是用数学方式证明安全属性成立，只要模型假设不变，就不存在该范围内的逻辑漏洞，但它覆盖范围比测试更窄，对模型假设高度依赖。
【参考资料】
[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]（Google DeepMind's AlphaProof Code formally verifies the Signal protocol's cryptographic code in four weeks）AI Brief
[2026-11-10]（DeepMind’s AI System Formally Verifies Signal Protocol）Msoftnews
【免责声明】
本文为 DeepMind AlphaProof Code 验证 Signal 真机代码的技术科普，本次形式化验证结论仅在论文预设模型、限定代码模块下成立；证明结果不等于产品安全认证，不能替代独立安全审计、渗透测试；相关证明材料、边界条件以 DeepMind 官方开源文档为准，本文不构成密码产品选型、安全评估依据。