The report says roughly 180 million lines of proof accepted by the proof checker came from about one billion lines Claude wrote during the project.
The proofs concern compiled RISC-V Linux binaries. For inputs under 64 MiB, they aim to establish that both ASan-instrumented and normal binaries do not fault, abort, or encounter behavior outside the formal model; they also establish a specified equivalence between the two builds. The report says checker runs for one proof can take 30 minutes to several CPU hours.
The stated scope is narrower than a general software-safety claim. It covers particular single-threaded, statically linked, musl-based binaries with a fixed memory budget, not typical x86 or ARM deployments using glibc. It does not prove termination, performance properties, or crash-freedom beyond the modeled behavior and input bound.
The appendix also describes a separate Rust experiment: Claude built a 17-tier Python-language fragment interpreter and Verus verified its implementation against a formal semantics. The connection between that semantics and CPython was tested empirically on more than 1.7 million programs, not formally proved.