10 月 22 日，Anthropic 公布与 Theorem 合作的形式化验证研究。团队称，Claude 在数周内为 123 个开源库的 239 个测试入口生成了证明，并在证明过程中发现、修补了一批缺陷。
这些证明针对编译后的 RISC-V 二进制及指定测试入口，不是对整个软件库全部行为的无条件保证。
把模糊测试入口变成待证明的命题
研究利用了 OSS-Fuzz 中已有的测试入口。传统模糊测试不断生成、变异输入，寻找能够触发崩溃或断言失败的情况；此次工作则将测试及执行环境转成形式化命题，让 Claude 编写证明，再由 Rocq 检查器核验。
证明过程中，如果发现命题不成立，Claude 可以尝试定位和修补问题，然后针对修改后的程序重新生成命题、继续证明。因此，一部分研究结果针对修补后的版本，不能理解为原始代码本来就不存在缺陷。
Anthropic 报告称，完整研究产生约 1.8 亿行 Rocq 证明代码。模型负责生成证明，最终是否满足形式化命题由检查器判定。
验证边界是什么
研究中的主要实验有明确条件：输入大小上限约 64 MB，程序以单线程、静态链接的 RISC-V 二进制在建模的 Linux 环境中运行，并受固定内存预算约束。
Theorem 的公开仓库给出了更具体的表述：在满足所列资源条件的输入上，普通构建与加入 sanitizer 的构建具有对应的可观察行为，且不会进入所定义的错误状态。实际结论应以各入口的定理、构建版本和环境模型为准，不能只看“不崩溃”这一概括。
可信基础仍包括形式化模型、定理陈述和 Rocq 检查器。仓库也明确说明，Linux 进程模型并不完整，包含未被检查的假设。
这些结果不覆盖所有 CPU、操作系统、并发行为和资源条件，也不自动证明全部业务逻辑正确。
研究总量与公开证明数量不同
Anthropic 报告的总量是 123 个库、239 个入口。
本次查阅的公开仓库 theorem-labs/oss-verify-proofs 则列出 25 个库、60 个入口的证明，覆盖 OpenSSL、simdjson、zstd、libpcap、bzip2 等项目的部分入口。仓库说明使用 Rocq 9.2.0 检查证明。
因此，研究报告中的全部成果与目前可下载、复核的公开证明子集，需要分开看。
开源维护者可以申请参与
Theorem 同时提供 OSS Verify，为符合条件的开源项目免费开展验证。项目由核心维护者提交申请，通常需要提供 project.yaml、Dockerfile 和 build.sh，并准备静态 riscv64 测试二进制。
Theorem 表示会优先考虑被广泛使用的基础软件。证明可能需要多日完成；发现的问题会私下报告给维护者，AI 生成的发现和补丁不保证经过人工预审。