Read the theorem before trusting an AI-generated proof

Start with the released evidence

Anthropic and Theorem announced proofs for 239 fuzzing entry points across 123 libraries on October 22. The public release covers 60 entry points in 25 libraries. Those are different populations. Anthropic withheld proofs that could expose unpatched bugs. Neither dividing the totals nor counting statement files produces a meaningful general success rate.^[1][2][3][4]

Kingy and Xenospectrum independently explain the release's narrower guarantees. Their analyses distinguish an agreement theorem from termination and a named executable from an entire library. The practical exercise below applies that distinction to an actual cJSON entry point. It is a documentation-reading exercise; no proof checker, executable or model benchmark was run here.^[1][2][5]

Read one actual statement and status

Open the versioned cJSON harness page linked in source 5. It names cjson/cjson_read_fuzzer, using cJSON 1.7.18 at upstream commit acc76239. The table marks asan_agrees, ubsan_agrees and asan_ubsan_agrees proved. Its halts statements remain open. A statement existing in Statements.v defines an obligation; the separate proof index and harness status identify which obligations have proofs.^[4][5]

Focus on asan_agrees. Its definition compares the plain and AddressSanitizer builds using the alloc-forced-only environment variant. The plain build's 2 GiB memory budget is a premise: inputs needing more are outside coverage. Memory requests may be refused only when the budget is spent or no address range is free. Other modeled requests can still fail.^[5][6]

Agreement says neither build reaches an error and their sets of observable behavior match under the stated conditions. Observable behavior includes stream and connection bytes, exit status and final file contents. It compares behavior sets rather than two executions in lockstep. Finite observations can describe a run that continues forever. A halting theorem is a separate obligation.^[4][6]

Inspect what the harness actually checks

This harness parses, prints and minifies JSON, then frees its outputs unexamined. It adds no independent functional check of those outputs. The proof therefore does not establish that the JSON result matches an application's intended meaning. A different harness might assert a round-trip property; a guarantee about that check requires the check to be present in the covered binary.^[3][5]

The release concerns static riscv64 Linux binaries compiled with clang 20.1.8 against musl. A package with the same library version on an x86 server with dynamic linking is another artifact. The Linux process model, LPS, is explicitly incomplete and includes unchecked assumptions. Machine checking inside that model cannot establish that the model matches every deployment behavior.^[3][4]

Try the assurance-sentence exercise

A hypothetical review says: “Our JSON service uses cJSON, whose AI-generated proof guarantees correct parsing and termination on untrusted files.” Before reading the answer, identify four unsupported extensions. Use the named statement, the memory premise, the harness behavior and the executable identity to decide what evidence would be needed.^[4][5][6]

Answer: the sentence expands one entry point to a service, assumes output correctness that the harness never checks, infers termination from agreement, and drops the binary and environment assumptions. The 2 GiB premise supplies no measured peak-memory result. An ordinary service can also misuse library calls in ways the covered harness never reaches.^[3][4][5][6]

A bounded replacement reads: “The released cjson_read_fuzzer asan_agrees statement is listed as proved for its specified plain and ASan binaries. Under its process-model, memory and refusal assumptions, the builds are error-free and agree in observable behavior. This result does not establish termination, application-level JSON correctness, other entry points or our deployed service.”^[4][5][6]

Keep a scope card beside the dependency

Record the release and statement revision, executable hashes, reachable entry point, property, input restrictions, memory premises, allowed environmental failures and model version. Record checker execution separately from reading a published status. Match the deployed artifact before carrying the assurance forward. Keep regression tests, caller checks and resource controls for obligations outside the theorem; refresh the record after a rebuild.^[1][3][4]