Anthropic 用 Claude 为 123 个开源库生成汇编级安全证明
先了解这件事
Anthropic 的 Frontier Red Team 与 Theorem 合作，让 Claude 在数周内为 Google OSS-Fuzz 项目中 123 个开源库的 239 个入口点生成约 1.8 亿行 Rocq 证明代码，由独立程序 Rocq 自动校验，典型单个证明约 60 万行。 这些证明只在严格条件下成立：特定处理器架构（RISC-V 汇编层）、单线程程序、输入小于 64 MB。单个证明的算力开销可达数亿 token，Anthropic 未披露项目总成本。 研究者称其为“完全自主”的证明生成，但工具与形式化基础由 Theorem 的人工构建。
AI 根据报道生成 · 4 天前更新
报道时间线
沿着报道，了解事件的不同侧面。
- The DecoderAnthropic用Claude自动完成代码形式化验证
Anthropic的Frontier Red Team与合作方Theorem合作，让Claude对现有开源代码进行数学正确性证明：模型在数周内生成约1.8亿行证明代码，覆盖Google OSS-Fuzz项目中123个开源库的测试程序，由独立程序Rocq自动校验。
- AIHOT 精选Anthropic 发布用 Claude 大规模形式化验证开源软件安全的研究
Anthropic 在 Frontier Red Team 博客发布研究，介绍用 Claude 大规模进行形式化验证的方法。团队与 Theorem Labs 合作，在数周内为超过一百个真实开源库证明了安全属性，突破了形式化验证过去仅适用于小型代码库或需大量专家人工的限制。全文见 https://www.anthropic.com/research/formal-verification。
- AIHOT 精选Anthropic 用 Claude 对 123 个开源库完成汇编级形式化安全证明
Anthropic 与 Theorem 合作，用 Claude 在 RISC-V 汇编层为 123 个 OSS-Fuzz 开源库的 239 个入口点生成形式化无崩溃证明，证明代码约 1.8 亿行 Rocq，典型单个证明约 60 万行。
本事件热度走势
- 可比范围当前
- 3
- 可比范围峰值
- 1010月23日 20:00
- 近 24 小时变化
- -51%
趋势仅比较持续完整观测到的相同主体，范围可能小于当前热度统计。移动指针或点击图表查看每小时热度；键盘可用左右方向键切换。