Case study · public audit · July 2026
Ten years of jsonparser, and the bug that got past us.
We took the audit we sell and ran it, in public, on a library our founder has maintained for a decade: jsonparser, a Go JSON parser with 5,500+ stars that ships inside Grafana Loki and, transitively, a good slice of the cloud-native stack. This page is the whole story: what the audit found, what it fixed, and the defect that got past it anyway. Every claim resolves to a public artifact.
The whole corpus is browsable live: portal.reqproof.com/projects/jsonparser: every requirement, every known issue with its reproducer command, and the map linking each requirement to the tests and code that verify it.
Why our own library went first.
An audit practice should start on code it cannot hide from. We picked the subject we could not hide from: our founder's own parser, ten years old, widely deployed, with a decade of issues, community fixes, and continuous fuzzing already behind it. Code we had every reason to trust, which is exactly the code that teaches you what trust is worth.
The stakes were not hypothetical. jsonparser sits in dependency graphs it never asked to join: log pipelines, service meshes, API infrastructure. A silent bug in a library like this becomes somebody's incident, three layers up, with a green build.
What the bar looks like when it is actually applied.
The behavior of the library was formalized into 123 requirements: 7 stakeholder-level promises and 116 system-level clauses; 116 of the 123 carry a machine-checkable formal specification, FRETish compiled to temporal logic. All 279 functions traced to the requirements they serve. Condition-level MC/DC measured at 100% of decisions and 100% of conditions. A corpus of proved solver lemmas over the parser's core invariants. Sixteen million executions of a structure-aware fuzzer built mid-campaign. The strict audit gate: zero errors, zero warnings.
One calibration story. Years ago, OSS-Fuzz caught a real panic in Delete by mutating bytes at random. Encoded as a solver constraint against the formalized spec, the same defect fell out as a Z3 counterexample in six milliseconds. Random search found it once, by luck; once specified, it cannot be missed again.
Seven bugs, one of them wearing eight costumes.
The review surfaced seven real bugs: four panics, two data-corruption defects, one encoding fault. The four panics were largely one bug in eight spellings: the same unchecked dereference, repeated at eight sites across the codebase. The hazard sweep caught seven of the sites. The eighth, hidden behind a slice operator and a byte literal, only surfaced during the root-cause analysis of a different miss entirely, the one that gets its own section below.
The OSS-Fuzz question answers itself in one line from the postmortem: the harness had hardcoded the key path "test", and no amount of byte mutation can discover a panic that requires an empty path component if the path is never mutated. We built and published a structure-aware fuzzer in response; it runs at roughly a quarter million inputs per second.
The audit also caught the benchmark lying: since 2017, the suite had been measuring a different library under encoding/json's name, and the issue reporting it had been open for nine years. And it made the parser faster, not slower: formalizing string handling exposed an unbounded backslash scan, and the fix took one hot path from 128 microseconds to 22.
The campaign scoreboard, for completeness: 50 open issues to zero. Twelve open pull requests to zero. Twelve real bugs fixed in all, the seven from the review plus five more shaken out of the decade-old backlog, across six releases in three days, with zero breaking changes.
Then the audit missed one.
Ask Set to write 9 at index [5] of the array [1,2], and it hands you back [9]. No panic. Valid JSON. The rest of your data, gone. The branch that should have grown the array only fired when its first element was an object; scalar arrays fell through to code that overwrote them, and a comment in the source described the overwrite as intentional. The defect predates the audit by years; the failure was not writing the bug but certifying around it. It reached us from the community, the way escapes usually do, and the fix landed and was pinned in the release train that followed.
The affected code carried 100% MC/DC at the time. The postmortem does not soften what that means: "MC/DC has no notion of 'correct'; it has only 'exercised.'" And the deeper sentence under it: "an unspecified partition is simply not in any check's denominator." Nobody had written the requirement for what scalar arrays deserve, so no check on earth was counting it.
What worked, what did not, in writing, in public.
We published the root-cause analysis the way we would demand it from a client's vendor: blameless, specific, and public. What worked: the hazard sweep found seven of the eight panic sites; the specified hazards were caught precisely because they were specified; coverage was an honest 100% of the code that existed. What did not, in three ways: partitions nobody specified, an output oracle nobody wrote, and a pattern matcher that recognized one spelling of an unsafe idiom but not its sibling.
The document's hardest passage, paraphrased against ourselves: the toolchain proves that the code does what the spec says, safely, in the shapes the spec and sweep recognize. It cannot find behavior the spec never named, correctness no oracle checked, or unsafe spellings the matcher never generalized. That is not a disclaimer. That is the honest boundary of the discipline, and knowing it is what the audit sells.
Then every escape became a gate: an obligation that inputs are never mutated, a differential oracle against a reference implementation, a signal rule that generalizes the unsafe spelling beyond the one form it knew, and a lint that checks the benchmark labels tell the truth. The misses got more than fixes: each one retired as a class.
The corpus, organized the way yours would be.
Everything this site describes in the abstract exists concretely in that repository, laid out the way every client corpus is laid out. This is the live exhibit: how requirements are stored, how code and tests declare what they answer for, and where the defect history lives.
specs/stakeholder/requirements/ ← 7 promises the library makes (STK-REQ-…) specs/system/requirements/ ← 116 testable clauses (SYS-REQ-…), plain YAML parser.go ← functions annotated with the requirements they implement set_spec_test.go ← // Verifies: SYS-REQ-009 and // Reproduces: KI-3, on one screen proof/known-issues/ ← the register: severity with its basis, evidence, review dates proof/problem-reports/ ← DEFECT records: root cause named, hardening recorded proof/signals/rules/ ← the unsafe pattern from the postmortem, generalized into a sweep proof/ ← evidence, vectors, impact reviews, changes: the rest of the memory
This page contains nothing you have to take on faith.
Every claim above resolves to one of these.
The postmortem
The blameless root-cause analysis of the escape, on the public master branch.
The 123 requirements
The full formalized corpus: 7 stakeholder promises, 116 system clauses, plain YAML.
The repository
Specs, proof artifacts, reproducers, and the audit gate, in the tree where they live.
The ten-year writeup
The long-form account of the whole campaign, in the founder's own words.
This, pointed at your component.
The audit above is the same engagement we sell: requirements your engineers sign, the code held to them, the evidence in your repo, re-run on every release. The difference is that yours stays private, always; the trust page explains why that is structural, not preference. And the misses, when they come, get the same treatment you just read.
The engagement Back to the ledger What month twelve looks like