Anthropic测试Claude自动验证开源软件正确性

Anthropic与Theorem让Claude为Google OSS-Fuzz项目中的123个开源库生成形式化证明，数周内产出约1.8亿行证明代码。Claude在证明过程中发现数百个缺陷，部分问题此前长期未被发现；证明由Rocq自动检查，但仅适用于特定处理器架构、单线程程序和低于64 MB的输入，个别证明消耗数亿tokens。