Claude 参与大规模形式验证,官方称覆盖 123 个开源库
Anthropic Frontier Red Team 公布与 Theorem 合作的形式验证研究:用 Claude 为 123 个真实开源库的 239 个 OSS-Fuzz 入口生成 Rocq 证明,官方称在限定 RISC-V/Linux 假设下证明这些入口对小于 64MB 的任意输入不会触发内存安全错误或断言失败,并在此过程中发现和修补数百个缺陷。
若公开证明与可信基础成立,这把形式验证从高成本小代码库推进到大量生产开源组件,可能改变漏洞发现与安全保证流程;但当前为官方发布,覆盖范围受特定假设限制。
实现链路
将既有 fuzz test 编译为 RISC-V 可执行文件,结合 Theorem 的 RISC-V/Linux 形式语义,把“测试永不崩溃”写成规范;Claude 生成 Rocq 证明并由 Rocq 内核检查,发现问题时修补代码后重新生成规范再证明。
最小复现思路
可独立检查公开证明子集的定理陈述与 Rocq 检查结果,并选一个小型 OSS-Fuzz 入口复现规范生成与证明流程;不在此执行。
已知与推测
来源披露:原帖与所附 Anthropic 研究页说明合作、数量、证明流程与假设;未独立核验证明,也未运行代码。
成本与风险
依赖 Theorem 形式语义、Rocq 工具链与专家审阅;当前仅覆盖单线程静态二进制、固定内存、RISC-V/Linux、输入小于 64MB 等假设,不能推出所有漏洞消失。
原始来源与证据范围 1 条
- X · @AnthropicAI ↗
已读取原帖正文;已读取所附允许域名页面(不证明视频画面)