测试软件，像是抽查一座桥；形式化验证（formal verification）则试图用数学证明，在规定条件内，每一种情况都不会出错。它过去贵得惊人：Anthropic举例称，seL4操作系统内核开发用了2人年，验证却用了20人年。如今，Anthropic与Theorem尝试让Claude代写这些证明，把原本高度依赖专家的工作推向更大规模。
团队让Claude检查123个真实开源库，并在RISC-V汇编代码——处理器实际执行的底层指令——层面证明一项具体性质：在输入小于64 MB、单线程静态程序、固定内存预算等假设下，程序面对其建模范围内的Linux响应和内存布局，都能正常退出，不触发内存安全错误或断言失败。证明仍需由工具逐步验算。Anthropic称，这是首次在生产软件的汇编层面大规模用AI开展形式化验证；但它证明的只是预先写下的规格，规格若遗漏现实风险，证明也不会自动补上这块盲区。