Anthropic：Claude为123个开源库的编译代码编写了可机器验证的证明
Anthropic前沿红队与形式化方法公司Theorem利用Claude证明，123个OSS-Fuzz库中的239个模糊测试入口在建模环境中、对小于64MB的任何输入都不会崩溃。这项工作发现了多年模糊测试遗漏的漏洞，但证明附带重要前提。
Anthropic发布研究称，其前沿红队与形式化方法公司Theorem合作，利用Claude对谷歌OSS-Fuzz项目中123个开源库的安全属性进行了形式化验证，覆盖239个模糊测试入口。值得注意的是，这些证明针对的是编译后的RISC-V机器码，而非源代码。
方法
每个现有的模糊测试都被转化为形式化规范：在建模环境中，编译后的测试对任何小于64MB的输入都不得崩溃（例如AddressSanitizer捕获的内存错误或断言失败）。Theorem提供了RISC-V指令集和Linux进程行为的形式化模型，Claude编写证明，再由Rocq证明检查器验证。据DevOps.com报道，Claude在几周内生成了约1.8亿行证明。
模糊测试遗漏的漏洞
Claude被允许修补遇到的漏洞，结果发现了数百个。例子包括一个解压器中的计数器下溢——只有在约20MB的输入下才会导致越界写入，以及一个需要64MB输入才能触发的图像解码器读取错误。Anthropic表示会惩罚大幅修改并进行审核，防止模型把程序改写成”永不崩溃”的空壳。
局限
Anthropic强调，“经过形式化验证”不等于”没有漏洞”。证明假设的是单线程、静态链接musl libc的RISC-V二进制文件，而大多数已部署的Linux软件运行在x86或ARM上并使用glibc；AddressSanitizer并不能捕获所有内存错误，也并非所有入口都经过验证。成本也是限制：证明可能消耗数亿个token。关于新版Claude效率提升的数据来自Anthropic自己的基准测试。部分证明已在GitHub上公开。