原始来源：Anthropic / Theorem · 研究报告
发现渠道：Hacker News · 发布前发现
模糊测试反复生成输入，寻找能让程序崩溃的情况；再多测试也不能穷尽所有输入。Anthropic 与 Theorem 的新报告尝试把已有测试入口转成形式化命题：在约定环境和输入限制内，带检测器的二进制不会触发错误，且与普通构建保持所定义的行为一致。Claude 编写证明，Rocq 的检查内核核对证明是否满足命题。
团队报告，在数周内为 123 个 OSS-Fuzz 库的 239 个入口修复问题并完成证明，成功证明约含 1.8 亿行 Rocq。这里保证的对象是编译后的单线程、静态 RISC-V Linux 程序，带固定内存预算；主文把输入限制写为 64 MB，附录具体写为 64 MiB。它不是对同库所有源码、所有入口及实际 x86/ARM 部署的通用保证。尝试证明的过程也发现了普通模糊测试不容易触及的大输入和罕见路径问题。
公开成果另有范围。截至本次读取，仓库列出 25 个库、60 个入口的证明，属于研究结果的一个子集。README 明确这些证明没有排除永不结束的执行；未被检测器捕获的错误、模型没有覆盖的系统行为以及调用方误用，也可能留在范围之外。最重要的进展是把更多真实软件性质变成可重复检查的对象，同时把剩余信任集中到命题、机器与操作系统语义模型、检查器及其相关工具上。
可信度 65 · 重要性 85 · 新颖度 78
技术与主题
AI 编程 · 评测与基准 · 基础模型 · 推理能力 · Formal Verification · Rocq · Binary Semantics
Theorem 研究团队
配套附录中的形式验证专家评读，属于发布材料内部讨论，并非独立第三方验收。
忠实转述（非原句）：附录肯定代理能为较复杂程序提炼更短的规范，也指出生成证明经常过度展开底层细节。这样的证明对同一个命题仍然有效，但能否直接扩展到更复杂程序尚无定论；更好的抽象可能决定后续规模。
编辑评读
这里的新能力不只在于写出很长的证明。已有测试入口包含维护者认为重要的性质，例如压缩再解压应回到原输入；若失败会触发断言，证明它在覆盖范围内永不触发，就把一种反复抽样的检查转成了普遍命题。复用现有测试约定，有机会降低从头编写完整业务规范的门槛。
真正需要改变的判断，是“模型生成的证明也只能靠另一个模型相信”。固定检查器可以判断形式推导是否成立；人仍需审查所证明的命题是不是自己关心的问题，以及语义模型是否对应实际环境。模型若同时修改程序以便完成证明，还可能通过削弱行为取巧。报告说团队对补丁设惩罚并记录、审计，但这不等于功能保持已经自动得到保证。
附录还保留了对扩展性的疑问：许多证明逐条展开寄存器、地址和分支，规模很大，人类专家往往会引入模块化抽象。共享证明和通用库可能降低重复工作，下一步应看软件升级时重证的成本、可信语义的独立审计和真实部署架构覆盖。本刊读了报告、附录与仓库说明，没有运行证明检查器，也没有把发布方的规模主张写成独立复现。