谷歌Anthropic七成代码交给AI，谁来验对错？形式化验证翻红

今年早些时候的谷歌云年度大会上，谷歌 CEO 桑达尔·皮查伊（Sundar Pichai）透露，公司大约 75% 的新代码出自 AI 之手，之后再由工程师审核批准。Anthropic 的内部数据则显示，其入库代码中已有 80% 以上是 Claude 写的。

AI 批量产出的不只是代码。10 月 26 日，AI 数学公司 Axiom Math 宣布，团队调度数十个 AI 智能体，花了 24 天，把数学史上篇幅最长的证明完整改写成可交给证明助手 Lean 逐步检查的形式化代码，长达 4,310 万行。

产量上去了，质量问题跟着来。开发者的拉取请求（pull request，即提交代码修改的申请）里，有 AI 参与编写的提交，平均 bug 数是纯人工提交的 1.7 倍。

AI 写代码、写证明的速度早已超出人类逐行审阅的能力，那谁来检验它们对不对？

行业把目光投向了一项有半个多世纪历史的技术：形式化验证（formal verification）。它的做法是先写清"程序应该做什么"，将其表述为精确的数学命题，然后构造证明，交给一个很小但可信的检查程序确认。

过去成本太高，形式化验证长期只在操作系统内核、加密库、芯片设计等少数领域使用。AI 来了，这项技术的经济账被直接改写。

8 月，规格说明和证明。

近期，AI 结合形式化验证的赛道正加速升温：Anthropic 与初创公司 Theorem 联合发布了用 Claude 对开源库做形式化验证的研究；美国 AI 数学公司 Harmonic 把其 AI 证明器用到 C 语言程序和芯片设计上；专注 AI 代码验证的 &Truth 10 月 29 日结束隐身，宣布拿到 7,000 万美元种子轮融资。

这项老技术为何突然翻红，它又能否真正化解 AI 时代的验证难题？

正确，但太贵

软件测试的通行做法，是挑大量输入去跑程序，看会不会出错。这样能找出缺陷，却证明不了缺陷不存在。形式化验证换了个思路：工程师先写下规格说明，再用逻辑推理证明程序在任何输入下都满足这条性质。

证明交给 Lean、Rocq、Isabelle 等证明助手机械检查，错一步就过不了。&Truth 联合创始人兼首席科学官、新加坡国立大学（NUS）副教授伊利亚·谢尔盖（Ilya Sergey）在接受《连线》（WIRED）采访时打了个比方：桥梁和楼房不会倒塌，是因为人们在建造之前做了数学计算，代码也应该如此。

这些工具的历史比很多人想象的更长。20 世纪 60 年代末，荷兰数学家德布鲁因（N.G. de Bruijn）开发出第一个能由计算机逐步检查数学证明的系统 Automath；几乎同一时期，

这两条技术路线之后慢慢走到了一起，同一套工具如今不但能校验数学定理，也能对软件做验证。Coq 是 Rocq 的前身，1989 年就已发布；眼下 AI 圈里热度最高的 Lean，则是微软研究院十几年前带来的证明助手，起初更多是为程序验证而设计，后来被大量数学家拿去把证明形式化。

其实这套做法早就走出了实验室。波音飞机的系统、亚马逊的服务器，还有超过 25 亿台在用的苹果设备，其中都跑着至少一部分经过形式化验证的软件，且多为安全相关代码——这类代码一旦被攻破，后果往往很严重。

那为什么不把全部代码都拿去做形式化验证？卡点主要在成本和周期上。五十多年里工具一直在迭代，可形式化验证始终是少数专家手里的技艺。业内被视为里程碑的 seL4 操作系统微内核验证项目就是个例子：前后投入约 20 人年（相当于 1 个人全职干 20 年）才做完。

苹果安全团队说过，形式化验证在他们加密库里揪出过其他手段发现不了的问题，但代价是新代码得放慢添加速度，验证才追得上。多家中型科技公司则最多只验证过产品里个别核心功能，招不到验证工程师、投入风险大、验证周期拖慢产品迭代，都是原因。

也有专家对这条路心存警惕。做缺陷挖掘的初创公司 Antithesis 创始人威尔·威尔逊（Will Wilson）就说，形式化验证是数学爱好者容易踩进去的"陷阱"。Antithesis 曾砸下数百万美元验证自家部分网络安全防线，整个过程"极其折磨人"，结果验证做完，公司自己的测试工具还是找出了额外错误。

以太坊（Ethereum）创始人维塔利克·布特林（Vitalik Buterin）今年 5 月在个人博客发过长文，他认为形式化验证并非万灵药，但同时也指出，AI 辅助的形式化验证会成抵御 AI 驱动网络攻击的关键防线。

AI 改写了成本账

AI 正在让形式化验证变得没那么难、也没那么贵：证明检查器给出的反馈非对即错，模型可以一遍遍试，失败就换个写法，最后过不过由检查器说了算，模型没法蒙混过关。

过去，卡住这项技术的是专家和人力，如今，大量繁琐的证明工作可以直接交给模型。

Anthropic 与 Theorem 的合作，让人看到了这项技术规模化的可能。双方从谷歌维护的开源测试项目里挑了 123 个开源库，把现成测试用例改写成规格说明，再让 Claude 直接对着编译后的程序写证明，证明在特定运行环境下，无论输入是什么、只要不超过 64MB，程序都不会崩溃。

整个项目花了几周，产出约 1.8 亿行证明代码。Claude 在证明途中发现并修补了数百个缺陷，其中有些连数万亿次自动化测试都没能拦住。换传统做法，这种规模的工作得让专家团队干上好几年。

