Findings · Formal verification

A widely used C JSON library does not preserve numbers across a serialise-and-reparse round trip: its number pipeline is lossy by design, printing with limited precision and comparing re-reads by tolerance rather than equality.

Evidence

Asked to prove that serialising a value and re-parsing it returns the same value, the honest answer was that the theorem is false of this target. The library prints numbers with limited precision, re-reads them, and only falls back to more digits if the re-read “differs” under a roughly one-unit-in-the-last-place tolerance, not equality. So print-then-parse is not value-preserving. This is not a proof difficulty; it is a property the artifact lacks, and a proof of round-trip would have to be weakened until it certified nothing anyone cared about.

Sample. cJSON's number pipeline read at the source level, corroborated by a differential over 120,000 fuzzed inputs (vsf-cjson @ dcdae40b, RESULTS.md:91-96) in which every input falls into exactly one of six categories: AGREE 116,476 (identical bytes and exit code); PORT_WRONG 0 (the Lean port at fault. A signature-free measure); TARGET_WRONG_OR_DIFFERENT 112, attributed to cJSON's IEEE-double pipeline but recognised by a signature the author chose, so it is an authored trusted-base classification, not an objective count of cJSON defects; INTENTIONAL_SEMANTIC_CHANGE 3,390 (divergences approved in SPEC §S6); HARNESS_ERROR 22 (the comparator could not decide); UNCLASSIFIED 0. The six sum to 120,000. The headline round-trip finding rests on the source-level reading; the 112 is a classified subset, not the finding's proof.

Boundary

That the library is defective for its purpose. A lax parser tuned for triage is a different artifact from one built to be exactly round-tripping; this is that a round-trip theorem is false of the target, not a quality judgement.

Independent reproduction. None known.

Reproduction

./verify.sh --quick

Toolchain: Lean 4 leanprover/lean4:v4.32.0 (Std only, no Mathlib), Python 3 stdlib, a C99 oracle
Expected output: 16 gates pass, exit 0; PORT_WRONG = 0
Claim stated at: repowazdogz-droid/vsf-cjson · PAPER.md:79-84,96-97
Verified at: repowazdogz-droid/vsf-cjson@dcdae40b (2026-07-20)

This pass. Confirmed by source read at dcdae40b; the 16-gate harness was not re-run this pass.

Artifact: repowazdogz-droid/vsf-cjson