10月23日，Anthropic与Theorem Labs团队联合发布了一份题为《大模型正让形式化软件验证在更大规模上变得可行》的研究报告。报告显示，Claude模型针对123个开源软件库中的239个程序入口，生成了约1.8亿行Rocq证明代码，并在此过程中发现并修复了数百个Bug，其中包括一些历经数万亿次测试、在多年运行中一直未被发现的漏洞。
该研究在开发者社区引发广泛关注，核心原因在于其将形式化验证推进到了汇编指令层面，以RISC-V指令集为基础进行证明。Anthropic方面表示，这是首次大规模利用AI在汇编代码层面将形式化验证应用于生产软件，让以往被认为不切实际的需求成为现实。
形式化验证与传统的漏洞扫描存在本质区别。传统安全测试无论执行多少次，都难以穷尽所有可能的输入与运行状态，因而无法完全避免漏洞残留。形式化验证则通过数学证明，确认程序在给定条件下满足特定的安全性质。过去，这项工作高度依赖专业人员，成本高、耗时长，难以大规模应用于普通软件。研究显示，随着大模型能力的提升以及Agent调用、主动执行任务能力的增强，形式化验证的规模化应用具备了可行性。
从行业背景看，网络安全形势正在快速恶化。10月中旬以来，重大安全事件频发：编程智能体OpenCode遭攻击泄露用户第三方模型密钥；全球近七成网站使用的PHP开源编程语言被曝出重大漏洞，导致不少网站关停。Axios报道称，AI Agent正在对美国银行系统发起攻击，速度超过金融机构的反应能力，摩根士丹利、美国银行等机构均在加急处理。Anthropic方面指出，大多数软件都存在漏洞，AI现在可以轻松发现并利用这些漏洞，主流的网络防御手段已无法满足要求，行业更需要能够证明代码无漏洞的可靠方法。
将安全检查前移至开发阶段，是该研究指向的重要应用方向。通过在代码上线之前完成验证，企业有望在漏洞被攻击者利用之前发现问题，而非在事件发生后紧急补救。这对于依赖开源组件构建业务系统的企业服务厂商和SaaS提供商具有直接意义，第三方依赖的安全性问题长期是软件供应链中的薄弱环节。
不过，形式化验证并不等同于证明整个软件绝对安全。它只能证明程序在特定假设、约束和验证范围内满足预设性质。如果规范本身存在缺陷，或验证范围之外仍存在漏洞，攻击者依然可能找到突破口。对于复杂软件系统而言，如何确定验证目标、处理第三方依赖，以及将修复方案安全部署到生产环境，仍需大量工程工作。
攻防双方的成本不对等是更现实的挑战。攻击者只需找到一个可利用的漏洞即可获得入侵机会，防御者却必须保护整个系统，不仅要发现漏洞，还要判断风险、验证修复，并避免修复过程引入新问题。即使AI大幅压低了漏洞发现与代码验证的成本，防御方也无法立即完成全部工作。此外，部分开发者提出，形式化验证可能拖慢开发速度，在AI驱动软件开发持续提速的背景下，为安全而减速可能演变为现实中的两难选择。还有开发者担心，AI生成的证明策略可能产生人类难以审查的冗长证明，最终脱离可监测、可管控的范围。
尽管存在上述限制，开发者社区对这项研究的讨论整体偏向乐观。知名AI与Web技术博主Pratham表示，这可能是目前AI所取得的成就中明显被低估的一个，随着网络安全问题变得更加棘手，行业尤其需要在这一领域取得更多进展。从企业服务市场的角度看，若形式化验证能够借助大模型实现成本下降和流程标准化，安全能力有望从独立的安全产品向内嵌于开发工具链的基础能力演进，进而影响DevSecOps工具链和软件供应链安全市场的竞争格局。
该文观点仅代表作者本人，企服科学平台仅提供信息存储空间服务。
