Projects · Formal verification · Research prototype · PROVEN

vsf-cjson

What this 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 this 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.

Trusted base

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.

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.

Result

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.

Reproduce

./verify.sh --quick

Toolchain

Lean 4 leanprover/lean4:v4.32.0 (Std only), Python 3 stdlib, a C99 oracle

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.

Independent reproduction

None known.

Prior art and positioning

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.

Links

• Source: repowazdogz-droid/vsf-cjson
• Finding: 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.