Anthropic称Claude为123个开源库完成形式化验证
先了解这件事
Anthropic 发布研究称，其 Frontier Red Team 与 Theorem 合作，用 Claude 将 OSS-Fuzz 模糊测试转化为规格，对 123 个开源库的 239 个入口点完成汇编级（RISC-V）形式化安全证明，生成约 1.8 亿行 Rocq 证明，由 Rocq 自动核验，几乎无需人工审查。 Anthropic 称，证明覆盖任意小于 64 MB 的输入及所建模的 Linux 系统响应和内存布局，程序总会正常退出，不触发内存安全错误或断言失败；前提是程序为单线程静态二进制、内存预算固定，运行在 RISC-V 1 CPU 的 Linux 上。Anthropic 表示已公开部分证明及 RISC-V 和操作系统语义，供他人验证和复用。 The Decoder 报道称，单个证明消耗数亿 token，计算成本高昂。Anthropic 称这突破了形式化验证过去仅适用于小型代码库、或需大量专家人工投入的限制；上述规模和效果均为 Anthropic 的说法。
AI 根据报道生成 · 7 天前更新
报道时间线
沿着报道，了解事件的不同侧面。
- The Decoder：AI NewsAnthropic 用 Claude 自动生成数学证明验证现有代码安全性
Anthropic 的 Frontier Red Team 与 Theorem 合作，让 Claude 将 OSS-Fuzz 测试转化为数学问题并生成约 1.8 亿行证明代码，由独立程序 Rocq 自动核验，几乎无需人工审查。
- Anthropic精选Anthropic 发布博客：用 Claude 大规模形式化验证开源软件安全性
Anthropic 在 Frontier Red Team 博客发布研究，介绍用 Claude 大规模进行形式化验证的方法。与 Theorem Labs 合作，团队在数周内为超过一百个真实开源库证明了安全属性，突破了形式化验证过去仅适用于小型代码库或需大量专家人工的限制。全文见 https://www.anthropic.com/research/formal-verification。
- Anthropic：Research精选Anthropic 用 Claude 对 123 个开源库完成汇编级形式化安全证明
Anthropic 与 Theorem 合作，用 Claude 将 OSS-Fuzz 模糊测试转化为规格，对 123 个开源库的 239 个入口点证明了任意 64 MB 以下输入不崩溃，生成约 1.8 亿行 Rocq 证明。
本事件热度走势
- 可比范围当前
- 3
- 可比范围峰值
- 6910月23日 20:00
- 近 24 小时变化
- -50%
趋势仅比较持续完整观测到的相同主体，范围可能小于当前热度统计。移动指针或点击图表查看每小时热度；键盘可用左右方向键切换。