Anthropic 称 Claude 为 123 个开源库完成安全属性形式化证明

Anthropic 于 2026 年 10 月 22 日发布研究，称与 Theorem 合作，Claude 为 123 个开源库中 239 个 fuzz 测试入口在 RISC-V 汇编代码层面生成了机器可检验的安全属性形式化证明。

据 Anthropic 称，Claude 修补了其发现的漏洞，随后证明：对于 64 MB 以下的任意输入，以及所有建模的 Linux 操作系统响应和内存布局，这些程序将始终正常退出，不会触发内存安全错误或断言失败。这些证明假设程序以单线程静态二进制形式运行，在采用 Linux 的 RISC-V CPU 上具有固定内存预算。Anthropic 表示，这些证明总计约 1.8 亿行 Rocq，典型证明约 60 万行，覆盖的二进制中位长度为 1.8 万条 RISC-V 指令。该公司称，据其所知，这是首次大规模利用 AI 在汇编代码层面对生产软件应用形式化验证。

部分证明及其背后的 RISC-V 与操作系统语义正在 GitHub 上发布。Anthropic 表示，还将发布为该项目构建且尚未公开的可信组件、无需修补的 fuzz 测试的完整证明，以及无法证明的 fuzz 测试的规范，但会保留可能暴露未修补漏洞的证明。

该方法将每个库现有的可编译模糊测试转换为一个形式化规范，该规范编码了一条规则：对于任何小于 64 MB 的输入，测试都不会崩溃。该规范基于编译后的 RISC-V 指令定义，使用 Theorem 对 RISC-V 指令集和 Linux 进程的形式化语义，并由 Rocq 证明检查器根据规范验证每个已完成的证明。Anthropic 表示，这样一来，开发者只需信任三个组件：RISC-V 和 Linux 进程的形式化模型、精确的定理陈述，以及 Rocq 检查器本身。

Anthropic 表示，它已将这一流程应用于 Google OSS-Fuzz 计划中的数百个项目。该计划为符合条件的开源项目提供持续的模糊测试，并自动为 C 和 C++ 程序插桩 AddressSanitizer；一旦发生不当内存访问，该工具就会使程序崩溃。一份日期为 2026 年 10 月 22 日的附录详细说明了所证明的完整定理：对于所有小于 64 MiB 的输入和所有内存布局，无论是经 ASan 插桩的二进制文件还是普通二进制文件，都不会发生故障、中止或表现出未建模的行为，并且两者产生相同的读写轨迹、退出行为和最终文件系统状态。

该附录指出，在这一工作中，Claude 编写了约十亿行 Rocq 代码，其中约 1.8 亿行通过了证明检查器；cJSON 的 391 行解析器入口点获得了 63 万行的证明，而链接了 5.1 万行的 fftw3 则获得了 48 万行的证明。由于允许 Claude 在完成证明之前修补代码，Anthropic 表示它对修补行为进行了惩罚，对证明修补改变了哪些输入给予额外加分，并记录和审计修补内容，以遏制奖励黑客行为。

证明尝试期间发现的缺陷

Anthropic 报告称，尝试进行这些证明的过程中发现了数百个缺陷，其中许多是模糊测试器不太可能发现的。在证明某个库的入口点时，Claude 发现了一个解压器中的计数器下溢，该下溢会导致越界写入，但仅在输入约为 20 MB 且具有一种罕见、特定布局时才会发生。其他发现包括：一个图像解码器中的越界读取，需要 64 MB 输入和超过 2 GB 内存；一个越界读取，需要在同一文件的两个句柄之间进行特定调用序列；以及在 libexpat 中重新发现 CVE-2026-56132，该漏洞需要深度嵌套的输入。

Claude 还发现了从不导致崩溃的逻辑缺陷，包括对应用程序可加载哪些文件的限制并非总能得到执行。Anthropic 表示，对几个广泛使用的关键应用程序进行验证尝试时，发现了一个此前未知、已潜伏十多年的逻辑缺陷；并且在验证一个广泛使用的 PDF 阅读器的过程中，它在一周内发现的安全缺陷数量与通常一年报告的数量相当。

其他实验与效率发现

除了 OSS-Fuzz 之外，Anthropic 还让 Claude 为定义 zlib 压缩格式的技术文档 RFC 1950 编写一份形式化规范，然后证明 Linux 内核的 zlib 实现正确地实现了该规范。Claude 直接证明了 x86 编译的二进制文件，使用的是 Claude 生成的 x86 指令集形式化语义；Anthropic 表示，它对另外六个广泛使用的库重复了这一过程，发现了轻微、不可利用的边角情况缺陷，这些缺陷正在向上游提交。该公司还报告称，生成 x86 语义的过程中，在官方参考文档中发现了数百处错误，并在硬件本身中发现了少量缺陷；并且，单步执行这些语义可以在 Linux 内核上启动一个 Ubuntu 用户空间。

在另一项实验中，Claude 用 Rust 构建了一个覆盖 Python 大部分子集的解释器，并使用 Verus 验证工具证明它符合一篇学术论文中概述的 CPython 语义。技术附录指出，该解释器的全部 17 层均已被证明，其定理成立：“每当解释器返回一个结果时，该结果就是形式化语义所规定的那个结果。”Anthropic 表示，对 170 万个随机生成的 Python 程序进行的实证测试发现，在 99.95% 的测试中行为与 CPython 完全相同；在故意注入的七个缺陷中，有五个在随机测试中存活下来，而全部七个都破坏了证明。

为了衡量效率，Anthropic 通过缩小真实的 OSS-Fuzz 入口点构建了 36 个小型验证任务，生成的程序包含 283–2,491 条指令，输入限制为 64 字节，并将 AddressSanitizer 替换为约 100 条指令的“mini-ASan”运行时。Anthropic 报告称，Opus 5.5 证明了一半的任务，所用 token 比 Opus 5 少约 40%。Anthropic 还报告称，在共享工作区中允许智能体互相复制证明时，所需 token 比单独工作的智能体少 17%；一些智能体在先前单独失败后取得了成功；而单独工作的智能体未能完成其中两个证明。该公司表示，在 OSS-Fuzz 工作中，同样的复用效应在大规模场景下也出现了：智能体团队会复制已完成的证明并加以改编，因为每个证明的很大一部分都涉及共享的 C 运行时和 AddressSanitizer 初始化代码。

Anthropic 表示，这些证明并不意味着这些库没有缺陷：剩余的缺陷可能位于受信任组件内部，或超出证明范围。这些证明覆盖的是链接 musl libc 的单线程静态 RISC-V 二进制文件，而大多数用户是在 x86 或 ARM 上运行这些库，并动态链接 glibc，且 AddressSanitizer 并不能检测所有内存安全缺陷。该公司表示，随着模型改进，预计这些限制将变得可控。

Theorem 通过其 OSS Verify 计划，向符合条件的开源项目免费提供同一流程。注册方式为提交拉取请求，向该计划的代码仓库添加 project.yaml、Dockerfile 和 build.sh 文件；Theorem 表示，其审核项目的方式与 OSS-Fuzz 类似，优先考虑被广泛使用的关键基础设施。据 Theorem 介绍，维护者会收到一份经 Rocq 内核检查的 Rocq 证明，证明每个 fuzz 目标在不超过 64 MiB 的任意输入下都不会崩溃；在证明过程中发现的缺陷会通过电子邮件私下告知维护者，且不设披露截止期限，而生成证明可能需要数天时间。Theorem 的路线图目标是验证整个 Nix 生态系统，包括 glibc、OpenSSL 和 cURL 等关键基础设施。