Google DeepMind 发布 AlphaProof Code：智能体写出约 650 万行 Lean 证明，在编译后的 Arm 机器码上证明 libsignal 一对一会话的多项安全性质

Google DeepMind 11 月 10 日发布 AlphaProof Code，并公开技术论文与验证代码。团队用它对 Signal 协议的参考实现 libsignal（v0.105.4，一对一会话）做形式化验证：研究人员与 Gemini 4 Carbon、Claude Opus 5.5 驱动的智能体一起写规格，由 Gemini 4 Carbon 智能体团队生成约 650 万行 Lean 证明，证明的对象是用标准 rustc 编译出的 AArch64 机器码，覆盖前向保密、认证、失陷后安全和握手保密。5 人团队用时四周。群聊、量子攻击者下的计算模型证明等仍不在范围内。

证明的是编译出来的二进制

Google DeepMind 11 月 10 日发布 AlphaProof Code，同时公开技术论文和 GitHub 仓库 google-deepmind/code-verification。验证对象是 Signal 协议的参考实现 libsignal v0.105.4（含 spqr v1.6.0），只限一对一会话，覆盖后量子 PQXDH 握手和 Triple Ratchet。团队没有停在协议设计层面，而是用标准 rustc 1.98.1 编译出 AArch64 Linux 可执行文件，再证明这个二进制满足前向保密、认证、失陷后安全和握手保密。DeepMind 博文称，这是广泛部署的同类协议实现第一次被形式化验证；论文的表述更收敛，称首次把符号层分析严格连到汇编实现。

人定规格，智能体写证明

规格由研究人员与 Gemini 4 Carbon、Claude Opus 5.5 驱动的智能体反复讨论写成，人负责决定证明什么并最终批准；证明代码全部由 Gemini 4 Carbon 智能体团队生成，作者没有手写。一次运行通常在单台机器上跑 40 到 80 个智能体、持续 24 到 72 小时。5 人团队用时四周，产出约 650 万行 Lean 证明，需要人去读和信任的部分约 2.6 万行（规格与 AArch64 语义）。DeepMind 称智能体只把约 1% 的代码标给人工复核。为检验能否分辨有缺陷的代码，团队把两个已修复的 libsignal 漏洞重新放回，证明了对应二进制违反安全定理。Signal CTO Ehren Kret 在博文中评价这项工作扩大了以往形式化验证的范围。

没有覆盖的部分

这次没有报告新漏洞。论文列出的信任基包括 Lean 内核、AArch64 语义、规格和 37 个被挂钩例程的契约；密码学原语按理想化或安全假设处理；计算模型下的证明只针对经典攻击者，多设备状态、群聊、线程与动态链接都不在范围内。博文只说开源验证工件，没有说明 AlphaProof Code 框架本身是否对外提供。

via: Google DeepMind 博客：AlphaProof Code: a breakthrough in verifying complex software at depth、技术论文：AlphaProof Code: Verifying Signal's Security at the Machine-Code Level、GitHub：google-deepmind/code-verification