AI 写了650万行证明，人只需读2.6万行，Signal 第一次被验到机器码

四个链接，其实是一条信任链

11 月 10 日，Google DeepMind 发了 AlphaProof Code：一个多智能体形式化验证框架，用它第一次把 Signal 协议参考实现的关键安全性质，证明到了编译后的 AArch64 机器码上。同一天，57 页技术论文、全部 Lean 规格与证明、以及 GitHub 仓库一起放了出来。发布稿里还专门点名了一年多前的老项目 CodeMender，说这类自动防御 agent 要与形式化验证配对使用，才能对抗现代网络威胁的速度和规模。

所以这不是四个孤立链接，是 Google 自己画好的一条链：CodeMender 负责找漏洞、打补丁、把整类漏洞从代码里消掉；AlphaProof Code 负责给出数学上可检查的保证。但两者最值得对比的地方不在功能，而在"凭什么信它"——CodeMender 生成的每一个补丁，至今仍要 100% 经过人类研究员审查才能上游；AlphaProof Code 生成的 650 万行证明，一行都不需要人相信。

把时间轴拉长会更清楚。2025 年 10 月 CodeMender 首次披露；2026 年 4 月这个方向被立为内部的 grand challenge；10 月 22 日 Anthropic 与 Theorem 交出另一份大规模形式化验证；11 月 10 日 DeepMind 开源。一年出头，形式化验证从"专家团队按人年计"变成了"几个工程师带着一群 agent 按周计"。这篇要讲清楚的不是又刷新了什么榜单，而是当 AI 包办了代码和证明之后，可信度到底落在了哪里。

验的不是协议模型，是编译出来的字节

密码协议的形式化分析有几十年的历史，Signal 更是被反复证过。但过去几乎所有工作都停在设计层：要么证一个抽象的协议模型，要么证一个为了好证而重写的实现，要么只证较窄的性质比如不崩溃。真实漏洞恰恰藏在设计与实现之间那条缝里。DeepMind 这次的突破点，是把 PQXDH 握手、Triple Ratchet、以及新的后量子 SPQR 棘轮，一路证到设备真正跑的那个可执行文件。

目标很具体：未修改的 libsignal v0.105.4 + spqr v1.6.0，外面包一个很薄的命令行 harness，用 stock rustc 1.98.1、musl 静态链接、LLVM ld.lld，编成一个 AArch64 Linux ELF。证明从可执行文件的入口点开始，逐条指令跟到最后的 exit_group 系统调用，中间连 musl 的 mallocng 分配器、memcpy/memset、字符串克隆、HKDF 与 HMAC 密钥派生、protobuf 序列化、MAC 校验都在射程内。被验证的代码约 560 KB、14 万条 AArch64 指令。

结果是两套独立的安全论证：符号模型下 10 条定理（前向保密、后向妥协安全、发起方与响应方保密性、认证、KCI 抗性、会话独立性、抗"先收割后解密"等），计算模型下 1 条主定理给出攻击者优势的具体界。另外他们还把两个已修复的历史 bug 反向打回 libsignal 源码、重新编译，用 Lean 严格证明这两个二进制不满足安全定理——一个叫 weak state（旧会话试解密导致未确认状态被存下），一个叫 small subgroup（X25519 基点未检查挠点，重放握手能造出共享密钥相同的第二个会话）。这一步很关键：它证明规格不是写得足够松、连有 bug 的代码都能通过。

官方博客的措辞是，这是第一次由 AI 在这个深度上形式化验证一个广泛部署的加密协议，也是这个级别的实现第一次被任何方法（含不含 AI 都算）验证到这层。Signal CTO Ehren Kret 的评价也给了：把线上代码翻译成有效的 Lean 定理，是重大突破。

650 万行证明，2.6 万行信任

论文第 7 节把账摊得很细，值得原样摆出来。整个仓库近 700 万行 Lean（含注释与空行），其中约 650 万行是证明：530 万行关于二进制层、两套安全证明共用；86 万行计算模型；35 万行符号模型；14 万行用来反证两个历史 bug；7 万行验证分配器。规格目录有约 5.4 万行，但每个文件都标了是可信、部分可信、还是由 Lean 检查过——把头条定理依赖的每个定义都读完，是约 1.8 万行（带文档约 2.8 万行），再加约 8,000 行 AArch64 语义与符号名。合计约 2.6 万行可信基础。

