Theorem 开放 OSS Verify：用编码 Agent 把开源项目登记做形式化验证
随 Anthropic 形式化验证研究一同公开的 OSS Verify 由 Theorem 运营，目标是证明开源项目编译后的 fuzz 入口在任何输入下都不会崩溃、挂起或触发 sanitizer。仓库附带一个 add-project 技能：维护者在项目目录里打开编码 Agent，粘贴一段提示，Agent 按仓库中的 AGENTS.md 完成登记所需的构建配置。
适用：Claude CodeCodexCursor
能做什么
- 引导编码 Agent 为项目编写 projects/<name>/ 下的 Dockerfile 和 build.sh
- 用 tools/validate.py 和 tools/check 在本地校验登记配置能否构建
- 登记后由 Theorem 证明 fuzz 入口不会崩溃、挂起或触发 sanitizer，并反馈发现与补丁
好在哪里
- 复用项目已有的 fuzz 测试作为规格，不需要维护者手写形式化规格
- 入口只是一段提示加一份 AGENTS.md，不需要安装任何包
- README 对网络访问、AI 补丁可靠性和披露流程写得很直白
安装 / 启用
Enroll this project in OSS Verify by following the instructions here: https://raw.githubusercontent.com/theorem-labs/oss-verify/refs/heads/main/AGENTS.md
要点
- 仅接受登记 PR，要求项目开源（OSI 认可许可）、有公开 git 仓库、至少一个 fuzz target、有安全联系人，且登记人是核心维护者
- README 警告 tools/check 会带网络访问构建项目的 Dockerfile，只应在可信项目上运行
- 发现的问题和补丁由 AI 生成，可能有误，必须逐个审查；项目不承诺发送前人工复核，也不设披露期限
为什么值得关注
适合已经接入 OSS-Fuzz 的开源项目维护者：现有 fuzz 测试可以直接转成形式化规格，免费获得更强的安全保证；普通使用者可以把它当作「Agent 按 AGENTS.md 完成多步配置」的范例。
来源
原文
theorem-labs/oss-verify
GitHub · github.com
原文
LLMs are making formal software verification feasible at a much larger scale
Anthropic · anthropic.com · 2026-10-22
### [Theorem 开放 OSS Verify：用编码 Agent 把开源项目登记做形式化验证]({{URL}})
随 Anthropic 形式化验证研究一同公开的 OSS Verify 由 Theorem 运营，目标是证明开源项目编译后的 fuzz 入口在任何输入下都不会崩溃、挂起或触发 sanitizer。仓库附带一个 add-project 技能：维护者在项目目录里打开编码 Agent，粘贴一段提示，Agent 按仓库中的 AGENTS.md 完成登记所需的构建配置。
- 仅接受登记 PR，要求项目开源（OSI 认可许可）、有公开 git 仓库、至少一个 fuzz target、有安全联系人，且登记人是核心维护者
- README 警告 tools/check 会带网络访问构建项目的 Dockerfile，只应在可信项目上运行
- 发现的问题和补丁由 AI 生成，可能有误，必须逐个审查；项目不承诺发送前人工复核，也不设披露期限
**为什么值得关注**：适合已经接入 OSS-Fuzz 的开源项目维护者：现有 fuzz 测试可以直接转成形式化规格，免费获得更强的安全保证；普通使用者可以把它当作「Agent 按 AGENTS.md 完成多步配置」的范例。
来源：[theorem-labs/oss-verify](https://github.com/theorem-labs/oss-verify)；[LLMs are making formal software verification feasible at a much larger scale](https://www.anthropic.com/research/formal-verification)