公开仓库提供可机器检查的 Rocq 证明与验证工具，但范围小于发布方报告的内部运行。
Anthropic 与 Theorem 发布 C 库机器校验证明
2026-10-22已核实动态TRIAL
Anthropic 与 Theorem 公开了 MIT 许可的 Rocq 证明和验证工具，覆盖部分 C 库 fuzz 入口。Anthropic 报告内部运行规模更大；当前公开证明仓库覆盖 25 个库的 60 个入口。保证范围只涵盖建模后的静态、单线程 RISC-V Linux 进程，以及每个 fuzz target 明确写出的性质。
对你意味着什么
对评估 AI 生成验证的团队来说，公开产物可以直接检查 proof，而不必只信 benchmark 分数。内部规模与公开子集有差距，执行模型也很窄，因此它适合可复现试点，不等于对整个软件栈给出安全保证。
证据与关联材料
技术细节与六维评分
| 公开产物 | 25 个库的 60 个 fuzz 入口 |
|---|---|
| 发布方报告的内部规模 | 123 个库、239 个入口，约 1.8 亿行 Rocq |
| 证明系统 | Rocq 与建模后的 Linux 进程语义 |
| 保证边界 | 静态、单线程 RISC-V 进程，musl 与建模后的 Linux 行为 |
| 许可 | 所引公开仓库为 MIT |
| 时间依据 | 官方文章和仓库只提供 2026-10-22 日期精度，无法严格定位小时边界 |
技术影响 4
工程价值 4
采用信号 2
成熟度 2
验证成本 3
风险 2