Anthropic shares a subset of Claude-written software proofs

In its October 22 announcement, Anthropic describes a pipeline that compiles a library and its existing fuzz test—a test entry point for generated inputs—to RISC-V machine code. The executable, a formal model of instructions and Linux, and a desired no-crash property determine the mathematical specification. Claude writes a proof; the Rocq kernel checks it against that specification.

The public proof repository makes the boundaries concrete: proofs concern particular compiled binaries and code reachable through a test entry point, under stated input and memory conditions. They do not establish correctness of the entire library, exclude wrong answers or memory leaks that the checks cannot detect, or apply to x86 builds. None of the proofs in this release rules out a run that never finishes. Its documented checker verifies binary hashes, constructs statements, compiles proofs and rejects assumptions outside an allowed list.

The underlying Linux process model also explains what a comparison of program behavior can mean. It distinguishes output bytes, their order, exit status and final file contents, but does not observe execution time or instruction count. A result must identify the statement actually proved; matching observable behavior alone does not establish termination. The model remains incomplete and relies on unchecked assumptions, so its authors direct readers to its scope document before treating a proof as evidence about a real program.

Matthias Bastian covered the project and its practical limitations for The Decoder on October 23.