Anthropic 用 Claude 证明 123 个开源库无崩溃, proofs 达 1.8 亿行 Rocq
inductionheads · x · 2026-10-23
Anthropic 在 Frontier Red Team 博客发布与 Theorem Labs 的合作研究：用 Claude 在数周内对 123 个真实开源库（OSS-Fuzz）完成形式化验证——修补发现的 bug 后，证明 239 个入口点在任何输入（最大 64MB）下都不会崩溃。
- 证明作用于编译后的 RISC-V 二进制，共约 1.8 亿行 Rocq 证明，单个证明约 60 万行，覆盖中位长度 1.8 万条 RISC-V 指令的二进制
- 方法：用 Theorem 的 RISC-V 指令与 Linux 进程语义把汇编翻译为数学模型；目前假设单线程静态二进制、固定内存预算
- 证明可复用：agent 共享工作区互相复制证明后，token 消耗减少 17%，36 个证明共复用 324 个文件
- 引发「攻防天平逆转」的讨论：形式化证明等非对称防御手段可能终结攻击者优势
所属事件:Anthropic 用 Claude 为百余开源库生成汇编级形式化安全证明(23 条相关)→
「安全」频道最新
- Anthropic 披露百余项安全控制，靠出口带宽限制保护模型权重 — bookwormengr · 2026-10-24
- PHP 漏洞遭泄露后,vista8 换用 1Password 并看中其 Agent 友好设计 — vista8 · 2026-10-24
- Lightspeed 播客谈 Agent 时代网络安全与模型可解释性 — theamberyang · 2026-10-24
- 「对齐自由应像言论自由」:千亿 agent 伦理单一化的 1984 警告 — robleclerc · 2026-10-24
- AI 加速漏洞挖掘，网络犯罪损失将下沉给全社会承担 — mimi10v3 · 2026-10-24
- 斯坦福 HAI 回顾：六年前提出 NAIRR 国家 AI 算力蓝图 — StanfordHAI · 2026-10-24