RecodeX 重构消息，Anthropic前沿红队团队与Theorem Labs发布报告，让Claude针对RISC-V底层汇编指令，对真实生产级开源代码库开展形式化验证。数周内，Claude在123个开源代码库的239个测试入口完成验证，累计生成约10亿行Rocq证明代码，其中约1.8亿行通过机器核验。
研究团队称，仅尝试证明的过程就揪出数百个Bug，包括解压器中需约20MB罕见输入才触发的计数器下溢。在Claude用Rust编写的Python解释器中故意植入的7个Bug，随机测试漏掉5个，形式化证明全部发现。
团队还称，Claude自主写出x86指令集数学模型，并发现官方参考文档数百处错误及少量CPU硬件缺陷。首批25个库、60个入口的证明已在GitHub公开。