# Claude 为 123 个开源库生成形式化证明，Anthropic 与 Theorem 公布验证成果 **URL:** \ **Category:** IT\ **Tags:** claude, ai, 编程\ **Created:** [2026 年10 月 24 日 14:42 UTC](https://www.sunai.net/t/topic/1548 "2026-10-24T14:42:52Z")\ **Posts on this page:** 2\ **Page:** 1
作者： ![wood](https://www.sunai.net/user_avatar/www.sunai.net/wood/32/1032_2.png) [@wood](https://www.sunai.net/u/wood)\ 发布日期： [2026 年10 月 24 日 14:42 UTC](https://www.sunai.net/t/topic/1548/1 "2026-10-24T14:42:52Z")
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 生成的发现和补丁不保证经过人工预审。 ## 来源与公开资源 - [Anthropic 研究说明，2026-10-22](https://www.anthropic.com/research/formal-verification) - [Theorem OSS Verify：验证范围、申请方式与条件](https://theorem.dev/oss-verify/) - [公开证明仓库：oss-verify-proofs](https://github.com/theorem-labs/oss-verify-proofs) - [项目接入仓库：oss-verify](https://github.com/theorem-labs/oss-verify) ---
作者： ![wood](https://www.sunai.net/user_avatar/www.sunai.net/wood/32/1032_2.png) [@wood](https://www.sunai.net/u/wood)\ 发布日期： [2026 年10 月 24 日 14:44 UTC](https://www.sunai.net/t/topic/1548/2 "2026-10-24T14:44:03Z")
## 术语解释 - **形式化验证** ：将待验证性质写成精确命题，并用数学证明及检查器确认程序在所列条件下满足它。保证范围取决于命题和环境模型。 - **Fuzzing / 模糊测试** ：持续生成、变异输入，通过实际运行寻找崩溃或性质违反。 - **OSS-Fuzz** ：Google 发起的开源软件持续模糊测试项目。 - **Rocq** ：证明助理及证明检查系统。模型生成的证明需要通过其检查，而不是由模型自行宣布有效。 - **RISC-V** ：指令集架构；本次主要实验针对编译为该架构的二进制。 - **ASan / UBSan** ：AddressSanitizer 和 UndefinedBehaviorSanitizer，分别用于检测多类内存访问问题和未定义行为。 - **可信基础** ：验证结论仍依赖其正确性的部分，例如定理陈述、执行环境模型和证明检查器。 - **测试入口 / fuzz target** ：接收测试输入、调用被测代码并检查性质的入口；覆盖一个入口不等于覆盖整个库。