谷歌 Gemini 4 Carbon 在 11 月 10 日至 11 日完成全球全量开放，定价低于同代的 Claude Fable 5.2 与 Opus 5.5，这是它在商业层面的第一步。紧接着，DeepMind 公布了这个模型的第一个重量级用例——不是写代码，而是证明代码。
项目叫 AlphaProof Code。它做的事可以一句话概括：用 AI 智能体为 Signal 加密协议的核心实现生成机器可检的安全证明。
为什么是「证明」而不是「测试」
软件质量的常规手段是测试：写用例、跑覆盖、看有没有挂。测试能发现错误，但无法证明没有错误——它只能覆盖你想得到的情况，想不到的路径永远测不到。
形式化验证走的是另一条路：把「这段代码必须满足什么性质」写成数学命题，再用逻辑推导证明它成立。证明一旦通过机器检查，就等于覆盖了所有可能的输入，而不是抽样。代价是极高的人力成本，一个中等规模系统的完整证明往往需要数人年。
航空、航天、芯片、轨道交通这些领域用这套方法几十年了，互联网基础设施基本没用——太贵。Signal 这样的加密协议恰好是最该用、又最用不起的典型：它的安全性直接决定数亿人的通信隐私，但重写一遍带证明的实现，此前没有商业团队愿意投入。
这次做了什么
流程分两段，人和模型各管一段。
第一段是人：研究人员把 Signal 协议的安全目标写成 Lean 规格。Lean 是一个交互式定理证明器，也是数学形式化领域最活跃的语言之一。规格约 2.6 万行，逐条审核，确保「要证的东西」本身没错。
第二段是模型：由 Gemini 4 Carbon 驱动的智能体自动生成证明，一路验证到编译后的 AArch64 机器码。这一步很关键——很多形式化验证只证到源代码层，而真正跑在手机上的是编译器输出的机器码，编译器本身可能有 bug。证到机器码，意味着信任链条覆盖了编译环节。
结果：约 650 万行 Lean 证明，全程约四周，仅约 1% 的代码需要人工复核。
反向测试
光有「证出来了」还不够，还要证明这套流程真的能发现问题。团队做了个聪明的实验：把那两个历史上真实出现过的漏洞重新植入实现，再跑一遍证明流程。
两次系统都给出了「不安全」的结论，而且这个结论本身是机器可检的——不是模型说「我觉得有问题」，而是一份能被 Lean 检查器验证的反例证明。
这一步的意义在于排除了「证明是编出来的」这种可能。AI 生成证明最大的风险是幻觉：模型可能生成看起来合理、实则通不过检查的推导。既然植入漏洞后能被抓住，说明流程在真实地工作。
为什么这件事重要
第一，它把形式化验证的成本结构改了。过去这项工作的瓶颈是「会写证明的人太少」，现在瓶颈变成「规格写得对不对」——前者是人力规模问题，后者是判断力问题。人力可以靠模型摊薄，判断力不行。
第二，它给出了 AI 可信性的一条新路径。当下的对齐研究大多在行为层做文章：让模型别说错话、别做危险操作。形式化验证走的是另一条：不管模型内部怎么想，它输出的东西必须通过数学检查。对关键系统来说，后者更可靠。
第三，它对「AI 写代码」这件事提出了新标准。现在的编程智能体以「任务通过率」论英雄，但通过测试不等于正确。当证明工具变得便宜，「这段代码有证明」可能会成为基础设施软件的新门槛。
边界在哪
DeepMind 自己的表述很克制：证明的目标由人设定，模型只负责找路径。换句话说，「该证什么」仍然是人的判断。如果规格写漏了一条性质，证明再完美也保护不了那条性质——这是形式化验证的老问题，AI 并没有解决它。
另外，四周、650 万行证明，是 Signal 协议这个特定规模的结果。换成操作系统内核、数据库引擎这类体量，成本会非线性上升。这套方法短期内不会普及到普通业务代码。
还有一个现实约束：Lean 生态的成熟度。规格与证明都依赖库，库不全就得自己补，这部分工作量无法由模型自动完成。
接下来会看到什么
最可能率先跟进的是三类系统：加密与身份认证、共识协议、以及安全关键的嵌入式固件。它们的共同点是规模可控、性质清晰、出错代价极高。
对普通用户来说，这件事的直接感受可能是零。但它决定的是另一个问题：当越来越多的基础设施由 AI 参与编写，我们凭什么相信它是对的。答案是——不凭什么，除了证明。