大语言模型让大规模形式化软件验证成为现实

软件漏洞问题长期困扰着整个行业。即便是 Linux 内核这样经过数十亿设备大规模部署和严格测试的成熟软件，近期仍披露了超过 1000 个安全漏洞。随着前沿 AI 模型越来越擅长将看似无害的小漏洞串联成高危攻击链，传统的测试与防御手段已难以应对新的威胁格局。形式化验证提供了一种从数学层面证明代码正确性的方法，但其高昂的人力成本使其长期局限于航空电子等极少数关键任务场景。

形式化验证的核心挑战在于规模与成本。以 seL4 操作系统内核为例，实现该内核仅需约两个人年，而对其进行完整的形式化验证却耗费了约 20 个人年。证明文件往往比原始代码大出数倍，且编写过程需要极为专业的数学与逻辑背景。正因如此，这一技术在过去几乎只出现在 Airbus 航电系统等极少数预算充裕、容错率极低的领域，普通开源项目根本无力承担。

大语言模型的出现正在改变这一局面。Anthropic 研究团队让 Claude 对 123 个开源库的 RISC-V 汇编代码进行形式化证明，验证目标是：在所有小于 64 MB 的输入、所有建模的 Linux 操作系统响应及内存布局下，程序始终能正常退出而不触发内存安全错误或断言失败。这一验证范围覆盖了数以万计的汇编指令在任意输入下的所有可能行为，是此前被认为难以实现的计算规模。

在生成证明的过程中，Claude 还意外发现了多个长期潜伏的漏洞——这些漏洞在经历数万亿次模糊测试后仍未被发现。研究团队采用的方法是将现有的可编译测试套件自动转换为形式化规范，以「测试套件始终通过」作为验证规则，再结合通用的 RISC-V 二进制执行模型进行证明。这种将模糊测试入口点转化为形式化证明起点的思路，为大规模自动化验证提供了可复用的工作流程。

除汇编代码验证外，研究团队还探索了形式化验证在其他场景的应用，包括评估 zlib 压缩算法的安全性、证明 Rust 编写的 Python 解释器的行为等价性，以及排查关键软件中长期存在的深层漏洞。Theorem 已宣布将为其他开源项目提供相同的验证流程，并发布配套的 Claude 技能工具，帮助开发者快速上手代码验证。随着模型能力持续提升，形式化验证的成本将进一步下降，有望成为安全软件开发的标准环节。

要点

• Claude 完成了首个针对生产级汇编代码的大规模 AI 形式化验证项目，覆盖 123 个真实开源库。
• 在生成形式化证明的过程中，Claude 发现了多个经历数万亿次模糊测试仍未被检测到的隐藏漏洞。
• 研究团队将现有测试套件自动转化为形式化规范，大幅降低了形式化验证的准入门槛。
• 随着模型能力提升和证明复用机制成熟，形式化验证的边际成本将持续下降，有望进入主流开发流程。
• Anthropic 已公开部分证明及 RISC-V 语义，Theorem 同步提供开源项目验证服务和开发者工具。