This page contains nothing you have to take on faith.
01 · The subject
Live project dashboard
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
On the run in this shot the verification panel reads Needs attention. That is what the run said, so that is what the page says. Read the branch line too: this is proof-demo (on our probelabs/jsonparser fork, not on buger/jsonparser), the showcase branch, and the 10 open findings on it are seeded demonstration entries, described in section 06. The three counts below this figure are read off master, not off this shot. Tinted to this page’s palette by a CSS filter; the portal’s own colours are different.
123 requirements28 approved4 issue records, every one fixed2 misses published
Counts are the cheapest thing an audit produces. They are an index to the artifacts below, not the argument. All four are read off master, which is why they do not match the seeded showcase branch in the shot above. Six defects, four known-issue records, eight defect files. proof/problem-reports/ holds eight records, all fixed on master; two of the eight were reported by outside contributors and are credited by name in the changelog, which leaves six the review found itself. The two published misses are those same two, so they sit beside the six rather than inside them. The register shows four known-issue records because KI-2 and KI-4 were fixed later, in v1.6.0. Two is what the postmortem documents. The project’s changelog declares three more: v1.3.1 says it “fixes 3 bugs that escaped the initial proof review”. Those three have no postmortem of their own, so they are not on this register, and that is a gap in it rather than an absence of misses. Each of these four numbers is a directory or a document in the repository above, so you can count them yourself.
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 this chain comes out of, counted by the product rather than by us: 123 requirements, 7 stakeholder and 116 system, and a software level that is empty because this project does not have one. The status column is mixed on purpose. The stakeholder row at the top reads review, which is the same thing step 01 below tells you about STK-REQ-005. Same run as the dashboard above, so the same branch note applies to the finding count in its header.
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.
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.
What this record does not prove, stated the way we would want a vendor to state it to us. Each of these is current. When one stops being true, it comes off this list, and the ledger will show why.
One public subject, and it is the friendly case.
jsonparser is a library: bounded, pure, no state carried between calls, no network, no scheduler. Nothing on this page shows how the method holds on a distributed service, a database, or a codebase with ten years of concurrency in it.
We chose it, and we maintain it.
Nobody handed us this repository. Recovering intent from code you already know is the easiest version of the job, and a self-selected subject is a weaker claim than an assigned one.
The open entries on the public dashboard are seeded.
The showcase branch carries demonstration defects next to the real history, and each one says so on its own page. The campaign's real findings sit under Fixed. If you open the dashboard expecting a live defect queue, read the labels first.
Two published misses are not a measured rate.
The postmortem records two, and this page said one until somebody read the document and counted. We know about the misses that have surfaced, whoever surfaced them. We do not know about the misses nobody has surfaced yet, and no page can honestly tell you that number.
Some of what we publish was reported to us.
The project’s changelog credits an outside reporter for each of the two published misses. Our own problem reports file both as audit findings. We have not reconciled the two records, we are not going to argue with a credit, and until the ledger carries the reporter the way it promises to, do not read our finding count as a measure of what this practice caught by itself.
Evidence only covers the promises somebody wrote down.
We judge behavior against the requirements that were approved. Behavior nobody named is outside every check, which is exactly what both published misses cost us. An empty finding list is not an empty defect list.
An approved requirement can be wrong.
Requirements are recovered by machine and approved by a person who owns the code. If that sentence is wrong, the gate will defend the wrong promise, on every commit, until somebody notices.
Nobody audits this register except us.
There is no outside party checking the ledger today. The reproducers exist so that you do not have to take our word for it: they are a check you run, not a certification we hold.
07 · The bar
Public methodology
The bar this work is judged against is published, and it is written to survive a hostile reading. It is not restated here, because a summary of a bar is not a bar.
One open-source pre-release audit each quarter, self-funded, coordinated with the maintainers and run on their schedule. No invoice, and no commercial follow-up.
This ledger has to earn the right to be believed, and open source is the only place it can. A client's requirements corpus describes their product in enough detail that publishing it would publish the product, and no permission fixes that. So the public record grows one self-funded open-source audit at a time, and paying our own way keeps the entries free of anyone's release marketing.
Maintainers, apply with the repository and what worries you most about it. If a release is coming, say when.
The map of the promises we recover, joined to the code that carries them and the tests that check them.
The findings, each one validated by a person before it reaches you.
Each finding carries a test you can run, and the record carries the command that runs it. Run them yourself. Keep them in your suite.
