jsonparser is a decade-old Go JSON library, maintained inside this practice and depended on across the cloud-native world. We ran the audit we sell against it, in public — and published the evidence behind every finding, the two defects that escaped us included.
The subject is jsonparser, a decade-old Go library maintained inside this practice. It went first on purpose, as code we could not hide from. The dashboard is public, it is served from the same portal a client gets, and we do not edit what it reports.
portal.reqproof.com/projects/jsonparser
The verification panel reads Needs attention because that is what the run said. The branch matters: proof-demo (our probelabs/jsonparser fork, not buger/jsonparser) is the showcase branch, and its 10 open findings are seeded demonstration entries (read the labels first). The three counts below are read off master, not this shot.
123 requirements28 approved4 issue records, every one fixed2 misses published
These counts are an index to the artifacts, not the argument, and each one is a directory or a document you can count yourself. All four are read off master, which is why they do not match the seeded showcase branch in the shot above. proof/problem-reports/ holds eight defect files, all fixed; two were reported by outside contributors and credited by name in the changelog, which leaves six the review found itself. The register shows four known-issue records (KI-1 through KI-4; KI-2 and KI-4 were fixed later, in v1.6.0), and two of the defects are published as misses, walked in full below — the changelog names three more, fixed in v1.3.1 with no postmortem of their own, a gap in the register rather than an absence of misses.
Overview
The latest run, the commit it ran on, and whether verification is complete.
Findings
The issue catalogue: known issues, problem reports, accepted risks and failing checks, by kind.
Requirements
Every requirement with its specification, rationale, obligations, evidence and trace links.
Audit checks
The checks behind the gate, and which of them are passing on this commit.
Map
The intent graph: requirements, code, tests and hazards, and the edges between them.
Timeline and activity
What changed, when, and which evidence had to run again because of it.
One requirement, and every artifact attached to it. Each step below is a file in the public repository. Open them in order and you have checked the chain yourself, without asking us anything.
The corpus behind this chain, counted by the product, not by us: 123 requirements — 7 stakeholder, 116 system, no software level in this project. The status column is mixed on purpose: the top stakeholder row reads review, the same fact step 01 states about STK-REQ-005. Same run as the dashboard, so the branch note covers its header count too.
The finding, walked in time
01requirement
SYS-REQ-009approved
Set() replaces the addressed value, creates a type-consistent path, or returns KeyPathNotFoundError. A person who owns the code approved that sentence before any code was judged against it.
An array-index path component under an object parent produced malformed JSON output, and Set() returned it with a nil error. The caller had no signal that the bytes could not be parsed again.
One executable test, pinning the failure while it was live: it asserted that the output was not valid JSON. The file carries // Verifies: SYS-REQ-009 and // Reproduces: KI-3 on one screen, so it says which promise it proves and which failure it pins.
The record names the code that carried it and dates it to the library's first release, so every revision before the fix is affected. The requirement's own history stamps the window: verification failing on 26 July 2026, passing again the next morning.
Set() now replaces a mismatched container with the type the path expects, so every non-erroring call returns valid JSON. The defect record names the root cause, the obligation it added, and the regression test.
The same test as step 03, still in the suite, flipped at the fix: it now asserts that every cross-type call returns valid JSON. The obligations on the requirement run against it again.
The same sentence as step 01, re-approved by the engineer who owns the code once the hardening was attached, with the defect named in the record as the reason for the re-approval.
Fig. 01 · Seven steps, seven records, and each one is a file in the public repository. The requirement that opens the chain is the requirement that closes it.
The same chain, file by file
01
Stakeholder promiseSTK-REQ-005status: review
Users update or delete addressed JSON values through the experimental mutation helpers, with deterministic edge-case behavior.
Read the file and the third line says status: review. The promise at the top of this chain is still a candidate, not an approved requirement, and we left it in view rather than starting the chain one step lower. The approved sentence is the next step, and that is where the obligations and the evidence attach.
Set must update the addressed JSON value without corrupting unrelated structure.
Approved means a person who owns the code approved the requirement. Until a requirement is approved it is a candidate, and nothing is judged against it. The line above is our summary of it; the approved text is the description field in SYS-REQ-009.req.yaml, and it is longer and more exact than a card can carry. The file names the reviewer and the role, and it records that it satisfies the promise in step 01.
Boundary, idempotency, malformed input, nested mutation. What must hold for the requirement to count as verified, and which evidence proves each one.
The obligations are where a requirement stops being prose. Each one is listed in the requirement file next to its worst case, and the manifests that satisfy it live beside them, so an unmet obligation is a visible hole rather than a silence.
The comment directly above func Set lists every requirement that function carries, SYS-REQ-009 first.
The annotation is in the source, not in a spreadsheet next to it, so it moves when the code moves. Follow the link and the highlighted lines are the annotation and the function it sits on.
The register entry: severity with its basis, the evidence, and the review dates.
A known issue is an unresolved problem. It stays a known issue until the closure is verified, and the register says which state it is in. This one now reads status: fixed.
Defect recordDEFECT-260726-MFPAcovered by requirement
The history that stays after the fix: root cause named, hardening recorded, reproducer pinned in CI.
The requirement that opened the chain is the requirement that closes it, proven again on the fixed code. This record strengthens SYS-REQ-009, which is step 02.
Nothing in that chain is a screenshot of a screen that does not exist. Every step is a file in a public repository, and the links above go to the files themselves.
03 · The record
Resolved defect records
A resolved defect record is what stays after a fix is verified. It carries what was expected, what happened instead, the test that reproduces it, the basis for its severity, the evidence, and the retest. This is DEFECT-260726-MFPA, the record for KI-3, read off the public register.
DEFECT-260726-MFPA · KI-3 · Set() / array-index path under an object parent
Fixed
Expected
Set writes the value at the addressed path.
Observed
Malformed JSON output on array-index paths under object parents.
Reproducer
set_spec_test.go· // Reproduces: KI-3 (fixed) ·go test -run TestSetArrayIndexUnderObjectMalformedJSON_KI3
While the bug was live this test asserted the bug: it pinned the output as not valid JSON. It was flipped at the fix and now asserts the opposite, so a regression trips it either way. It was never red and then green, and saying so would have been the easier story.
Severity
high · basis: reproducer. Our assessment, weighted by reachability and impact. A starting point for the maintainers' triage, not a CVSS determination.
Fixed and pinned. The reproducer stays in CI as a regression test.
One reproducer settles the instance. Closing the whole defect class takes broader evidence, and the record states which of the two it claims. That distinction is the difference between a bug that is gone and a failure mode that cannot come back.
04 · The ledger
The public ledger
The ledger exists for formal accountability, not for marketing. Every entry is dated, publishes its own triage boundary, and names the person who validated it or says why the name is withheld. The miss sits on the same page as the fixes.
No reproducer, no finding.
A finding you cannot re-run is an opinion with formatting. The reproducer, not the signature, is what gives a finding its authority.
The register, read off master
6
found by the review
2
reported outside, credited
8
defect files on master
4
known-issue records shown in this register
Fig. 02 · The register lists known issues; the full defect
history sits beside them in proof/problem-reports/, and the two outside reports are credited by name in the CHANGELOG — they are the two misses published above. KI-2 and KI-4 were fixed later, in v1.6.0.
FindingWhat was wrongResult
KI-1
An empty key path component panicked in the key search instead of returning an error.
Four issue records on the project's master branch, every one of them status: fixed, every one of them carrying the command that reproduces it. The wider defect history, including the two misses below, sits beside them in proof/problem-reports/.
Originating issue
Where the problem came in, including when it came from a user rather than from us.
Defect record
The evidence-bearing history after the fix is verified: root cause named, hardening recorded.
Closure evidence
The test that pins the failure, and the named revision it was run on. Some pin it by failing until the fix lands. Some pin it by asserting the broken behavior while it is live and getting flipped at the fix. The record says which.
Class-closure status
Whether the whole failure mode is closed, or only this instance of it. The two are never merged into one count.
Fixing change
The change that landed upstream, and the release that carries it.
Affected requirements
Which promises this touched, so the evidence they depend on runs again.
We publish our misses, because a record that only contains wins has been edited.
The postmortem on this project is called Two Bugs That Escaped L3 Strict Proof Review, and two is the honest number. Both misses are in Set(). The affected code carried 100% MC/DC at the time, which means every condition in the decision logic we checked was exercised. It does not mean the behavior was correct.
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 the data, gone.
What escaped, two of two
Ask Set to write at the path "a" then "", and it panics. The empty path component is the same failure class a hazard sweep had already closed. The sweep found seven sites, fixed all seven and reported clean. The eighth was written keys[depth:][0][0] instead of keys[i][0], and the pattern the sweep matched on did not see it.
Why the checks passed
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. Nobody had written the requirement for what scalar arrays deserve, so no check was counting the case.
The panic site passed for a second reason. The sweep was looking for one spelling of an unsafe construct rather than for the property behind it, so a slice expression and a second index level were enough to hide the same mistake in plain sight.
The gap, in the postmortem's own words
“MC/DC has no notion of ‘correct’; it has only ‘exercised.’”
“An unspecified partition is simply not in any check's denominator.”
proof-gap-root-cause.md
How we found them
Not through the gate. Past that, the public record gives two accounts, and we are not going to quietly keep the one that flatters us.
What our own files say. The postmortem says both turned up on the same branch that filed the empty-key issue, on a later pass over code the strict posture had already cleared. Both problem reports in the register open with source: type: audit_finding.
What the project's changelog says. The release that shipped these fixes credits people outside this practice. The entry Fix Set data loss on scalar arrays (#267) describes the same silent overwrite quoted at the top of this section, and it ends “Reported by @Solaris-star (#286)”. The entry for the empty-key panics says the hazard sweep found them and, in the same paragraph, “Reported by @c-tonneslan (#284)”. That release's acknowledgments list both names again.
Two files in one repository disagree about where these came in, and the public record does not settle it. So we state the part that is not in tension: the gate stopped neither defect, and the project's changelog credits an outside reporter for each of them. A credit like that stands. Our own ledger promises to record when a problem came from a user rather than from us, and on these two entries it does not. That is a third gap, and it belongs inside this postmortem rather than underneath it.
What is not in dispute: both defects date to the library's inception, years before this work, so writing them was not the failure. Certifying around them was. Both sat inside the declared scope with evidence attached, so nothing about the boundary excuses either one. That is why they count as misses and why they get a postmortem.
The root-cause analysis, blameless, specific and public, on the project's master branch, next to the finding and the fix, where you can re-run both. It runs to six sections including a remediation table, and the last of them is titled What proof did right, because the specified hazards were caught precisely for being specified. It is not signed. Its author line reads proof-gap review, and what you check it against is the reproducers, not a name.
What changed after it
Two requirements that did not exist before, both now approved. SYS-REQ-110 says what Set owes an array index past the end of the array, for every element type rather than only the one the old code handled. SYS-REQ-111 says the empty path component is a defined input on every entry point and must never panic.
Then three pieces of machinery, because a requirement with nothing checking it is a sentence. A reference oracle compares output against the standard library. A path-mutating fuzzer explores the key path, not only the bytes. And a signal rule flags the unguarded dereference in every spelling, including the one the sweep walked past; its file says so in its own header.
The behavior the requirements namedEvery condition exercised. Coverage complete inside this boundary.
The behavior nobody namedScalar arrays under Set(), and the empty path component. In no check's denominator. Both misses lived here.
Coverage counts the code inside the boundary somebody wrote down. Both defects were outside it, and a complete number said nothing about that.
Coverage was complete. The proof was not.
This is the entry we lead with, and it is the reason to believe the rest of the page. An auditor that only shows you its wins is asking for faith. Open the postmortem and its own first line will tell you the count is two.
Everything above resolves to a file in a public repository. Here are the six you can open — the repository, the requirements, the live map, one reproducer, the register and the postmortem — each under the project's own licence, each checkable without asking us anything.
portal.reqproof.com — the dashboard, the findings, the requirements and the graph. No account, no sales step. seeded showcase branch; read the labels first
