Software, held to what was promised.
Security firms audit whether your software can be broken into. We audit whether it works.
Composition of one audit
A Continuous Correctness Audit is a standing, machine-checked statement of what one component of your software is required to do, and evidence — re-runnable evidence — that it does it.
Every quantity on the label opposite is taken from a real, publicly inspectable audit. Nothing on it is estimated, projected, or asserted by its author without a check behind it. Where the method failed, the failure is on the label too.
The Gate
The audit runs in your CI, on every change. When a requirement cannot be shown to hold, the pipeline exits non-zero and the change does not merge. There is no dashboard to ignore and no report to file away. The gate is the deliverable.
$ proof audit --fail-level warn continuous correctness audit · 52 checks · 4 evidence classes requirement_approval ............. PASS 123 approved formal_proof / kind2 ............. PASS formal_proof / z3 ................ PASS coverage / mcdc .................. PASS 100.0% hazard_analysis .................. PASS per requirement finding_register ................. FAIL 1 open FINDING F-XXXX requirement not held under boundary input reproducer: findings/F-XXXX/repro.sh · signed: named reviewer exit status 1
The Evidence
Four classes of evidence are admitted: formal proof, condition-level coverage, runnable reproducers, and named signatures. Author-asserted metadata is not evidence and is not admitted. Everything below re-runs from the repository.
evidence/ ├── requirements/ 123 approved · FRETish ├── proofs/ │ ├── kind2/ model-checked │ └── z3/ SMT-solved ├── coverage/ │ └── mcdc/ condition-level, avionics bar ├── hazards/ per-requirement analysis ├── findings/ 7 · reproducers attached ├── misses/ │ └── 0001-set-silent-loss/postmortem — published └── signatures/ named reviewer, per finding
The Public Audit — jsonparser
We audited buger/jsonparser, a widely used Go JSON library, in public. The full register — requirements, findings, and the miss — is open for independent inspection at portal.reqproof.com/projects/jsonparser.
| Ref | Item | Qty | Disposition |
|---|---|---|---|
| REQ | Requirements, approved | 123 | IN FORCE |
| F-ALL | Findings, confirmed real bugs | 7 | REPRODUCERS ATTACHED |
| F-PANIC | of which: one panic class | 8 sites | CONFIRMED |
| MISS-001 | Silent data loss in Set() — escaped under 100% MC/DC | 1 | PUBLISHED · RE-RUNNABLE |
The Method
Standard instruments. Aviation-grade lineage. Applied to ordinary software, which is where the money actually is.
| Part No. | Designation | Function | Origin / Note |
|---|---|---|---|
| MTH-01 | KIND2 | Model checker — formal verification of requirements | Proves, not tests |
| MTH-02 | Z3 | SMT solver — formal verification of requirements | Proves, not tests |
| MTH-03 | FRETISH | Structured requirement language | NASA flight-software lineage |
| MTH-04 | MC/DC | Condition-level coverage measurement | Avionics certification bar · 11 languages incl. Go, Rust, Solidity, Zig |
| MTH-05 | HAZARD ANALYSIS | What happens when each requirement fails | Performed per requirement |
The Engagement
Terms are short because the deliverable is not a document. It is a gate that keeps running after we leave.
The Signature
No finding in this practice is issued anonymously. A named reviewer signs every finding and answers for it — by name, not by brand. If we are wrong, you know exactly who was wrong.
Request for Scoping
Complete the form below. Submission constitutes a request for scoping and nothing else.
A named human will respond.