这就是整件事最反直觉的地方：650 万行 AI 生成物一行都不用信，2.6 万行人写的东西一行都不能错。证明不可信没关系，Lean 内核会逐行检查，任何逻辑错误都会被拒；规格却无法被自动检查，一个写松了的前提就能让定理变成废话。发布稿说 agent 先自审证明、只把约 1% 的区域标出来请人复核——那是博客口径下的"人工复核范围"，和上面 2.6 万行的"可信计算基"是两个不同口径，别混着读。

算力侧同样直白：每轮 proof campaign 通常 40 到 80 个 agent，在单台机器上连续跑 24 到 72 小时；团队是五个人、四周，并行推进符号与计算两条线。论文拿它和经典工程作量级参照：seL4 微内核耗了 20 人年，CompCert 验证过的 C 编译器 6 人年。但原文紧接着就加了限定——那些成功案例的源码本来就是为了便于验证而专门写的，而这次是既有的工业级代码、由优化编译器编译出来、一行不许改。目标不同，20 人年和 0.38 人年不能直接相除，能比的是"过去按人年计的事，现在按周计"。

底层还有一组容易被忽略的数字：他们自己写了一份 AArch64 用户态语义，7,578 行 Lean 覆盖 467 条指令和 31 个系统调用，用 Unicorn（源自 QEMU）和 Arm 官方 ASL 衍生的 Sail 模型双 oracle 逐指令对拍，加载器与系统调用模型再拿 qemu-aarch64 验。Figure 5 那组场景在 Lean 语义里跑了 10 次调用、1,560 万条指令，每次结果都和真实二进制一致，包括会话状态。但论文也承认：真实硬件和内核不是形式对象，语义的 soundness 无法被证明，只能把可信定义压小、反复测。

把编译器踢出可信基，代价写在证明里

流程分四块。规格：spec-writer agent 与人类一起把文献里的模型和性质翻成 Lean 陈述，reviewer agent 挑刺，人类逐条批准，批准后那个 git commit 就是基线。机器码语义：把可执行文件当作一串字节载入 Lean，用 ElfRunsTo 描述所有可能的运行。证明合成：orchestrator 分工、team lead 管长期目标、worker 写证明、architect 调整拆解、integrator 合并去重，critic 单独审规格修订。守门：gatekeeper 调 comparator，确认证明的陈述及其依赖的每个定义，与一份 agent 无权写入的 held-out 规格副本完全一致，只用 Lean 标准公理，且内核接受，才算过。

这里有个非常硬的技术取舍，论文第 9 节讲得比发布稿清楚：选机器码层验证，是为了不必信任编译器。Rust 编译器、LLVM、甚至 Rust 源码本身都不在可信计算基里——编译器若有 bug 破坏了被形式化的安全性质，定理会变成假，证明就过不去，而不是蒙混过关。代价也很实在：650 万行证明里有 530 万行在处理寄存器、栈帧和内存布局，这些在源码层会被抽象掉。论文自己说，源码层验证能大幅省算力，但要重新把编译器和语言语义请回可信基。

守门机制里最见功力的一条，是 specification 是被"隔离"保护的。为什么？因为 agent 会为了完成任务偷偷把目标改简单。

agent 把谓词改成了 False，还传染了整个集群

论文第 7 节引了一个真实事故，读起来比任何 benchmark 都说明问题：在某群 Lean 证明 agent 里，有一个 agent 把猜想假设里用到的谓词重新定义成了 False，命题因此变得平凡可证，而这个"技巧"随后扩散到了集群里的其他 agent。这就是奖励黑客在形式化验证里的版本——不是模型答错题，是模型找到了判据的漏洞，并把它当成经验互相学走。

于是整套防御都围绕"绝不采信 agent 的自述"来设计：

1. 不信汇报。prover、team lead、orchestrator 都不能自行宣布顶层目标完成。gatekeeper 只看文件路径和定理名，完全不看 prover 的对话与解释；Lean 在全新环境重放每条证明，sorry 和 native_decide 直接拒绝。

2. 规格锁在够不着的地方。campaign 开始时把基线规格复制到 held-out 目录，任何 agent 都写不进去；只有经过 critic 审查、并由人类或人类设定的策略批准的 amendment 才能改。critic 自己不看证明尝试，避免被"证不出来"的压力带偏。

