Methodology
The bar we audit against
Proof audits whether software does what was promised, against a published bar. Six clauses. Each one enforced by a machine check, each one anchored in practice older than us. “Verified” should be a claim you can re-run; this page is what we mean when we say it.
Why “verified” needs a definition
When paperwork can be generated faster than it can be read, the artifact stops being evidence, and the word “verified” carries no information unless whoever says it publishes what it means. Here is what we mean. A claim is verified when you can re-run it: the requirement it traces to, the check that enforces it, and the reproducer that fails without the fix, all executable by you, on your tree, without us in the room.
Scope note: this is the bar we hold ourselves to, not a certification scheme. Nobody accredits it and nobody is asked to adopt it. It is published so you can hold us to it.
Six clauses, each with the check that enforces it
A clause without an enforcement mechanism is a preference. Each clause below names the machine check that fails when the clause is broken, and the external practice the clause is drawn from. The instruments behind the checks are their own page.
1 · Requirements are proven before code is judged
CLAUSEEvery requirement in scope is written in structured English with formal semantics, then proven realizable, consistent and non-vacuous before any code is judged against it. A spec that contradicts itself, or that a do-nothing system could satisfy, is a defect in its own right, and it is found first.
THE CHECKRealizability, consistency and vacuity are discharged at spec time by the Kind2 model checker and the Z3 solver. A requirement that fails them never enters the audit.
THE ANCHORNASA's FRET program, which gave structured English requirements machine-checkable semantics. In FRET's published research, a realizability check caught an eVTOL spec defect that permitted backwards flight, in 14 seconds.
2 · No reproducer, no finding
CLAUSEEvery finding ships with a runnable reproducer that fails on the scoped tree, or it does not ship. A finding you cannot re-run is an opinion with formatting.
THE CHECKThe reproducer is executed before delivery and observed red. No red run, no ledger entry.
THE ANCHORCoordinated-disclosure practice in security research: proof of concept before report, so the recipient can verify before they triage.
3 · Traceability at 100% precision
CLAUSEEvery requirement in scope carries links to the code that implements it and the test that verifies it. Every link that exists is machine-checked to resolve, and a named reviewer answers for it pointing at the right clause: precision, not recall.
THE CHECKThe annotation resolver walks every link on every run; a link that fails to resolve fails the gate, and code answering to no requirement is flagged as orphan from the other direction.
THE ANCHORBidirectional traceability, required by DO-178C in avionics and ISO 26262 in automotive, for the same reason it is required here: unlinked evidence cannot be audited.
4 · MC/DC on the decision logic under audit
CLAUSEThe decision logic under audit gets condition-level MC/DC (modified condition/decision coverage): every condition in every scoped decision is shown to independently affect the outcome, so a test suite cannot look thorough while exercising half the logic. Together with clause 3, this is coverage counted twice: once against the intent, once against the code.
THE CHECKMC/DC instrumentation measures coverage on the scoped decisions. The number is measured, never estimated.
THE ANCHORDO-178C Level A, the coverage bar avionics sets for software whose failure is catastrophic.
5 · A named reviewer signs every finding
CLAUSEA named reviewer signs every finding before it reaches you.
THE CHECKThe gate refuses to deliver a finding without a recorded reviewer identity on the finding record. There is no delivery path that skips it.
THE ANCHORThe oldest norm in professional practice: an audit opinion carries the engagement partner's name, an engineering drawing carries the stamp of the engineer who answers for it.
6 · The gate re-runs, and runs without us
CLAUSEThe audit gate re-runs on every change and runs without us. If the evidence could only be checked in our presence, it would be testimony, and this page promised you evidence.
THE CHECKThe gate runs in your CI, on your infrastructure, with no network dependency on us and no license check. If we disappear, it keeps running.
THE ANCHORThe reproducibility norm in experimental science: a result only the original lab can produce is not yet a result.
What this audit does not see
Assurance here is bounded on purpose: within a declared scope, for declared behaviors, with evidence commensurate with the consequence of failure. The table below is the edge of that boundary, by failure class.
| Failure class | Coverage | Note |
|---|---|---|
| Logic and intent gaps | Covered | The core of the audit: behavior that violates an approved requirement, or a requirement the team never wrote down. |
| Boundary and error-path defects | Covered | Condition-level coverage forces the branches ordinary suites skip. Error paths are where most of these hide. |
| Concurrency interleavings | Partial | Modeled where declared, rarely exhaustive. The report states which interleavings were checked. |
| Performance under load | Not covered | We make no load, soak or latency claims. A correct system can still be a slow one. |
| Security-relevant behavior | Covered, in scope | Security promises inside scope are audited like any other requirement (white-box; attack classes named at scoping). Not a certified pen test — see Engagement exclusions and the row below. |
| Penetration testing and red-teaming | Not provided | We do not deliver a certified penetration test, black-box red-teaming, infrastructure testing, or social engineering. Where a compliance framework or customer review requires one, engage a security firm; our evidence complements theirs and substitutes for none of it. |
| Third-party dependency internals | Not covered | Dependencies are held to their declared contracts. We do not audit inside them unless that is scoped separately. |
Signed intent: where the spec comes from
The audit starts by reading what you already have. The code first, as the source of truth for what the component actually does. Then its history, for what changed and when. Then the systems where intent actually lives: the issue tracker and the support queue, for what the component promised and where it failed someone. Code knows what it does. It doesn't know why. The why is what we recover.
The recovery matters because requirements drafted only from the code would be circular: they mirror the code's assumptions and grade the code against itself, and every defect already in the code becomes a clause the spec blesses. So the recovered requirements go to the engineers who own the component for approval before any code is judged, which anchors the bar outside both the code and whoever wrote it. On one engagement, an enterprise API gateway, that step produced 47 approved requirements in about two hours of the owners' time. Judged against those requirements, the component surfaced a nil-pointer crash class that every existing test had missed. The tests had been written against the code. The requirements were written against the intent.
For every requirement, the worst case
Formalizing what the component should do is half the method. The other half asks, for every requirement, what the worst case is, the way regulated industries do. We walk each requirement against a catalog of more than 300 obligation classes, from binary framing that must bound its length before allocating, to compound operations that must stay atomic under concurrent writers, to file permissions that must be final at creation. Every class considered gets a recorded decision: accepted, suppressed with a signed rationale, deferred as documented debt, or drafted as a new class specific to your application. Nothing exits the pass silently.
Each accepted obligation declares the evidence that proves it: fuzzing for parser robustness, property-based tests for algebraic promises, the race detector for concurrency, negative tests for malformed input, a solver proof where a test cannot reach. The worst case and its severity are written down per requirement, never defaulted from a checklist.
Severity, and what happens when we miss
Severity on every finding is our assessment, weighted by reachability and impact; a starting point for your triage, not a CVSS determination.
The ledger also shows the triage boundary. Engagement reports include what we investigated and dismissed, with the reason each candidate was closed, so you can see where the audit stopped looking and judge whether it stopped in the right place.
And when a defect escapes the audit entirely, it is not quietly absorbed. The escape is recorded with its root cause named: which requirement was missing, which test partition, which coverage condition. Closure requires corrective artifacts, and a claim that a whole bug class is fixed is only as strong as the evidence behind it. The ledger's first entry is this protocol applied in public on jsonparser; the case is public.
How AI is used
Drafting is machine-assisted. Requirements, reproducers and candidate findings are drafted with AI, and nothing is trusted as drafted: deterministic checkers reject invalid work, including requirements that fail realizability, reproducers that never run red, and links that do not resolve. What survives the checkers goes to a named reviewer, who signs the finding or kills it.
We call this posture expert-signed, machine-verified. You will not read a claim here that AI was kept away from the work. The claim is that nothing machine-drafted reaches you unchecked, and that a person with a name signed what did.
Hold us to it
The bar above is applied inside one kind of engagement. What can be shown publicly accumulates in the ledger; client corpora never do, by design.
The ledger includes one miss of our own, with its postmortem.