别信 Agent 说「没问题」：DeepMind 用 Lean 验证 Signal 代码，人只看了约 1%

别信 Agent 说「没问题」：DeepMind 用 Lean 验证 Signal 代码，人只看了约 1%

昨天那篇《给 Agent 做急停》，说的是 agent 已经在跑、你决定让它停的时候，保险丝该写在哪一层。《Agent 写基础设施的 4 道验收》 则把验收卡在真实边界上，而不是「又生成了一批看起来能跑的 diff」。这一篇补验收那一侧更硬的一句：当 agent 写完、并告诉你「没问题」时，你到底信哪一层检查。

2026 年 11 月 10 日，Google DeepMind 发布了 AlphaProof Code 官方博文，并同期放出技术报告。据其自述，他们用一套多智能体形式化验证框架，证明了 Signal 协议参考实现 libsignal 的若干关键安全性质，而且验到了编译后的机器码。

先把结论放在前面：值得抄的不是「650 万行 Lean」或「人只看了约 1%」这两个数字，而是分工：人审规格，机器硬检查证明，人只再看被标记出来的部分。 Agent 口头说「没问题」，和 Lean kernel 接受一份证明，不是同一件事。

说明：下文机制与数字，均据 DeepMind 官方博文（2026-11-10）与技术报告转述，数字写「据 DeepMind 称」。本文未复现这些证明，也未对 Signal 产品做独立审计。验证针对的是特定 CLI 与编译配置下的性质，并依赖一组可信假设——不要把它读成「Signal 全产品已被证明绝对安全」。

一、他们实际验证了什么（以及没验证什么）

据技术报告，验证对象是 libsignal（报告写明为 v0.105.4，并带上 SPQR 相关 crate）的一对一会话代码：包括后量子握手 PQXDH，以及 Triple Ratchet 消息阶段。他们没有对着 Rust 源码「看一眼就签字」，而是把未改动的库链进一个小型命令行工具 libsignal-cli，用常规的 rustc（报告写明为 1.98.1）编译成 AArch64 Linux 可执行文件，再对这份机器码陈述定理。

据报告，被验证的 libsignal 代码大约 560 KB，约 14 万条 AArch64 指令。证明覆盖的性质包括前向保密、认证、失陷后安全（post-compromise security）以及握手保密等。博文也强调：多数协议验证停在设计层，而这套工作往下走到了「编译后、设备上跑的那份代码」是否满足所写规格。

边界同样写在原文里，值得先看：

1. 验的是这份 CLI 构建，不是 Signal 官方 App 本身。 报告写明，Android / iOS 上的 Signal 应用跑的是同一份 Rust 协议代码，但编译参数、链接方式和操作系统接口不同。定理要迁过去，还需要额外信任这些环境没有改变协议代码在该 CLI 里被行使的行为。
2. 不是整个产品。 一对一会话是范围；群组消息被明确留作后续工作。密钥生成（keygen）也未纳入验证，定理把各方密钥当作前置条件。
3. 性质是「规格里写下的那些」，不是「绝对安全」。 证明依赖 Lean 的 kernel、密码原语的安全性假设、AArch64 与进程模型，以及对若干被合约替换的底层例程。规格写错、假设不成立，或超出这份构建的范围，结论就不能原样搬用。

Signal CTO Ehren Kret 在博文中对方法给予正面评价，把「用 AI agent 把实时代码翻译成可通过的 Lean 定理」称作一次重要扩展。这句话是当事方的评价，不是「全产品已被证明绝对安全」的背书。

二、四步流程：人审规格，机器检查证明

AlphaProof Code 被写成一套多人、多模型分工的框架。据博文与报告，大致是四步：

