别让模型给模型打分：AlphaProof Code 把判定权交给了 Lean

11 月 10 日这天，Google 一口气放了两件事。一件是 Gemini 4 Carbon 全面开放，开发者、企业、科研人员、普通用户都能用。另一件没那么热闹：DeepMind 公布 AlphaProof Code，用一群智能体给 Signal 协议实际运行的代码写形式化证明，每一行都由 Lean 检查。

我更想聊第二件。因为它碰到了一个这两年一直被绕开的问题：AI 干完的活，到底谁说了算。

把验证从设计稿推到编译后的机器码

先说清楚它做了什么。DeepMind 官方博客把 AlphaProof Code 定义成一个结合人类专家与 AI 智能体的多模型框架。分工很干净：人决定「要证什么」，把安全目标翻成形式化规格，并且逐份审核；智能体负责写证明；每一份证明都必须过 Lean 的检查，过不了就是过不了。

验证对象不是白板上的协议设计，而是 Signal 协议的实际代码。官方技术页写得更具体：证明覆盖后量子 PQXDH 握手和 Triple Ratchet，建立前向保密、认证、妥协后安全和握手保密；针对的是编译后的二进制，不是纸面推导。官方说这是首批把协议级安全保证连到未修改实现代码上的证明。

规模也摆在那儿。官方技术页说智能体生成了约 650 万行经机器检查的 Lean 证明代码，底下垫着约 2.6 万行必须人工信任的规格与 AArch64 语义。DeepMind 博客给的说法是「超过六百万行」，两边对得上。整件事只用了四周，官方说这类工作过去要专家团队干几年。智能体标出来需要人再看一眼的部分，只占代码库的 1%，其余交给 Lean。

最让我服气的不是行数，是一个反向测试。团队把两处此前修好的真实漏洞，重新植回隔离出来的 Signal 代码副本。两次，系统都给出了机器检查过的「这版不安全」的证明。一个只会点头说「看起来没问题」的系统没有价值；这个系统能说不，而且拿得出凭据。

值得抄的不是 Lean，是分工

现在很多智能体工作流的验收方式是：让另一个模型读一遍输出，打个分。这套做法便宜，也脆。模型打分能被恭维，能被绕开，能被一段自信的输出带偏。Lean 不吃这一套，它只认能不能通过检查。

所以真正可迁移的，是把「生成」和「判定」拆开。判定那头尽量交给不可说服的东西：编译器、类型系统、测试、形式化 kernel。人把稀缺的注意力留给最前面那一步，到底要证什么，以及哪些假设可以信。这个分工比任何具体工具都值钱。

但也别把话说满。信任问题没有消失，只是挪了位置。规格是人写、人审的；没写进规格的性质，一个字都没被证明。官方博客用的是「关键安全属性」，举例是设备在临时失陷前后消息仍受保护，可没说整个应用、全部属性都验过了。文章自己也写着，把这套方法放大到别的系统还需要继续研究。所以「Signal 已被形式化验证」是过头话，准确说法是「这层代码满足这批规格」。

还有一层得记着：上面所有数字都来自 Google 自己的发布材料，没有第三方独立复核。写进结论之前，先在心里给它们标个「厂商自测」。

顺手记一条实操信息：Carbon 开放了，但价格有期限

同一天 Google 官方博客宣布 Gemini 4 Carbon 开放。开发者走 Google AI Studio 和 Android Studio 的 API 付费档，Google AI Ultra 订阅者能在 AI Studio 和 Antigravity 里试。官方还在 Antigravity 预览了 /swarm，一条指令变成一组可实时追踪的智能体，Carbon 放在架构设计、协调、审计这类最费推理的位置，旁边配更快更轻的模型和逐改动做测试的对抗式验证器。

价格得看仔细。官方博客写明引入期与 Gemini 4 Argon 相同：输入每百万 token 2 美元，输出 10 美元。脚注说引入期 11 月 30 日到期，之后变成输入 4 美元、输出 20 美元，而且只适用于面向公众开放的 Carbon 模型。如果你打算把长任务智能体迁过去，别拿引入价做长期预算。

官方自测也一并看：模拟攻击测试里拦截了 99% 的攻击轨迹，一项 375 项任务的智能体诚实度基准通过 92%，Argon 是 70%。数字挺好看，出处是厂商自己。

同一天，一边把更强的模型放出来，一边把「怎么证明它没乱来」摆到台面上。后者没那么好传播，却更该被抄走。下次搭智能体流程，先想清楚判定权交给谁，再谈生成速度。