Claude在与形式化验证公司Theorem合作下，为123个开源库编写了约1.8亿行数学证明，成功找出数百个软件漏洞。传统测试依赖随机数据输入，无法保证不遗漏错误，而这次通过数学证明，Claude试图从根本上排除特定类型的错误。几周内，Claude完成了239个测试入口的验证，结果显示在指定运行环境下，这些程序面对小于64 MB的任意输入，都不会触发崩溃。证明过程中，Claude还发现并修复了数百个bug，包括内存越界写入和图像解码漏洞等。过去，这类数学验证极为耗时，例如sel4操作系统内核的数学验证需耗时约20年。