Anthropic 用 Claude 对 123 个开源库完成汇编级形式化安全证明

Anthropic 与 Theorem 合作，用 Claude 将 OSS-Fuzz 模糊测试转化为规格，对 123 个开源库的 239 个入口点证明了任意 64 MB 以下输入不崩溃。整个工作生成了约 1.8 亿行 Rocq 证明。