Research & instruments
The instruments
Every claim on this site rests on machinery. This page explains the machinery behind our audits.
We build the instruments we audit with.
The engine is called Proof, the same name as the practice, and it is proprietary. It compiles requirements, runs the solvers, measures the coverage, and refuses to pass anything it cannot trace. The engine carries the breadth of the work: every requirement, every annotation, every decision point, checked the same way on every run.
Review carries the judgment. A named reviewer decides what a result means, what it is worth, and whether it ships. The boundary between the two is a policy we hold to: publish our evidence, keep the engine. What it produces for our public work lands in the open where it can be re-run; the fullest example is the jsonparser corpus, and you can audit our audit there. What it produces for a client never lands anywhere public, for reasons the trust page explains.
Six links. Each one leaves an artifact.
01 Structured English, compiled
Requirements are written in structured English and compiled through a 288-template compiler descended from NASA's FRET, whose template semantics are formally specified. Ambiguity fails at compile time.
artifact: each shall-line's template ID, with its formal semantics attached
02 The specification judged first
Realizability, consistency and vacuity are checked before any code is judged (Kind2, Z3). A specification that cannot be satisfied, or is satisfied trivially, never reaches review.
artifact: a solver verdict on the specification itself
03 Proofs over all inputs
Z3 proofs over encoded core invariants hold for all inputs rather than a sample. The encoding is tied back to the code through the traceability layer, and a passing proof is a statement about every value the type admits.
artifact: an UNSAT result on the negated property
04 Traceability
Every annotation that exists is machine-checked to resolve and be correct (100% precision). Recall is covered from the other side: code that answers to no requirement is flagged as orphan.
artifact: a requirement tag on the function, a Verifies: tag on its test
05 MC/DC at code level
Code-level MC/DC in eleven languages: Go, JavaScript, TypeScript, Rust, Python, Java, C#, Solidity, and Zig instrumented directly, C and C++ imported from the compiler's own measurement into the same gate. This measurement has mostly lived inside certification suites built for embedded work; ours runs on the stacks teams actually ship, in ordinary CI, down to Solana programs. Every condition in every scoped decision must be shown to matter on its own, and the shapes we cannot measure are counted and reported, never silently dropped.
artifact: a per-decision verdict, condition by condition
06 The gate
A 52-check audit gate admits or rejects the whole chain. It runs in the client's CI and needs nothing from us.
artifact: one exit code, re-runnable by anyone with the repo
What the artifacts look like.
REQUIREMENT, COMPILED
While in degraded mode, when queue_depth exceeds MAX_DEPTH,
the component shall, within 250 ms, satisfy reject_new_work.
template XXX of 288 · semantics: NASA FRET
ANNOTATION PAIR
// SW-REQ-XXX
func RejectWhenSaturated(q *Queue) error { … }
// Verifies: SW-REQ-XXX
func TestRejectWhenSaturated_AtBound(t *testing.T) { … }
MC/DC VERDICT
mcdc component.go:XX decision (a && (b || !c))
3/3 conditions independently affect the outcome ✓
shapes only · placeholders throughout · drawn from no client engagement
The engine audits itself.
Proof runs under its own gate: more than 1,500 requirements across four specification levels, every function annotated, zero orphan code, checked on every change the same way client work is checked. The same discipline covers its own defect history: every recorded defect is root-caused to the gap that let it through and closed with evidence. A corpus that size, held green under its own audit, is hard to fake, and the vacuity checks in the chain above are what keep "green" from being gamed.
That corpus stays private, for the same reason client corpora do: a full requirements tree describes its system completely enough to rebuild it, and this one describes the engine. The public reference is the jsonparser audit, whose requirements, defect records, and evidence are browsable file by file.
Some instruments are public.
An OSS-Fuzz harness had run for years on jsonparser (the case study). It caught one real panic, and a whole defect class got past it, because it held key paths fixed while varying everything else. We built fuzzers that hold nothing fixed, for JSON and then for GraphQL, and published them. The third instrument, probe, is the search tool that walks code and corpus together.
github.com/probelabs/probe · github.com/probelabs/json-fuzz · github.com/probelabs/graphql-fuzz
Where the semantics come from.
The requirement templates descend from NASA's FRET program, built to state flight-software requirements precisely enough to check by machine. Its published record includes a realizability check catching, in 14 seconds, an eVTOL specification that permitted flying backwards.
In December 2025, Martin Kleppmann described where he wants software verification to go: "have the AI prove to me that the code it has generated is correct." That is the direction of travel; what we ship today is the enforcement half, a bar such proofs would have to clear.
What the instruments do not do.
No instrument here proves total correctness, and we claim none. Performance is outside the chain: the chain judges declared behavior and says nothing about latency or throughput. This complements security tooling; it does not replace it. And the limit we paid to learn in public: unspecified behavior is invisible to every check in the chain. The jsonparser escape is the standing proof.
What they deliver is bounded: within a declared scope, for declared behaviors, with evidence commensurate with the consequence of failure.
The audits are the first act.
We sell audits because accountability is what the market can buy today, and because it is the honest way to prove the discipline works: one component, one engagement, evidence a client can re-run. But look at what each engagement leaves behind: a machine-readable graph of what a system promises, how each promise is verified, what broke, why it broke, and what retired the class.
Software engineering has never had that graph. Code-writing agents make decisions in the dark: no ground truth for intent, no memory of past failures, nothing to check their work against except their own output. Give the agents the graph and the gate, and the loop changes. Decisions get faster and more accurate at the same time, because for the first time there is something independent to be accurate against. The first piece already ships: every known issue in the engagement dashboard carries a copy-ready prompt, context and reproducer included, that any coding agent can work from. That dashboard is live for our public audit: the jsonparser register.
That is the trajectory. The audit proves the discipline. The corpus compounds into infrastructure. The infrastructure becomes the missing evidence layer for engineering that increasingly runs itself, with humans setting intent and signing what matters. The practice is the first act of that company, not the whole of it.
Two places to go from here.
See what the instruments produced →
Have them pointed at your component →