Anthropic：Claude 已大规模形式化验证开源库

10 月 22 日，人工智能公司 Anthropic 旗下 Frontier Red Team 发布一项研究，指出大语言模型目前已具备在更大规模上自动生成形式化证明的能力。该团队联合 Theorem，基于 Claude 模型，在 RISC-V 汇编层级对逾 100 个真实开源库开展了安全性质的形式化验证——这是迄今首次有 AI 系统在汇编层面对生产级软件实施的大规模形式化验证。在证明构建过程中，团队还意外揭示了多个长期未被发现的安全漏洞。实验方法是将 Google OSS-Fuzz 中已有的可编译 fuzz 测试用例转化为形式化规格，并在单线程静态二进制、固定内存预算、RISC-V CPU 架构及 Linux 运行环境等约束条件下，对任意大小不超过 64 MB 的输入执行验证。