Continuous Correctness Audit
We audit whether your software does what you promised.
A Continuous Correctness Audit is a standing engagement against a written bar. We formalize the requirements for one component you choose with us, your engineers approve them, and we prove and test the code against every approved clause. The findings, the proofs and the audit gate stay in your repo, where your CI re-runs them on every release. The claim is bounded on purpose: within a declared scope, for declared behaviors, with evidence commensurate with the consequence of failure.
Every finding is signed by name, so we take a limited number of engagements each quarter. Scoping requests go through the form at the end of this page.
Two ways to buy it.
Baseline Correctness Audit
One component, chosen with you. We scope it and quote a fixed fee before work starts. Roughly four weeks end to end, from requirements approval to a gate in your CI. Re-verification of your fixes is included: when you fix a finding, we confirm the reproducer passes and the proofs still hold.
The continuous retainer
After a baseline, the audit that doesn't expire: a retainer on the cadence you choose, per release, weekly, even daily. Sized to that cadence when scoped, then flat month to month. It buys: every release re-audited; new and changed code held to the approved requirements; fixed findings re-verified and pinned; the register maintained, severities re-checked; and one more component brought under the bar each quarter, included. Month twelve checks strictly more than month one.
In either shape, fix work is scoped separately from the audit, so the party grading a fix has no stake in having written it.
What the four weeks look like.
Week one · Requirements the owners approve
We index the component first: the code, as the source of truth for what it actually does. Then its history, and the systems where intent lives: the issue tracker, the support queue, the docs nobody updated. Code knows what it does; it doesn't know why. The why is what we recover. Requirements drafted only from the code would mirror its assumptions, so every requirement carries recovered intent, and the engineers who own the component approve each one before any code is judged, about two hours of their time, because the drafting is ours. In our first engagement the approval step alone surfaced seven undocumented design decisions the team itself disagreed about.
Week two · Formalize and prove
Approved requirements become formal properties. We check the spec itself first, for realizability, consistency and vacuity, so a bad clause cannot condemn good code. Then proofs and coverage runs begin.
Week three · Gap analysis and findings
Where the code and the approved requirements disagree, we write it up. Every finding ships under the reproducer guarantee in § 6, or it does not ship.
Week four · Evidence handoff and gate
The evidence corpus lands in your repo and the audit gate wires into your CI. We walk your team through every finding and every proof.
What stays behind.
your-repo/ ├── specs/ │ └── <component>.req.yaml ← approved by your engineers ├── src/… ← // SW-REQ-XXX ├── tests/… ← // Verifies: SW-REQ-XXX └── evidence/ ├── findings/F-XXX_test.go ← fails on main until fixed └── formal/<component>.log
A file tree in your repo, not a PDF in your inbox. What you own at the end is a verification harness most teams never get to build for themselves: per-finding reproducers, regression tests that pin fixed defects, condition-level MC/DC on the component's decision logic (a strictly harder bar than line coverage), and formal checks on its requirements, in plain YAML and executable tests in your git.
The corpus ships with a dashboard over it: every requirement and every known issue, with status and evidence, readable by the people who will never open the repo. On the known-issue screen, a copy-ready prompt hands a coding agent everything it needs to start the fix: the issue, its context, the reproducer. The dashboard is a window over the corpus; the record itself stays in your repo. A public example is live: the jsonparser dashboard, the same view your engagement gets, on our own open-source audit.
What changes after week four.
After week four, the register does the work. Known issues become scheduled fixes the gate grades. When a customer reports a bug, you check the register before you open a debugger. And when a defect does slip through, we widen the bar so its whole class cannot slip through again. The full picture, month two to month twelve →
Five commitments, in the contract.
- Reproducer guarantee. Runnable or it does not ship. Every finding arrives with a reproducer that fails on your current main and the name of the reviewer who validated it.
- Severity escalation. A finding we assess at our highest severity reaches your named contact within one business day of validation. It does not wait for the weekly report.
- Regression guarantee. Every fixed defect becomes a regression test in your CI. If the defect returns, your build fails before anyone has to remember it existed.
- Bounded claims, in writing. The scope, the behaviors and the depth of evidence are written into the contract. We sign what we checked and nothing beyond it.
- Zero lock-in. The gate runs without us. The corpus is plain YAML and executable tests in your git. If you cancel, everything that runs stays yours; what ends is our ongoing involvement.
What we will not claim.
- This is not a penetration test. We audit whether the software does what you intended. Attack-surface review is a different discipline, and we complement it.
- This does not replace static analysis. Pattern scanners catch known bug shapes cheaply; keep them running. We audit against requirements the owners approved, which no scanner has read.
- We will not claim total correctness. No audit can. Our signature covers the declared scope and declared behaviors at the stated depth of evidence, and it stops there.
- Performance is out of scope. Throughput, latency and capacity belong with your performance engineers.
- Severity labels are ours: our assessment, weighted by reachability and impact; a starting point for your triage, not a CVSS determination.
The longer table of what this audit cannot see is on the methodology page.
Before the form.
Worth your time if
- You can already name the component. Most readers who get this far can.
- A failure in it costs money or trust you can put a story to.
- Your release process is settled enough to host a gate.
- The engineers who own the component will give week one about two hours.
Today we audit Go, Rust, JavaScript, TypeScript, and Solidity at production depth. Python, Zig, Java, and C# are newer; we will tell you honestly where each stands. C and C++ arrive through the compiler's own coverage measurement, in the same gate. Another stack? Say so on the form and you get an honest timeline.
Request confidential scoping.
Findings are signed by name; who signs is its own page. Your email is the only required field; the rest is optional context that lets us come prepared. We reply personally, with a scoping call or an honest no. Fees are quoted after scoping and fixed before work starts. For private code, we countersign your NDA before reading a line.