Anthropic用Claude形式化验证123个开源库

Anthropic 旗下前沿红队（Frontier Red Team）与形式化验证机构 Theorem 合作宣布，其 Claude 模型成功编写出经机器校验的数学证明，证实来自 123 个开源软件库的编译代码在指定条件下绝不会发生崩溃。

在编写证明的过程中，Claude 还发现了多个潜伏多年、经历数万亿次常规测试仍未被发现的代码缺陷。Anthropic 表示，这可能是业内首次大规模利用 AI，在汇编代码层面对生产级软件实施形式化验证。团队认为，当前 AI 已能轻易发现并利用软件漏洞，单纯依赖传统测试已不足以保障软件安全。

从模糊测试到数学证明

研究团队以 Google OSS-Fuzz 项目中的模糊测试用例为起点，将其转化为形式化规范。验证设定的基准规则为：当代码编译为 RISC-V 机器码时，面对任何小于 64 MB 的输入数据均不得发生崩溃。

在数周时间内，Claude 针对 123 个开源库的 239 个入口点完成了上述证明。生成的证明代码总计约 1.8 亿行，采用 Rocq 证明语言编写，单份证明通常包含约 60 万行代码。由于 Rocq 证明检查器能够自动验证证明是否符合规范，开发者无需逐行人工审查生成出的代码。

Anthropic 正在公开部分证明文件以及背后的 RISC-V 与 Linux 语义模型。Theorem 也已推出开源验证计划，为符合条件的开源项目免费提供相同验证流程，并发布了专用的 Claude 技能扩展。

发现传统测试遗漏的缺陷

在编写证明时，Claude 发现了数百个隐藏缺陷，并在完成修复后才对修正后的代码进行最终证明。

例如，在一个解压程序中，Claude 发现了一个计数器下溢漏洞，该漏洞仅在特定格式、大小约 20 MB 的输入下才会触发越界写入。在另一个图像解码器中，它定位了一处需要 64 MB 输入并消耗超过 2 GB 内存才会触发的越界读取问题。此外，Claude 还重新发现了 libexpat 中的已知漏洞，并排查出一处文件加载权限限制未被正确执行的逻辑缺陷。

验证范围与实际局限

Anthropic 同时强调，完成上述证明并不等同于代码完全没有 Bug。

该验证基于特定假设条件：软件作为单线程静态二进制程序运行，具有固定内存预算，且环境为 Linux 操作系统下的 RISC-V 处理器架构。任何未覆盖的缺陷可能存在于形式化验证范围之外，或存在于受信任的基础组件中（如硬件与操作系统模型、定理陈述本身以及 Rocq 检查器）。实际生产环境中，多数系统部署在其他处理器架构及不同配置下。

即便如此，Anthropic 认为软件安全验证的成本效益正在改变，并建议此前在弱能力模型上尝试形式化验证受挫的开发者重新评估这一路径。