Artifact
vsf-cjson
Four kernel-checked theorems about a JSON parser and serialiser, with a differential over 120,000 inputs.
What it establishes
Four machine-checked Lean theorems about a JSON parser and serialiser, totality, round-trip on a canonical exact-number model, canonicity, and idempotence, together with a differential measurement against a C reference over a large fuzzed corpus.
What it does not establish
Grammar-soundness is not proved; the theorems are about the function, not the compiled binary, and the idempotence run is the only bridge. The corpus score is a measure of how faithfully a lax parser was replicated, not a quality score. The round-trip theorem holds only after numbers are modelled exactly; it is false of the C target's own lossy pipeline.
Method
The specification models JSON numbers exactly rather than as IEEE doubles, which makes the round-trip theorem true and provable and turns every number divergence from the C into a measured finding; a 16-gate harness and a 20-attack mutation suite guard the result.
Results
The four theorems are kernel-checked; the differential over 120,000 fuzzed inputs classifies 116,476 agree and 0 port-wrong; idempotence holds over 20,318 inputs.
What has to be trusted
Lean 4 (v4.32.0), Std only with no Mathlib; the axioms propext, Classical.choice and Quot.sound; no sorry and no native_decide. Also the Lean kernel, compiler and runtime, the C compiler, and the human-authored SPEC.md.
Prior work
JSON parsing, canonical serialisation (RFC 8785), and differential testing. The contribution is the exact-number specification that makes round-trip provable, and the account of what the C target lacks.