Google DeepMind 用 AI 智能体为 Signal 编译代码生成 Lean 安全证明

Google DeepMind 于 2026 年 11 月 10 日推出 AlphaProof Code，利用 AI 智能体团队为 Signal 编译后的 libsignal 代码的特定安全属性生成经机器校验的 Lean 证明。这个五人研究团队在四周内完成了证明工作，并公开了其规格说明与验证产物以供外部审查。

这项工作超越了 Signal 协议设计的抽象模型，直接针对其编译后的实现。研究人员将未经修改的 libsignal v0.105.4 和 SPQR v1.6.0 crate 封装在一个小型命令行测试框架中，然后使用原版 rustc 构建了一个静态链接的 AArch64 Linux 可执行文件。技术论文将这一成果描述为首次针对广泛部署的密码协议实现中未经修改代码的协议级安全证明。

五名研究人员在证明工作上花费了四周时间，在他们的工作站上持续运行智能体，同时并行推进符号证明和计算证明。论文报告称，智能体生成了约 650 万行经机器校验的 Lean 证明代码，这些代码建立在约 2.6 万行可信规格说明和 AArch64 语义之上。

人类负责选择属性、解决歧义与安全权衡、审查规格说明并保留最终批准权。由 Gemini 4 Carbon 和 Claude Opus 5.5 驱动的智能体起草并审查了这些规格说明，其中包括来自不同模型家族的审查。随后，Gemini 4 Carbon 智能体团队生成了全部证明代码；没有任何作者编写证明代码。典型的运行活动在一台机器上使用 40 到 80 个智能体，持续 24 到 72 小时，由一名编排者和团队负责人协调证明工作者，同时架构师和集成者角色维护共享的证明基础。

只有在 Lean 内核检查通过，并且比较器确认该证明与留出的、经人类批准的规格说明（包括每一个传递性定义）相匹配，且仅使用 Lean 的标准公理时，把关程序才会接受该证明。当证明暴露出规格说明问题时，智能体可以提出小幅修正，但对可信假设的更改需要人类批准或用户设定的策略，并会连同理由一起记录。该控制措施针对的是智能体生成证明中一个已有记录的风险：规格说明可能通过其某个定义被间接削弱。

验证目标是覆盖 PQXDH 握手和 Triple Ratchet 消息传递的一对一会话代码。研究人员报告了两个独立的论证：在理想化密码学假设下的十个符号定理，以及一个通过密码学假设和统计项来界定攻击者优势的计算证明。其属性包括前向保密（在当前状态被窃取后保护较早的消息）、认证、妥协后安全（涉及妥协后的恢复）以及握手保密。符号论证还额外覆盖了在后续 Diffie–Hellman 被攻破后的握手保密。

为了测试这些规格说明能否捕获真实错误，团队反向应用了两个此前已修复的 libsignal 漏洞（称为弱状态和小子群）的修复，并重新编译了修改后的二进制文件。在这两种情况下，它都生成了 Lean 证明，表明符号安全定理失败。公开的验证仓库将计算、符号、共享二进制和 AArch64 语义材料分开，并记录了如何重建和独立检查这些证明。

Signal 首席技术官 Ehren Kret 表示，这项工作“让我们对代码的隐私保障更有信心”。

局限与后续步骤

论文指出，这两个论证都没有证明 SPQR 旨在增加的后量子恢复能力：计算定理覆盖的是经典攻击者，而符号棘轮定理允许攻击者选择 SPQR 密钥。计算模型还限制了若干攻击者行为，并且在消息和会话规模足够大时会变得空洞。这些边界界定了外部审查者在将机器校验的证明视为特定部署的安全保障之前必须信任的内容。

研究人员声明的后续步骤是加强定理、通过验证更多挂钩例程并将密码学契约与已验证实现连接来缩小可信基础，以及将覆盖范围扩展到群组消息传递、密封发送者和服务器端协议。他们在新 libsignal 版本发布前进行验证的目标是一个研究目标，而非已宣布的部署。

这一成果的直接意义在于它所展示的分工：智能体处理证明构建，而保障仍然依赖于经人类审查的规格说明和明确的假设。公开证明和检查程序为外部审查者提供了一种检验该基础的方法，同时研究人员正努力将这一工作流程带入持续的 libsignal 开发中。