The method, and what it cannot see.
We scope one component, recover what it's supposed to do, and then look for the places where implementation, tests, and documented intent stop agreeing. Every finding clears five gates before it reaches you. The limits are on this page too, in a table.
The work is expert-signed and machine-verified: analysis carries the breadth and a named reviewer carries the judgment. These five gates are the triage boundary we publish, so you can hold any delivered finding against it and tell us where it falls short.
| Gate | What we check |
|---|---|
| Reproducibility | A runnable reproducer, test, fixture, replay, or trace ships with the finding, or the report gives a bounded explanation of why full reproduction isn't possible and what evidence is missing. For each reproducer we name the exact code change that flips it from failing to passing, so you can check that it tests the thing it claims to test. |
| Severity | Severity is our own assessment, weighted by reachability and impact, and it is offered as a starting point for your triage. It is not a CVSS score and not a vendor determination. The weighting takes in preconditions, required privilege, blast radius, data and security boundaries, resource-exhaustion potential, regression likelihood, and how hard the behavior is to detect from the outside. Disagree with the rating and the rationale is right there to argue with. |
| Noise control | Duplicates are merged and affected surfaces are checked against the code before anything is written up. A lead we couldn't validate is delivered labeled as a lead, with the evidence that made us look and the evidence we couldn't get. |
| Patch verification | Fixes are retested against the original reproducer and against adjacent cases in the same bug class. A fixed finding becomes a permanent regression test in your CI that fails the build the day the behavior tries to come back. |
| Disclosure | Client findings stay private. Publication, advisory language, and field-note reuse each need written approval, and coordinated disclosure timing is yours to set. |
Alongside the findings, the report lists the candidates we investigated and dismissed, and the reason for each. That list is how you check our noise ratio instead of taking our word for it.
The method, the validation gates, the instruments we use, and the limits table.
Client code and client findings, unless publication is approved in writing.
What the method covers, flags, and misses.
This table is where the boundary actually sits. Read the rows near the bottom first; those are the ones that change what you should buy.
An audit that names its own limits is the one you can take to your board. If a class in the bottom half of that table is where your worst incidents come from, say so during scoping. Some of it can be brought into scope with a bigger evidence budget. Some of it can't, and we'd rather tell you that before you buy.
| Failure class | Standing | What that means in the report |
|---|---|---|
| Behavior against approved requirements | Covered | We formalize the component's intended behavior and your architects approve that list before the audit runs. Disagreements inside your own team surface at this step, before any code is read. |
| Input handling, boundaries, error paths | Covered | Malformed input, ambiguous syntax, size bounds, error propagation, and whether the path fails closed. These carry runnable reproducers most often. |
| Regressions and fix quality | Covered | Everything previously verified is re-checked on the agreed cadence. A fix that introduces a new defect gets its own finding at its own severity. |
| Decision logic and stated invariants | Covered where the path warrants it | MC/DC and property proofs are used when the logic is dense enough that ordinary tests don't settle the question. Not claimed for every component by default. |
| Resource exhaustion and amplification | Covered as a correctness question | Inputs and request shapes that amplify CPU, memory, recursion, fan-out, or downstream work. We report the amplifying input. We don't produce load-test numbers. |
| Concurrency, ordering, cancellation, shared state | Partly covered | We write down the ordering, cancellation, and cleanup obligations the reviewed path carries. Where the available evidence can't settle one, that obligation is named in the report and flagged as uncovered. It stays on the register as an open obligation until something settles it. |
| Distributed-systems failure modes | Flagged, rarely resolved | Partition behavior, clock skew, replica divergence, and split-brain need fault injection against a running cluster. We name the obligation and the experiment that would settle it. A code-and-spec audit does not settle it for you. |
| Performance and latency behavior | Not covered | Where a requirement states a bound, we report that the bound is unmeasured. We don't measure it. |
| Security as a discipline | Not a substitute | Security-relevant correctness defects are reported at their real severity when we find them. This is not a penetration test and it doesn't replace a security audit. |
| Deployment configuration and infrastructure | Only if declared in scope | Production topology, runtime configuration, and infrastructure code are reviewed when they're named in the scope before work starts, and not otherwise. |
| Unreviewed components | Not covered | Scope is fixed in writing before work starts. Anything outside it is unreviewed, and the report says which parts of your system that includes. |
Five steps, run against one component at a time.
Pick the parser, protocol layer, policy engine, storage path, SDK, agent loop, or release window where failure would matter. Scope is written down and fixed before work starts.
Map what the component is supposed to do from requirements, docs, tickets, tests, code, and the promises your product page already makes. Your architects review and approve that list. Budget about two hours of their time per component.
Identify where implementation, tests, documentation, and expected behavior stop agreeing. Drift is where the defects live, and it's invisible to a suite that only checks what someone already thought to check.
Confirm each finding with a reproducer, a regression test, expanded coverage, MC/DC, or a formal artifact where the path warrants one. Anything we can't confirm is delivered as an open question with the evidence attached.
Retest patches against the original reproducer and adjacent cases, then rerun the whole corpus on the agreed cadence. Month twelve of continuous coverage checks strictly more than month one, because nothing leaves the corpus.
Used where they raise confidence.
None of these is claimed for every component by default. We reach for them when the reviewed path has decision logic, state transitions, or invariants where ordinary tests don't give enough evidence. When we use one, the artifact ships with the finding so you can rerun it yourself.
Line coverage tells you the branch ran. Branch coverage tells you both paths ran. MC/DC tells you whether flipping one condition on its own changes the result. If flipping it never changes anything, that's dead logic and your tests never noticed.
Kind2 takes the formalized requirements and checks whether any implementation could satisfy all of them at once. A specification nothing can satisfy is a design defect, and it shows up before anyone writes the code that tries.
A test samples. Z3 either returns a concrete input that violates the property or shows there isn't one inside the model. The model's assumptions ship with the proof, because a proof is only as honest as what it assumed.
For each reproducer we identify the exact code change that flips it from failing to passing. That's the check on our own evidence, and it's the reason a delivered reproducer is worth running.
Six parts, built for the engineer who owns the code.
A finding has to survive being read by the person who wrote the code, and then survive being rerun six months later by someone who has never heard of us. The same evidence that demonstrates the defect verifies the patch, or shows what's left.
A finding that can't be rerun isn't finished. A static paragraph loses its value the moment the codebase moves. A reproducer stays in the repository and keeps answering the same question in month twelve.
What the system should do, what it does instead, and which requirement or invariant that breaks.
Minimal steps, test case, input, or counterexample that demonstrates the behavior on the scoped tree.
Severity with its rationale: affected surface, reachability, blast radius, and regression likelihood.
Tests, traces, coverage, MC/DC, formal artifacts, and the reviewer's validation note, with the reviewer named.
Fix guidance aimed at the bug class rather than the one instance we happened to trip over.
Patch verification against the same evidence, with per-finding status when the report is re-issued.
Why patch verification is a gate and not a courtesy.
A fix is a change like any other, so it gets reviewed like one. A patch can close the tracked issue and leave the bug class open, and a green suite doesn't settle which of those happened.
This is the failure mode a point-in-time audit can't reach. The report you bought was true on the day it was written, and then the code moved. So the corpus keeps running after the report ships, and every fix is retested against the evidence that found the defect.
Set([1,2], "9", "[5]") returned [9]. No panic, valid JSON,
elements gone. We published that as a
blameless
proof-gap postmortem instead of hardening the tool and saying nothing. Coverage told us
the branch was reachable and had nothing to say about which output was correct.
A pre-release audit of a major open-source infrastructure tool, coordinated with its maintainers. The tool, the components, and the counts stay under embargo, so what we can show you is the method and the shape of the engagement.
The buyer should not depend on Proof to believe the report.
- Every delivered finding carries the affected surface, the severity rationale, the reproduction path, and its retest status.
- Reproducers and regression tests are plain files in your repo. They run in your CI, on your machines, without us.
- The corpus is plain YAML and executable tests. If the engagement ends, the gate keeps running and nothing has to be exported.
- Anything we deliver, you can rerun. That's the test we'd apply to a vendor, so it's the one we publish against.
- Fix work is scoped separately and never bundled into an audit. Route any finding to your own team at identical status. Where we do write the fix, acceptance is mechanical and signed off by your engineer rather than ours.
Scoped evidence, not total correctness theater.
No blanket claim that all software is correct.
- We don't claim full-system total correctness. No engagement can, and any vendor that offers it is selling you the wrong thing.
- Unreviewed components stay out of scope, and the report names which parts of your system that covers.
- Assurance is bounded: within a declared scope, for declared behaviors, with evidence commensurate to the consequence of failure. The same bound is written into the engagement contract.
- Client findings stay private unless publication is approved in writing.
Check the method against something we published.
The findings page carries dated entries with these gates applied, including the triage boundary for each one. Read a finding first. If the evidence doesn't hold up, the rest of this page is worth nothing to you.
Proof is founded and led by Leonid Bugaev, author of GoReplay and jsonparser. Every finding is validated by a named reviewer before it reaches you, and that reviewer's name is on the finding.
The data-handling and disclosure terms your security reviewer will ask for, and the instruments we audit with.