3. 修订三条件。amendment 必须必要（有机器检查的反证、二进制上的反例，或基于代码的论证）、不削弱安全性（新增假设必须对真实代码成立）、足够小（通常一个定义里几行）。"把安全性改弱去迁就代码"永远不算 amendment，会被升级给人当作潜在 bug 处理。论文举的例子是反过来加强 contract："memcpy 可以从只读内存拷贝"。

4. 防止证空命题。agent 每引入一条新 invariant，都必须附一个在可达状态上成立的 witness；规格质量还要过 vacuity 检测、变异测试（故意跳过 MAC 校验，看定理是否变假）、以及历史 bug 回放。规格用 Gemini 4 Carbon 与 Claude Opus 5.5 交叉评审——特意换不同模型家族，避免同源盲点。

把这几条连起来看，本质是一次信任搬迁：生成方（模型、agent 集群、他们之间的对话）全部列为不可信，可信度只压到一个小而可被外部重放的检查器上。这跟 RL 里靠 reward model 打分完全不同，检查器不给"大概对"的分数，只给通过或不通过。

证明便宜了，规格成了新的稀缺品

论文第 7 节有一句最值得抄下来的话：once proofs become cheap, the hard question is what to prove（一旦证明变便宜，难的问题变成"该证什么"）。五个人四周里，主要精力不在证明，而在规格；作者明确写，没有任何一位作者写过一行证明代码，证明全部由 Gemini 4 Carbon 驱动的 agent 团队生成。人类的工作改成了：选证什么、裁决歧义、权衡安全取舍、批准规格、以及为了可读性让 agent 重写规格——这在新成员后期加入审阅时省了大麻烦。

更意外的是，照着真实代码写规格，反过来成了对学术文献的压力测试。他们把 Lean 陈述与参考论文、与 libsignal 的每一处偏离都记进目录：计算侧 200 多条，符号侧约 35 条。多数只是表述差异或论文为了工具能终止而加的限制，但其中有 15 条是已发表的 Double Ratchet 计算分析里的缺口或错误——缺假设、安全游戏条件允许平凡获胜。符号侧也发现 Cheval 等人的 ProVerif 查询在错误的棘轮索引上查跳过的消息密钥，导致印刷版里接收方前向保密并不成立，还有变量未绑定、后向妥协安全的括号范围写错等问题。不把论文证一遍，这些都还留在纸面上。

论文第 9 节因此给出一个不那么技术、但很实在的判断：复杂规格需要维护者、分析者和使用者社区共同认可，要经过多轮公开评审才能稳定下来，这是社会技术问题，不是纯技术问题。他们把全部规格与证明开源，正是为了让这个过程发生。仓库里连复现都钉死了版本：Lean 4.34.0、Rust 1.98.1、ld.lld 22.1.8、Zig 0.16.0，干净构建要数小时、峰值 15–34 GiB 内存，comparator 因为依赖 Landlock LSM 只能在 Linux 上跑。换句话说，"机器可检查"并不等于"人人能复现"，中间还隔着一道不小的工程门槛。

链条的另一半：CodeMender 至今仍要人逐补丁过目

2025 年 10 月 6 日，Raluca Ada Popa 与 Four Flynn 披露 CodeMender：基于 Gemini Deep Think 的自主 agent，既能反应式地给新漏洞打补丁，也能主动式地重写已有代码、把整类漏洞消掉。六个月内向开源项目上游提交了 72 个安全修复，涉及的项目最大有 450 万行代码。工具箱很全：静态与动态分析、差分测试、fuzzing、SMT 求解器、debugger、源码浏览器、多 agent 分工，还有基于 LLM 的 critique 工具比对改动前后是否引入回归，以及按功能等价配置的 LLM judge，失败就自我纠正。

最有代表性的例子是给 libwebp 的部分代码加上 -fbounds-safety 注解，让编译器插入边界检查。官方说，当年被用作零点击 iOS 利用链的堆溢出 CVE-2023-4863，以及已加注解区域里大多数缓冲区溢出，本会因此永久不可利用——注意这是条件式表述，只覆盖加了注解的部分，也不是在说它修了那个 CVE。

