形式化验证：半个世纪前的“代码验算”技术，为何被AI捧红？

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

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

产量上去了，随之而来的是质量问题。代码审查公司 CodeRabbit 分析了 470 个开源项目的拉取请求（pull request，开发者提交代码修改的申请），发现有 AI 参与编写的提交，平均 bug 数是纯人工提交的 1.7 倍。

当 AI 生产代码和证明的速度已经远超人类逐行审阅的能力，谁来检验它们是对的？

行业将目光转向了一种有半个多世纪历史的技术：形式化验证（formal verification）。它先把“程序应该做什么”写成精确的数学命题，再构造证明，交给一个很小但可信的检查程序确认。

此前由于成本太高，形式化验证长期只用于操作系统内核、加密库、芯片设计等少数领域。但 AI 的到来，直接改写了该技术的经济性。

8 月，斯坦福大学博士生 Chuyue (Livia) Sun 在预印本论文中报告：对于同一个加密库，人类主导的验证工作由 5 名主要贡献者花了 8 个月；而给定顶层规格后，他们的 AI 系统仅用 11.4 小时、花费约 467 美元，就自动补全了其余全部规格说明和证明。

近期，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；几乎同一时期，图灵奖得主托尼·霍尔（Tony Hoare）等计算机科学家提出了用逻辑规则证明程序正确的方法。

两条线后来逐渐汇合，同一套工具既能检查数学定理，也能验证软件。Rocq 的前身 Coq 发布于 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 在证明过程中发现并修补了数百个缺陷，其中一些躲过了数万亿次自动化测试。按传统做法，这种规模的工作需要专家团队投入数年。

（来源：Anthropic）

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）

&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 辅助制作