Anthropic用Claude实现大规模形式化验证

在最新研究中，Anthropic旗下Claude模型找到了历经数万亿次测试仍未被发现的软件Bug，并首次在生产级软件中跑通了大规模形式化验证。

AI正在重塑软件开发的各个环节，但在网络安全防御侧，局势却长期处于劣势。随着AI生成代码带来潜在隐患，黑客又能低成本利用AI大批量挖掘系统漏洞，传统安全团队疲于应对。在此背景下，Anthropic与Theorem Labs团队发布题为《大模型正让形式化软件验证在更大规模上变得可行》（LLMs are making formal software verification feasible at a much larger scale）的研究报告，在开发者生态引发广泛讨论。

从“模糊查虫”走向“数学证明”

根据研究报告，Claude模型针对123个开源软件库中的239个程序入口，自动生成了约1.8亿行Rocq证明代码，成功排查并修复了数百个Bug。其中部分缺陷在生产环境中运行多年，历经数万亿次传统测试却始终未暴露。

该研究的核心突破在于将形式化验证推进到了汇编指令层，基于RISC-V指令集完成端到端的数学证明。

在传统网络安全中，AI主要用于辅助测试和查找漏洞，但再高频的测试也无法穷尽极端边界情况。形式化验证则通过严谨的数学推导，证明程序在既定约束下百分之百符合特定的安全规格。以往形式化验证极度依赖顶尖数学家与工程师，成本高昂且效率低下，难以应用于主流软件开发。大语言模型与AI智能体（Agent）能力的演进，使得这种复杂的证明工作首次具备了规模化落地的现实基础。

防御方能否彻底扭转攻防失衡？

通过大规模形式化验证，安全团队能将代码审计关口大幅前移到开发阶段，消除潜在隐患。然而，这并不意味着攻防天平能瞬间逆转：

1. 形式化验证的局限性：形式化证明只能确保代码在预设规范与边界条件内的正确性。若安全规范本身存在定义盲区，或威胁来自系统边界之外的第三方依赖，系统仍面临被攻破的可能。
2. 攻防成本不对称：黑客只需找到一处缺口即可实施入侵，防御方则需证明全系统的无死角安全。即便大语言模型显著降低了写证明的成本，修补、验证与生产环境部署的复杂工程量依旧庞大。
3. 开发节奏与工程信任：形式化验证可能拖累软件迭代速度。同时，AI生成的大规模机器证明极其冗长，人类工程师难以逐行审查，如何确保模型生成的证明策略自身没有漏洞，也是未来需要持续面对的工程课题。

尽管完全解决网安失衡尚需时日，但AI驱动形式化验证的突破，正标志着软件工程正在迈入以“机器证明安全”替代“被动修补漏洞”的新阶段。