Anthropic 与 Theorem 公布一项大规模软件形式化验证工作，让 Claude 为 123 个真实开源库的程序入口构建安全证明。10 月 22 日发布的研究把关注点从寻找单个漏洞推进到检查明确的安全性质，证明在指定条件下，程序面对所有符合范围的输入都能正常退出。
研究在 RISC-V 汇编层面建模，覆盖的性质包括不触发内存安全错误及断言失败。其结论有具体范围：输入小于 64MB，程序是单线程静态二进制，使用固定内存预算，并运行在所建模的 Linux 系统响应和内存布局之下。这些假设定义了证明的适用边界，不能外推成整个软件在所有平台都没有漏洞。
团队已公开部分证明以及 RISC-V 和操作系统语义，使其他开发者能够复查与复用。研究还称，Claude 在写证明时发现了一些长期未被测试识别的问题。Theorem 提供同类验证流程，并发布帮助开发者着手验证代码的 Claude skill，将证明构建从一次研究展示延伸到其他开源项目。