开源软件的安全性长期依赖模糊测试来发现问题，但测试覆盖的边界始终有限。Anthropic与Theorem展开合作，尝试用大模型把这一环节推进到形式化验证层面，让安全证明不再只停留在抽样测试的层面。

具体做法是，由Claude将OSS-Fuzz的模糊测试结果转化为形式化规格，再据此生成机器可检验的证明。这套流程覆盖了123个开源库中的239个入口点，目标是证明任意64 MB以下的输入都不会引发崩溃，而非仅仅验证测试样本内的行为。

最终产出的证明规模约为1.8亿行Rocq代码。Rocq是此前名为Coq的证明助手，其证明可由机器逐行校验，这意味着结论建立在可审计的形式化推导之上，而非模型自身的判断。

对AI行业而言，这一合作展示了模型在软件安全验证中的新型角色：从辅助编写代码延伸至参与形式化证明的生成。不过，该方法目前仍依赖模糊测试作为规格来源，其适用范围与后续推广效果有待进一步观察。