1. 人与模型一起写规格，每一条由人审。 研究员和模型把安全目标翻译成 Lean 里的形式化规格。规格是可信基的一部分：它定义「正确和安全」到底指什么，以及证明排除了哪类错误与攻击。规格本身不能靠自动检查来保证没写弱——写得过窄、假设过强，有漏洞的代码也可能「证明通过」。所以人要做最终决定。
2. 由 Gemini Carbon 驱动的 agent 写证明。 据技术报告，agent 生成了约 650 万行经 Lean kernel 检查的证明代码；博文的口径是「超过 600 万行」。这些证明本身被当作不可信产物：写错了，kernel 会拒。
3. Lean kernel 做硬检查。 报告把这一点写得很死：证明是否成立，不取决于写证明的那些 agent 可不可靠，而取决于 kernel 是否接受，以及（开发过程中）比较工具是否确认它证明的正好是人批准过的那份规格。
4. agent 标出需要人再看的部分。 据博文，这部分大约相当于代码库的 1%。因为其余证明由 Lean 自动检查，专家可以把人工复查集中在判断真正重要的地方。

据报告，读者若要信任这些定理，需要审阅定理语句及其依赖的定义：仓库内大约 1.8 万行，再加上约 8,000 行 AArch64 语义，合计大约 2.6 万行可信规格与机器模型；另有一份从目标文件抽出的机器码表示，Lean 会按可执行文件的字节核对，需要额外信任的主要是符号名。换句话说：人要认真看的是规格和假设，不是把 650 万行证明逐行读完。

流程里还有一个容易被标题带跑的点。博文把全过程写成：据称由 5 人团队在四周内并行完成，并对照「历史上专家团队往往要数年」。这是官方自己的对照口径，且报告也写明，耗费主要从「写证明」转到了「把规格写对」。不要把它读成「五个人四周就能给任意产品盖章」。

三、为什么「模型说没问题」算不得验收

形式化验证把一件事拆开了：生成证明的可以是 agent，检查证明的必须是独立的硬逻辑。Lean kernel 不看模型是否自信，只看证明是否在已批准的规格下成立。

这还不够。如果规格本身是空的、过弱的，或者悄悄加了过强的前提，证明通过也保护不了你。报告写了他们用来给规格「压力测试」的办法：审稿 agent 从怀疑立场挑毛病；证明 agent 会额外证明前提并非自相矛盾；以及用已知坏例做检验。其中最直白的一项是：他们把两个此前已修复的真实漏洞，重新引入隔离版本并重新编译，然后给出机器检查的证明——有漏洞的那一版，不满足其符号安全定理。

对做 harness 或代码验收的人，只需记住这一句：验收标准要强到「已知的坏例子会失败」；否则你测到的可能只是「模型很会把话说圆」。 本文不展开这两个历史漏洞的触发路径，它们当时已被上游修复，这里只用来说明：规格本身也要拿坏例子去撞。

四、范围和假设，必须写在结论旁边

标题里的「人只看了约 1%」很容易被读成「几乎不用看」。官方自己把假设和限制写得很长，这里只摘对阅读结论最要紧的几条（均据报告）：

• 特定运行形态。 定理说的是这份 libsignal-cli：一次运行做一方的一次操作（如 init / send / recv），状态落在目录里，随机数来自约定文件。不是对 Signal 服务器、客户端界面，或任意编译开关下的二进制，做了同样的声明。
• 一组必须信任的底座。 包括 Lean kernel、AArch64 与进程语义、若干底层密码例程及其他被合约替换的函数，以及密码原语本身的安全假设。Rust 编译器反而被明确排除在信任之外：若编译器或源码里有会破坏所列性质的错误，定理应当变为不成立，证明也就过不去。
• 两套模型，覆盖并不相同。 符号模型把原语理想化，并在一定前提下讨论包括「未来量子对手破坏 DH」在内的握手保密等性质；计算模型给的是经典对手优势的具体上界，报告写明它不覆盖量子对手。哪一条性质在哪一套模型里成立，不能混着说。
• 规模与场景还有限制。 例如计算侧的统计项会在会话或轮次极大时变得没有意义；符号侧的机器码定理覆盖的场景，也比模型本身更窄。这些不是脚注，而是结论的一部分。

所以，对外表述应当停在：「据 DeepMind 称，他们在特定 CLI 与编译配置下，对 libsignal 的关键协议性质给出了机器检查的证明，并公开了规格、证明与假设。」不要写成「Signal 已被证明绝对安全」。