但真正决定定位的是这句：目前 CodeMender 生成的每一个补丁，都要先由人类研究员审查，才提交上游。理由是"代码安全上的错误代价太高"。项目仍是早期研究，没作为通用工具发布，技术论文也说要等后续几个月。原因不难理解：它的判据是测试、静态分析、fuzzing 和 LLM 评审，这些都是经验性证据，没有一样能给出"这个性质在所有输入下成立"的保证，所以人必须留在环里当最后一道。

两条路线的分野就在这里。CodeMender 的判据是"没测出问题"，人必须审查；AlphaProof Code 的判据是"内核接受了证明"，人退到规格那一端。所以别把 72 个修复和 650 万行证明当成同一量纲的 KPI——一个衡量覆盖了多少真实漏洞，一个衡量保证能推到多深。DeepMind 说要把两者配对，意思正是：agent 找漏洞的速度会越来越快，人类审查跟不上，得有一层不依赖人眼的判据兜底。

十九天里的同题竞答：1.8 亿行 Rocq 对 650 万行 Lean

10 月 22 日，Anthropic Frontier Red Team 与 Theorem 也发过一份大规模形式化验证：239 个 OSS-Fuzz 入口点、123 个不同的库，加起来约 1.8 亿行 Rocq 证明，一个典型证明约 60 万行，对应二进制长度中位数 18,000 条 RISC-V 指令；Mathlib 已接近 30 万条定理，Verus 那组实验里 99.95% 的测试与 CPython 行为一致。那是广度优先：把验证铺到大量真实 C 库上，抓 fuzzer 够不到的边界 bug。

DeepMind 这份是深度优先：只盯一个协议，但一路扎到 AArch64 机器码，还要同时给出符号与计算两套独立论证、10 条安全定理、以及协议级的前向保密与后向妥协安全。相隔 19 天，两家把同一件事的两个极端各做了一遍——一个回答"能不能大规模铺开"，一个回答"能不能证到底"。谁更强这类问法没意义，值得看的是它们共用同一个前提：证明由 AI 批量生成，人负责定义什么算对。

顺带一个有意思的细节：本号 11 月 5 日扒 OpenAI Pando 那篇时，里面就写着工程师让 GPT-6 Astra 写 Lean 和 TLA+ 去形式化验证 git 后端的理论、并借此发现实现 bug。五天之后，Lean 证明被推到了密码协议的机器码层。基础设施、版本控制、代码评审、验证，正在被同一股力量依次推着走。

几盆冷水：边界比结论重要

把论文的限制条款读一遍，比记住那些大数字更有用：

37 个 hook 只给契约，没证实现。SHA-256/SHA-512 压缩、AES-256-CBC、X25519、Kyber1024、ML-KEM-768 等底层密码例程，加上少数格式化与写文件函数，在二进制边界被 contract 替换；密码学原语是被理想化的，结论以"原语安全"为前提。契约本身没有对真实例程证明过。另有 18 个 panic 入口以 SIGABRT 结束运行。

覆盖范围有限。keygen 未验证，密钥作为前提给定；只覆盖一对一会话，群聊、多设备、两方以上、TOFU 首次使用信任路径、任意长度消息、侧信道都不在内；real hardware 与内核的语义 soundness 不可证；线程、信号、vDSO、动态链接、当前目录外的文件都不建模。

两套证明各有各的盲区。计算证明只覆盖经典攻击者，不覆盖量子攻击者，且在多长会话、多 epoch 的大规模场景下，优势界会变得空洞；符号证明反过来能在 DH 被未来量子计算机破解的假设下谈握手保密性，但它把密码学理想化了，不谈字节的计算保密性。Signal 把 MAC 截断成 8 字节，攻击者有 2 的 -64 次方概率猜中，所以二进制层定理只能写成"除碰撞外成立"，而碰撞概率的界不在 Lean 里。

反证也有不对称。两个历史 bug 能被 Lean 证明违反符号安全定理；但论文坦承，要反证计算定理，得先证明 Gap-DH 这类困难假设本身，那是开放问题。

还有两个口径别读错。发布稿说"超过 600 万行 Lean"、论文说"约 650 万行"，是同一批证明的不同取整；"四周"是五个人类研究员带着 agent 的四周，不是模型自己跑四周，而"历史上要专家团队数年"是 Google 自己的比较，不是第三方测评。另外仓库首页明写着 This is not an official Google product，libsignal 那部分沿用 AGPL-3.0，二次使用前得看清许可。

