Anthropic 用 Claude 数周验证 123 个开源项目，形式化验证规模化到来
Miles_Brundage · x · 2026-10-23
- Anthropic 在 Frontier Red Team 博客发布新研究：与 Theorem Labs 合作，用 Claude 在几周内对 100 多个真实开源库完成了安全属性的形式化验证。
- 形式化验证可以证明代码不存在某类 bug，但历史上只适用于小型代码库或需要大量专家时间；AI 模型正在改变这一点。
- Theorem 同步推出 OSS Verify：为符合条件的开源项目免费提供二进制级形式化验证。区别于测试（只覆盖写过的输入）和模糊测试（只试过碰到的输入），验证证明覆盖所有输入——其定理针对编译后的二进制而非源码，声称「任何不超过 64 MiB 的输入都不会导致崩溃」。
- 项目方会收到机器校验的证明文件，或得到需要修复的补丁，目标是自举一个「已验证软件」生态。
所属事件:Anthropic 用 Claude 为百余开源库生成汇编级形式化安全证明(5 条相关)→
「安全」频道最新
- 25 位学者新论文:用芯片供应链「硬暂停」前沿 AI 训练可行吗 — wfithian · 2026-10-23
- Garrison Lovely 新书《Obsolete》出版:AI 万亿替代竞赛的批判之作 — GarrisonLovely · 2026-10-23
- 被解雇的 OpenAI 安全研究员将上播客，首次公开回应 — kevinroose · 2026-10-23
- Linux 内核现两个 9.0 分 RCE 漏洞，官方补丁尚未发布 — emax · 2026-10-23
- FDA 批准个性化新抗原癌症疫苗：每位患者产品皆不同 — alex_peys · 2026-10-23
- Reddit 热议网络安全圈震荡：AI 驱动攻击让防御方措手不及 — Anen-o-me · 2026-10-23