五、个人和小团队可直接拿走的清单

不必假装自己能在四周内形式化验证一套加密协议。大多数本地或小团队 agent，真正能抄的是分工，而不是 Lean 的体量。

1. 不要把「agent 说没问题」当成验收结论。 口头 LGTM、它自己写的测试全绿、它自己做的 code review，都还在同一支笔杆里。检查必须来自独立的硬逻辑。
2. 先把验收标准写成可检查的规格，并且由人审。 对照 AlphaProof Code：人决定证明什么、假设是什么、边界在哪里。规格含糊时，后面的自动检查再快也只是在检查一句空话。
3. 硬检查交给机器，不要交给模型的判断。 对大多数项目，这就是类型检查、单元测试、属性测试、CI、linter，或合同测试；只有极少数关键路径才需要定理证明器。共同点是：通过或失败不取决于模型此刻是否自信。
4. 人只复查规格，以及被自动检查标出来的部分。 「约 1%」是他们的结果，不是你的指标。你要问的是：哪些失败必须人看，哪些通过可以不再人肉翻 diff。
5. 用已知的坏例子撞一下验收标准。 他们把已修复的漏洞重新引入隔离版本，检查规格会不会放行。你至少可以对着曾经出过的回归、故意写错的断言、缺校验的分支跑一遍：坏的必须红，不能只看新功能是不是绿。
6. 结论旁边写范围和假设。 这份检查覆盖哪条命令、哪个构建、哪类输入；不覆盖哪些环境。写不清范围的「已验证」，和模型说「没问题」没有本质区别。
7. 自动检查跑不起来时，不要改成「先算过」。 这和 783 里控制面挂掉就拒绝、而不是放行，是同一类选择。CI 坏了、测试套件没跑、规格还没批准，就不能把合并或发布写成已验收。

一张极简对照表：

你现在怎么验收	它实际检查的是什么	它经常检查不到什么
Agent 回复「没问题」「测试都过了」	模型此刻的表述	规格是否够强、测试是否独立、坏例子会不会红
Agent 自己生成并执行的测试	它愿意覆盖的路径	它没写到的分支，以及被它写弱的断言
独立 CI / 类型系统 / 属性测试 / 定理证明器（对人审过的规格）	预先写明、可重复的硬条件	规格范围之外的环境与假设（所以范围必须写清）
人只看被标记处，同时审规格	机器过不了的地方，以及「到底在证明什么」	没被纳入规格、也没被工具标出来的问题

如果只能改一个习惯：下次 agent 交卷时，先问「验收标准是哪一份人审过的规格」，再问「硬检查是哪一套不由它自己说了算的工具」。两问都答不上来，就还没有验收，只是有一句「没问题」。

六、结尾：急停管停，验收管过

783 把急停从提示词里挪到集中瓶颈上；这一篇把验收从「模型口头保证」挪到「人审规格 + 机器硬检查」。一边是正在跑的 agent 还能不能继续产生副作用，一边是它已经写出的东西凭什么算通过。两边都不能把希望寄托在同一张嘴里。

独立开发者不必去复刻一套数百万行的 Lean 工程。DeepMind 这次工作最有用的地方，不是它宣布了「人只看约 1%」，而是它把可信与不可信拆开：规格和假设必须人审，证明可以交给 agent，最终是否成立交给 kernel。对我们日常的 harness，对应的只是一句更朴素的话：先写清要验收什么，再让独立的硬检查去跑；模型可以说「没问题」，但不能由它来宣布通过。

参考

• Google DeepMind（2026-11-10）：Introducing AlphaProof Code
• 技术报告（2026-11-10）：AlphaProof Code: Verifying Signal’s Security at the Machine-Code Level
• 公开产物：google-deepmind/code-verification
• 轻对照 · 本站 783：https://blog.zhoudw.vip/blog/783
• 轻对照 · 本站 778：https://blog.zhoudw.vip/blog/778

机制与数字均为 DeepMind 官方自述，本文未复现证明，也未把特定 CLI 构建上的结论写成 Signal 全产品的绝对安全保证。