模糊测试反复生成输入，寻找能让程序崩溃的情况；再多测试也不能穷尽所有输入。Anthropic 与 Theorem 的新报告尝试把已有测试入口转成形式化命题：在约定环境和输入限制内，带检测器的二进制不会触发错误，且与普通构建保持所定义的行为一致。Claude 编写证明，Rocq 的检查内核核对证明是否满足命题。
团队报告，在数周内为 123 个 OSS-Fuzz 库的 239 个入口修复问题并完成证明，成功证明约含 1.8 亿行 Rocq。这里保证的对象是编译后的单线程、静态 RISC-V Linux 程序，带固定内存预算；主文把输入限制写为 64 MB，附录具体写为 64 MiB。它不是对同库所有源码、所有入口及实际 x86/ARM 部署的通用保证。尝试证明的过程也发现了普通模糊测试不容易触及的大输入和罕见路径问题。
公开成果另有范围。截至本次读取，仓库列出 25 个库、60 个入口的证明，属于研究结果的一个子集。README 明确这些证明没有排除永不结束的执行；未被检测器捕获的错误、模型没有覆盖的系统行为以及调用方误用，也可能留在范围之外。最重要的进展是把更多真实软件性质变成可重复检查的对象，同时把剩余信任集中到命题、机器与操作系统语义模型、检查器及其相关工具上。