Harmonic把AI证明器Aristotle的数学能力直接搬到了软件工程上。Aristotle曾在2025年国际数学奥林匹克（IMO）拿到金牌水平，10月27日起被用来验证C语言程序和芯片设计。AI芯片公司Tensordyne的试用中，团队公认最难验证的模块里，它挖出了藏得很深的缺陷。

Axiom的有限单群分类定理（CFSG）证明项目，则说明这套工具链扛得住极其复杂的推理。逐行翻译时，智能体在已发表的证明中揪出34处错漏，最严重的一处来自1986年的一篇关键论文，智能体还给其中一个断言找到了明确的反例。这个错误在数学界存续了约40年，所幸没有推翻定理本身，Axiom的系统随后补上了替代论证。

资本押注，路线分化

一年之间，形式化验证从学术圈的冷门方向，变成了资本争相下注的热门赛道。Axiom、Harmonic、&Truth和Pramaana Labs四家主要玩家，累计融资已超过6.5亿美元。

融资最多的两家，起点都是数学。Axiom由洪乐潼（Carina Hong）创办，去年拿了6400万美元种子轮，今年又完成2亿美元A轮融资，投后估值超过16亿美元。投资方Menlo Ventures说得很直白：他们看中的不是规模只有几十亿美元的传统形式化验证市场，而是未来每一行AI生成代码都要验证的机会。

Harmonic则由美国券商Robinhood CEO弗拉德·特涅夫（Vlad Tenev）联合创立，英伟达（NVIDIA）旗下风投、红杉资本（Sequoia Capital）等参投。2025年11月完成1.2亿美元融资后，估值达14.5亿美元，累计融资约2.95亿美元。

两家公司的路子差不多：先在数学竞赛和定理证明上攒出可量化的能力指标，再把跑通的证明引擎卖给软件和芯片客户。

另一批公司则从软件安全切进来。公益公司（public benefit corporation，在章程中承诺兼顾公共利益的营利性公司）&Truth今年年初成立，联合创始人包括斯坦福大学教授克拉克·巴雷特（Clark Barrett）和伊利亚。前文提到的Chuyue Sun也是克拉克的学生，今年8月已加入公司。

&Truth想做一台能读懂任何编程语言代码的“通用验证机器”，基于Lean构建，基础库计划开源。公司称，AI能把形式化验证提速至少100倍，自家的证明自动化技术还能再快100倍。

与Anthropic合作的Theorem规模小得多，2025年走出Y Combinator。今年10月，双方联合发布了Claude技能插件，帮开发者自己上手做验证。近期，一位在微软研究院（Microsoft Research）干了20多年的资深研究员也离职创业，成立了形式化验证公司Truidic。

医疗、法律这类领域，检验AI回答对不对至关重要，这活同样能交给形式化验证。Pramaana Labs今年6月拿到2,700万美元种子轮融资，客户是在高风险业务里用AI辅助决策的机构。它的做法是用Lean把税务、法律、医疗等领域的规则写成形式化知识库，再核对AI的答案是否合规。

国内这边同样有人下场。多家大模型公司把基于Lean的定理证明模型放到了开源社区；北京大学董彬教授团队今年借助AI智能体，攻克了一个搁置十余年的代数难题，完整的证明还由系统自动生成，可直接交给Lean核验。只是这些工作的重心多落在数学证明上，真正面向企业客户的软件验证产品，目前仍处于起步阶段。

放眼全球，这条赛道的商业模式仍不清晰。两位没有相关经验的网络安全高管对《连线》（WIRED）表示，就算AI能把验证自动化，他们也拿不准值不值得投，但可以考虑直接向大模型公司买“经过验证”的AI代码。

需求端的信号也确实有：长期做传统验证服务的Proofcraft表示，近期咨询量远超他们和同行能接的规模。资本、技术、需求都齐了，但形式化验证到底能给出多大程度的保证，还得谨慎看。

证明了什么

形式化验证给出的“担保”有边界。它能证明代码符合规格说明，可规格说明本身有漏洞的话，验证过程也会将错就错。

更何况，AI写代码变快，找漏洞也变快。&Truth在成立声明里写道，AI正以超越人类的速度攻破代码，这个时代“99%安全”就等于不安全。

不少人觉得，AI让黑客如虎添翼，网络安全注定守不住。维塔利克却不这么看：经过数学证明的代码，不会因为攻击者变强就失守，形式化验证有可能让攻防天平重新倒向防守一方。它或许会成为AI时代软件安全的底线。

过去人们信一款软件，靠的是厂商信誉、代码审查和长期运行记录；今后，越来越多的信任可能落在一份谁都能独立检查的证明上。

人的角色也跟着变：写代码、写证明可以交给机器，但到底要证明什么、谁来定义、谁来监督，仍是人必须回答的问题。

这里还埋着一个更隐秘的新陷阱：写代码的是AI，写规格说明和证明的也是AI，而这些AI又出自同一家公司，“经过验证”就可能沦为既当选手又当裁判的循环论证，一些AI系统甚至可能自己编出不成立的公理，把论证凑完。

所以这条赛道真正的分水岭，也许不在验证速度，而在规格说明和证明标准的治理权归谁。它决定形式化验证最终是人人可查的公共基础设施，还是少数公司手里的认证服务。

参考内容： 
https://www.wired.com/story/software-verification-is-the-hot-new-answer-to-the-ai-safety-crisis/

https://www.anthropic.com/research/formal-verification

https://arxiv.org/abs/2608.00965

https://axiommath.ai/research/the-enormous-theorem-formalized/

https://www.startupresearcher.com/news/harmonic-expands-aristotle-to-software-and-hardware-verification

http://andtruth.com/press/andtruth-emerges-from-stealth/

注：封面/首图由AI辅助制作