Claude 用 LLM 实现大规模形式化验证

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

传统形式化验证因耗时耗力难以普及，但 LLM 正在改变这一现状。我们与 Theorem 合作，利用 Claude 在 123 个开源库的 RISC-V 汇编代码层面证明了安全属性，这是首次大规模将 AI 应用于生产软件的形式化验证。Claude 不仅生成了数百万行 Rocq 证明代码，还修复了连 OSS-Fuzz 数万亿次测试都未发现的深层漏洞。这一突破让软件在任意输入下不崩溃的数学保证成为可能，标志着安全软件开发工作流的新篇章。