AI生成代码激增，形式化验证成质量“守门人”
今年早些时候，谷歌CEO桑达尔·皮查伊披露，公司约75%的新代码由AI生成并经工程师审核；Anthropic数据显示，其入库代码中超过80%由Claude编写。不仅限于代码，AI数学公司Axiom Math近期宣布，团队指挥数十个AI智能体在24天内将数学史上篇幅最长的证明改写为4,310万行可供Lean检查的形式化代码。
产量飙升背后是质量隐忧。CodeRabbit分析470个开源项目发现，含AI编写的提交平均Bug数是纯人工提交的1.7倍。当AI产出速度远超人类审阅能力时，行业将目光转向拥有半个多世纪历史的“形式化验证”（formal verification）。该技术通过数学命题精确描述程序行为，并由可信检查程序确认，此前因成本高仅用于内核、加密库等关键领域，而AI的到来正在重构其经济性。
从“昂贵技艺”到“自动化标配”
传统软件测试通过大量输入运行来发现缺陷，但无法证明缺陷不存在。形式化验证则要求工程师先写下规格说明，再通过逻辑推理证明程序在任何输入下均满足性质。证明过程由Lean、Rocq、Isabelle等助手机械检查，一步出错即不通过。
&Truth联合创始人、新加坡国立大学教授伊利亚·谢尔盖比喻称，正如桥梁建造前需进行数学计算，代码也应如此。这项技术源于20世纪60年代，Coq前身发布于1989年，微软推出的Lean证明助手近年来被广泛用于数学定理形式化及软件验证。目前，波音飞机、亚马逊服务器及苹果设备中均有经过形式化验证的安全相关代码。
然而，高昂的成本和漫长的周期限制了其普及。seL4操作系统微内核验证项目投入约20人年才完成。苹果安全团队虽借此发现加密库深层问题，但不得不放慢新功能添加节奏。Antithesis创始人威尔·威尔逊直言，验证过程极其折磨人且未必能覆盖所有错误。以太坊创始人维塔利克·布特林也指出，形式化验证并非万灵药，但AI辅助的版本将是抵御AI驱动网络攻击的关键防线。
AI重构验证成本与效率
AI大幅降低了形式化验证的门槛。证明检查器的反馈非对即错，模型可反复尝试直至通过，无需依赖稀缺的人类专家。斯坦福大学博士生Chuyue Sun的研究显示，对于同一加密库，人类团队耗时8个月的工作，AI系统在给定顶层规格后仅需11.4小时和约467美元即可完成。
Anthropic与Theorem的合作展示了规模化潜力。双方选取123个开源库，由Claude针对编译后程序编写证明，确保其在特定环境下对任意不超过64MB的输入不崩溃。该项目耗时数周，生成1.8亿行证明代码，发现并修补了数百个躲过万亿次自动化测试的缺陷。若按传统方式，这需专家团队数年投入。
（来源：Anthropic）
Harmonic将其曾在IMO达到金牌水平的AI证明器Aristotle应用于C语言和芯片设计，在Tensordyne试用中发现了极难察觉的模块缺陷。Axiom在处理有限单群分类定理时，甚至在已发表40年的数学论文中找出34处错漏，并提供了替代论证。
资本涌入，赛道路线分化
过去一年，形式化验证从学术冷门变为资本热点。Axiom、Harmonic、&Truth和Pramaana Labs四家公司累计融资超6.5亿美元。
数学起步，降维打击软件验证
Axiom由洪乐潼创立，今年完成2亿美元A轮融资，估值超16亿美元。投资方Menlo Ventures看重其为未来每一行AI生成代码提供验证的市场潜力。Harmonic由Robinhood CEO联合创立，获英伟达、红杉等投资，估值达14.5亿美元。两家均先在数学竞赛建立能力指标，再将引擎推向软件和芯片客户。
通用验证机器与垂直领域应用
&Truth定位为基于Lean构建的“通用验证机器”，计划开源基础库，声称AI可将其提速百倍。Theorem则通过与Anthropic合作推出Claude技能插件，降低开发者上手门槛。Pramaana Labs面向医疗、法律等高风险领域，将规则转化为形式化知识库以检验AI决策的正确性。
（来源：&Truth）
中国团队也在加速布局。多家大模型公司开源基于Lean的定理证明模型，北京大学董彬团队利用AI智能体解决了悬置十余年的代数问题。不过，国内积累主要集中在数学证明侧，面向企业的软件验证产品尚处起步阶段。
信任机制的重构与挑战
尽管前景广阔，形式化验证仍存在局限。它只能证明代码符合规格说明，若规格本身存在漏洞，验证将“将错就错”。&Truth指出，在AI加速攻击的时代，“99%安全”等同于不安全。维塔利克认为，经数学证明的代码不会因攻击者变强而失守，这可能使攻防天平重新倒向防守方。
未来的软件信任体系可能不再依赖厂商信誉或长期运行记录，而是建立在可供独立检查的证明之上。人的价值将从编写代码和证明，转向定义“要证明什么”以及监督验证过程。
然而，新的风险随之而来：如果代码、规格说明和证明均由同一家公司的AI生成，可能形成“既当选手又当裁判”的循环论证，甚至出现AI编造公理的情况。因此，赛道的分水岭在于规格说明和证明标准的治理权归属——这决定了形式化验证将成为公共基础设施，还是被少数巨头掌控的认证服务。
注：封面/首图由 AI 辅助制作