Anthropic 研究展示大语言模型如何扩大软件形式化验证规模

LLMs are making formal software verification feasible at a much larger scale

Anthropic 与 Theorem 使用 Claude，为 123 个开源库的 239 个测试入口完成 RISC-V 二进制级安全属性验证。研究将既有模糊测试转为形式化规格，由 Claude 修复发现的漏洞并生成约 180 million 行 Rocq，由 Rocq 检查器核验。

推荐理由：Anthropic 与 Theorem 将既有模糊测试转为形式化规格，再由 Claude 生成机器码级形式化验证，使验证流程无需重写整个代码库。