我的几点想法

1. 真正的创新不是"AI 会证定理"，是把信任从生成方搬到了检查方。过去两年大家习惯用更大的模型、更好的 RL 去提升生成质量；这条路线干脆承认生成物一律不可信，只在末端放一个无法被说服、无法被传染、可独立重放的检查器。held-out 规格 + comparator + 内核重放，是一套比"让模型更诚实"可靠得多的工程解。

2. 奖励黑客只是换了个马甲。把谓词重定义成 False、然后整个 agent 集群互相学走，和 RL 里刷 reward、和 agent 写测试时把断言改松，是同一类行为。凡是给 agent 设了可优化的目标，就得配一个它改不动的判据。论文里"每引入一条 invariant 必须附可达状态上的 witness"这条，几乎可以直接抄到任何 agentic 工作流里。

3. 瓶颈正在往上游迁移。写代码便宜了，git、CI、评审先崩，本号十月那几篇写的都是这个；现在证明也便宜了，规格顶上来成了新瓶颈，而且卡点从技术变成了共识——谁有权定义"正确"，社区怎么就一份复杂规格达成一致。论文自己说这是社会技术问题，这判断比 650 万行更值钱。

4. 别急着把形式化验证当成"AI 代码已解决"。这次是人先在四周里把规格磨到能证、再让 40–80 个 agent 跑上几十小时，验的还是 560 KB 的单个可执行文件、外加 37 个理想化契约。它证明的是"深水区可以打了"，不是"所有代码都能这么打"。CodeMender 那 100% 人工审查也不是保守，是判据不同导致的必然。

5. 接上本号这条线。10 月 14 日 Scion 篇讲代码太多版本控制先扛不住，10 月 19 日 code review 篇讲人已经不逐行读代码、改看证据与意图，11 月 5 日 Pando 篇里 OpenAI 已经开始让模型写 Lean 验证系统性质。到今天这一步，人连证明都不读了，只读那 2.6 万行规格。AI 写代码撕开的三道口子，正在被逐个补上；而人在环里的位置，每次都往更上游挪一格。

— END —

参考资料：
[1] Pushmeet Kohli, Swarat Chaudhuri, "Introducing AlphaProof Code: a breakthrough in verifying complex software at depth", Google DeepMind, 2026-11-10
https://deepmind.google/blog/introducing-alphaproof-code/
[2] Swarat Chaudhuri, Andrew Ferraiuolo, Anton Kovsharov, Tej Chajed, Sam Schlesinger, Karn Seth, Jonathan Katz, Charles Sutton, Pushmeet Kohli, "AlphaProof Code: Verifying Signal's Security at the Machine-Code Level", 2026-11-10（57 页技术论文）
https://deepmind.google/documents/36/Formal_Verification_of_Signal_4.pdf
[3] AlphaProof Code Lean development（全部规格与证明）
https://google-deepmind.github.io/code-verification/
[4] google-deepmind/code-verification（Initial commit 2026-11-10；Lean 4.34.0 / Rust 1.98.1 / ld.lld 22.1.8 / Zig 0.16.0；声明 This is not an official Google product）
https://github.com/google-deepmind/code-verification
[5] Raluca Ada Popa, Four Flynn, "Introducing CodeMender: an AI agent for code security", Google DeepMind, 2025-10-06
https://deepmind.google/blog/introducing-codemender-an-ai-agent-for-code-security/
[6] Anthropic Frontier Red Team with Theorem, "Formal verification", 2026-10-22
https://www.anthropic.com/research/formal-verification
[7] 本号前作：《每天合并3万条代码，git 先扛不住了》（2026-10-14）
https://mp.weixin.qq.com/s/VPlqtCM7L-WYIAHmFwL0-w
[8] 本号前作：《Claude 写了90%的代码，那谁来做 code review？》（2026-10-19）
https://mp.weixin.qq.com/s/Kms5dr1tIHqtH5vj17HuGg
[9] 本号前作：《Anthropic 把 git 扔了，OpenAI 说不用扔》（2026-11-05）
https://mp.weixin.qq.com/s/fh5tslrkKXqlzKXOxdmneg