AI改写验证成本，形式化验证赛道升温

今年以来，谷歌披露约四分之三新代码由人工智能生成并需工程师审核；安思罗皮克称入库代码超八成由模型编写。代码审查初创企业科德拉比特分析470个开源项目发现，模型参与提交平均缺陷数为纯人工1.7倍。人工智能使代码与数学证明产量激增，人类逐行审阅承压，拥有半个多世纪历史的形式化验证重新升温。该技术支持把程序行为写成数学规格，再经证明助手机械检查，过去因成本高只用于内核、加密库、芯片等关键系统。 人工智能正大幅降低验证门槛。斯坦福博士生孙初月称，某加密库人类验证需五人八个月，模型在给定顶层规格后11.4小时、约467美元补全证明。安思罗皮克与初创公司定理用模型验证123个开源库，数周生成约1.8亿行证明代码并修补数百缺陷。美国公司公理将超长数学证明改写为4310万行可检查代码，并发现历史证明错漏；哈莫尼克把证明器用于底层程序与芯片设计；专注代码验证的真理公司结束隐身并获七千万美元种子轮融资，主要玩家累计融资超6.5亿美元。中国团队亦进入定理证明与自动验证。 但形式化验证存在局限：它只证明代码符合规格，无法保证规格本身正确；智能体也会加速攻击。更隐蔽风险是，代码、规格、证明若由同一模型生成，验证或沦为闭环认证。赛道关键将转向规格与证明标准的治理权，决定其成为公共基础设施还是厂商认证服务。