Anthropic与Theorem在10月22日公布软件形式验证研究。合作方报告，Claude为123个开源库的239个测试入口生成了可由Rocq检查的证明。测试入口是把输入交给库中特定功能的小程序，因此“覆盖某个库”并不意味着验证了整个库。这里的239是合作方报告的规模，本轮没有独立重跑证明，也不能据此计算所有尝试的成功率。

Anthropic and Theorem announced research on formal software verification on October 22. The collaborators reported that Claude generated proofs checkable by Rocq for 239 test entry points across 123 open-source libraries. A test entry point is a small program that passes input to a particular function in a library, so covering a library does not mean verifying that library in its entirety. The figure of 239 is the scale reported by the collaborators. This review did not independently rerun the proofs, and the figure cannot be used to calculate the success rate across all attempts.

普通测试通过具体输入寻找反例；形式验证则先精确定义程序和允许的行为，再检查某项性质是否在这些前提下成立。模型负责提出并撰写证明，检查器核查证明步骤。这样的分工有价值：读者可以检查证明，而不必只相信模型说“代码没问题”。但如果规格遗漏了重要风险，证明再正确也不能补上遗漏；机器语义模型和检查器本身仍属于需要信任的基础。

Conventional testing looks for counterexamples by running specific inputs. Formal verification first defines the program and its permitted behavior precisely, then checks whether a particular property holds under those assumptions. The model proposes and writes the proof; the checker verifies its steps. This division of labor matters because a reader can inspect a proof rather than simply trust the model's claim that the code has no problems. But if a specification omits an important risk, even a correct proof cannot fill that gap. The model of machine semantics and the checker itself also remain part of the trusted foundation.

截至本次读取，公开仓库列出25个库、60个入口，是总体研究的一个子集，不能说123个库的全部证明都已公开复验。仓库还明确：这一批公开证明没有证明程序必然结束。因此不能把结果概括为“任意输入都正常退出”，更不能称为没有逻辑错误、内存泄漏或安全漏洞的完整保证。

At the time the material was read, the public repository listed 25 libraries and 60 entry points. This is a subset of the overall research, so it would be incorrect to say that proofs for all 123 libraries had been publicly reproduced. The repository also states explicitly that this collection of public proofs does not prove termination. The results therefore cannot be summarized as guaranteeing normal exit for every possible input, still less as a complete guarantee against logic errors, memory leaks or security vulnerabilities.

研究针对指定的RISC-V静态、单线程构建及受限Linux运行模型；输入大小与内存预算也有约束，附录的完整输入范围小于64 MiB。不能直接推广到常见x86或ARM、多线程、动态链接或未建模的系统行为。模型获准修改代码时，证明针对对应的修改后版本，也不代表补丁已经被上游项目接受。

The research concerns specified static, single-threaded RISC-V builds and a restricted model of a Linux runtime. Input size and memory use are constrained, and the full input range described in the appendix is below 64 MiB. The findings cannot be generalized directly to common x86 or ARM environments, multithreading, dynamic linking or system behavior outside the model. Where the model was permitted to modify code, the proof applies to that modified version; it does not establish that the upstream project has accepted the patch.

Theorem官网目前接受合格开源项目的维护者申请免费验证，按项目审核，要求兼容的静态RISC-V构建，证明生成可能需要多天。这提供了实际申请入口，但不等于Claude推出了面向所有代码的一键通用验证服务。

Theorem's website currently accepts applications from maintainers of qualifying open-source projects for free verification, subject to project review. It requires a compatible static RISC-V build, and proof generation may take days. This is a real application route, but it does not mean that Claude has launched a universal, one-click verification service for arbitrary code.

维护解析器、压缩库等基础组件的团队，可以把它看作在现有测试之外增加可检查证据的一条路径。判断它能否进入日常开发，要看外部团队能否复验公开证明、更多真实运行环境能否获得支持，以及生成和检查证明的总成本。研究附录也指出证明可能很冗长，复杂程序还需要更好的模块化方法；本次结果不足以推算普遍成本节省或商业收益。

Teams maintaining foundational components such as parsers and compression libraries can view this as a way of adding checkable evidence alongside existing tests. Whether it can become part of everyday development will depend on external teams reproducing the public proofs, support for more real runtime environments, and the total cost of generating and checking proofs. The research appendix also notes that proofs can be very lengthy and that complex programs need better modular methods. These results do not establish general cost savings or commercial returns.