Research & instruments
The instruments that produce the evidence.
Proof compiles what the software must do, then checks it. Each instrument leaves an artifact you can rerun.
01 · The boundary
We build the instruments we audit with.
The platform holds the engine and the intent graph. The assurance practice runs the audits and checks what the engine reports. An audit compiles the requirements, runs the solvers, measures coverage, and refuses anything it cannot trace.
Proof connects approved requirements to hazards, code and verification obligations. Its checks produce inspectable results tied to the revision and conditions tested. The engineer assessing a change can see what passed, what failed and what remains unestablished.
Three evidence questions stay separate. MC/DC over a requirement formula asks whether its conditions independently affect the specified decision. MC/DC over code asks that question about implementation decisions. Executed acceptance checks ask whether the observed behavior meets the agreed criterion. None alone establishes that every important requirement or risk has been captured. See how these obligations fit into an engagement.
We plan to release the quality-engineering harness as open source, including local intent recovery, supported checks and readable evidence records. The dashboard and factory orchestration remain proprietary. The open release is planned, not yet released. Customer requirements, tests and evidence remain theirs. Read the ownership and access terms.
02 · The verification chain
Every link leaves an artifact.
The chain runs from the first written sentence to one exit code. Break a link and the gate refuses the change.
01 · Compiled requirements
Requirements are written in structured English. The sentences are tight enough for a machine to check their meaning. A template compiler descended from NASA’s FRET compiles them. FRET is the flight-software requirements language whose template semantics are formally specified. Structural ambiguity fails at compile time. A person still reads what the author meant.
artifact: each shall-line’s template ID, with its formal semantics attached
02 · The spec judged first
Kind2 and Z3 check the specification before any code is judged. Kind2 is a model checker. Z3 is a theorem prover. They check realizability, consistency, and vacuity. A specification that cannot be satisfied never reaches review. Neither does one a do-nothing system would already satisfy.
artifact: a solver verdict on the specification itself
03 · Solver proofs over encoded invariants
Z3 proofs run over encoded core invariants. Within the stated encoding and type domain, the solver establishes that no counterexample exists. Traceability ties that encoding back to the code. Behavior the encoding does not express stays outside the proof.
artifact: an UNSAT result on the negated property: the solver’s report that no counterexample exists
04 · Traceability
Every annotation that exists is machine-checked to resolve. A link that fails to resolve fails the gate. That is precision. Code that answers to no requirement is flagged as orphan. That is recall.
artifact: a requirement tag on the function, a Verifies: tag on its test
05 · The obligation catalog
Each obligation class names the evidence that proves it. Fuzz targets, mechanically generated hostile inputs, cover parsers that must not panic. Property-based tests cover algebraic laws. Race-detector runs cover concurrency. Negative tests cover malformed input. Solver lemmas cover invariants. Classes cite the frameworks auditors recognize, including OWASP ASVS, CWE, and NIST controls. Projects extend the catalog. Application-specific classes live in your repo, next to the requirements they guard.
artifact: a recorded decision on every class considered
06 · MC/DC at code level
Code-level MC/DC is modified condition/decision coverage. Every condition in every scoped decision has to be shown to matter on its own. Proof measures that on the scoped decisions and feeds it into the same gate for every language. This measurement has mostly lived inside certification suites built for embedded work. Ours runs in ordinary CI. The shapes it cannot measure are counted and reported, never silently dropped. How the measurement is obtained differs by language, and so does the public evidence. The table below states both.
artifact: a per-decision verdict, condition by condition
07 · The gate
The audit gate is one battery of machine checks, sized to the corpus it guards. It admits or rejects the whole chain. It runs in the client’s CI. It needs nothing from us.
artifact: one exit code, re-runnable by anyone with the repo
Where each language stands
How the condition-level measurement is obtained varies by language. So does whether a public corpus exists. Most rows have no public evidence yet.
| Language | How MC/DC is obtained | Public evidence |
|---|---|---|
| Go | Native MC/DC. Proof instruments the source in a staged workspace and runs go test. Statement coverage comes off the same run. |
jsonparser, the published depth. The dossier. |
| JavaScript TypeScript |
Native MC/DC. A Babel source transform adds a trace recorder. Tests run through node:test or Vitest. | None published yet. |
| Rust | Native MC/DC, with a prerequisite on one of the two paths. The default engine is a rustc driver reading MIR. It needs a driver binary built against a pinned nightly. We do not publish that binary. The instrument-in-place engine needs no compiler internals and runs on stock stable. | None published yet. |
| Java | Native MC/DC. Source instrumentation puts a recorder on the classpath. The run goes through Maven or Gradle. This is not JaCoCo, and not line coverage rebadged. | None published yet. |
| C# | Native MC/DC. Source instrumentation adds a generated recorder. The run goes through dotnet test. There is no coverlet dependency. |
None published yet. |
| PHP | Native MC/DC. Source instrumentation adds an injected recorder. The run goes through Composer and PHPUnit. | None published yet. |
| Zig | Native MC/DC. AST-guided source probes run through zig build test. |
None published yet. |
| Solidity | Native MC/DC. Contract instrumentation adds an injected runtime. The run goes through Foundry forge test. |
None published yet. |
| Python | Native measurement. Independence pairs are not certified yet. On CPython 3.12+ the runtime monitor records which conditions were exercised. It does not rewrite the source. Older interpreters import branch data from coverage.py, labelled as imported. Neither path reconstructs the independence witness today. The report carries condition-level signal and says which path it used. | None published yet. |
| C C++ |
Imported compiler coverage. There is no Proof instrumentation here. The gate ingests llvm-cov MC/DC summaries or gcov condition JSON that your build produced. That export has to exist. An uncovered condition arrives without its decision structure. It is reported as feasibility-unknown rather than counted against you. | rsync, 99 findings filed. The case study. |
| Kotlin Ruby Swift Svelte |
Parse-only. Annotations and trace links resolve. The traceability clause applies. There is no condition-level measurement, so the MC/DC clause does not. | Not applicable. |
| Everything else | Unsupported for coverage. A handful of languages are scanned for annotation comments only. Line-coverage import through Cobertura, LCOV, or Go profiles satisfies the coverage gate for any language. It never satisfies the MC/DC gate. | Not applicable. |
A native engine means the measurement exists and runs in ordinary CI. It does not mean we have published an audit in that language. Two rows carry public evidence today. Every other row says so in its own words.
03 · Change evidence
What the gate enforces about a change.
The methodology says every change carries its evidence. The engine enforces part of that clause today. A review can also carry a scenario, an API exchange, or a narrated demo. If that evidence is missing, it stays missing. The gate does not turn it into a pass.
Enforced on every run
A change record that names the requirements it affects must be cited back by each of those requirements, or the check fails. A closed record that moved no spec is caught there. A separate check watches wording. Edit a formalized requirement’s words while its formal semantics and its evidence stay untouched, and verification blocks until somebody reviews that delta.
Shipped, off until switched on
The check that reads a change’s declared kind and demands the evidence that kind requires is opt-in. The kinds are feature, refactor, and fix. It ships as change_evidence_complete, disabled by default. A project turns it on in its configuration. Our own repository has not turned it on. The check records skip in our audit, so the list above is the whole of what our gate enforces about a change today. Our public jsonparser corpus has turned it on: change_evidence_complete: enabled: true, on master, in a proof.yaml anyone can open.
What a record contains, and why a defect fix is held to more than a feature, is on the changes page. The clause is clause 8 on Methodology.
04 · Invalidation and re-verification
When the ground moves, the evidence stops counting.
This half is enforced. These checks run by default. They withdraw confidence that no longer matches what is in the repository now.
Approval fingerprints
An approval is recorded against a fingerprint of the requirement it approved. Edit the requirement and the approval stops counting until somebody approves the text that is there now.
Suspect links
A trace link whose code or test has moved under it is marked suspect. It stays suspect until a reviewer records that the link still holds and cites where.
Interface drift
An interface requirement is reviewed against a fingerprint of the code that implements it. Edit that code and the review is reported stale on the next run.
Calendar staleness
An approved requirement that has gone longer than the project’s review cadence is reported stale even when its fingerprint still matches. Nothing moved under it. Time passed.
Expired exemptions
A coverage exemption granted because of a known issue becomes an error once that issue is fixed. A waiver cannot outlive the bug that justified it.
Stale and violated are different states, and they ask you for different things. A stale claim asks for a rerun or a review. A violated claim asks for a fix, and it arrives with a reproducer that proves it. Methodology sets out the three states. The changes page shows one going stale on a record.
05 · The shapes
See the artifacts, not just the architecture.
Requirement, compiled
While in degraded mode, when queue_depth exceeds MAX_DEPTH,
the component shall, within 250 ms, satisfy reject_new_work.
template ID attached · 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
06 · Self-verification
The engine runs under its own gate.
Proof runs under its own gate. Just over two thousand requirements sit across four specification levels, from stakeholder intent down to integration contracts. Every production function is annotated. Orphan code is zero. The check runs on every change, the same way client work is checked.
Private / anonymized
Not publicly inspectable
Requirements
2,012 requirement files across the four levels, 1,584 of them approved.
Orphan code
13,619 of 13,619 production functions carry a requirement annotation that resolves.
What you can check
Neither figure. Both come off our own audit of 28 August 2026, on a repository we do not publish. The public reference below is the one you can re-run.
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. The vacuity checks in the chain above keep “green” from being gamed on a corpus that size.
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. Its requirements, defect records, and evidence are browsable file by file.
07 · Public instruments
Some instruments are public.
An OSS-Fuzz harness had run for years on jsonparser. It is Google’s continuous fuzzing service for open-source projects. It caught one real panic. A whole defect class still got past it, because the harness 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 public instrument is probe. It walks code and corpus together.
Semantic code search over large trees. Ripgrep speed, with tree-sitter structure. Engagements use it to walk code and corpus in one pass.
language: Rust
Structure-aware JSON fuzzer. A grammar-based generator, JSON-aware mutations, and correctness gates for differential testing of JSON parsers.
language: Go
Structure-aware GraphQL fuzzer. Grammar-based query, operation, and schema generators, with correctness gates for differential testing of GraphQL parsers.
language: Rust
08 · Research lineage
Where the semantics come from.
The requirement templates descend from NASA’s FRET program. FRET was built to state flight-software requirements precisely enough to check by machine. In FRET’s published research, a realizability check caught an eVTOL specification that permitted flying backwards. It took 14 seconds.
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 ships today is the enforcement half, a bar such proofs would have to clear.
09 · Limits
What the instruments cannot prove.
No instrument here establishes total correctness. A latency or throughput claim needs an agreed workload, operating conditions and measured results. Passing functional checks alone does not establish it. Each evidence plan must name the relevant obligations and the limits of its checks.
Unspecified behavior is invisible to every check in the chain. We paid to learn that limit in public. The two jsonparser escapes are the standing proof. What the instruments deliver is bounded on purpose. The bound is a declared scope, declared behaviors, and evidence commensurate with the consequence of failure. The longer table of what the audit cannot see is on the methodology page.
10 · Where this goes
One engineering model. Two ways to use it.
The software factory coordinates a change through clarification, implementation and verification. The continuous audit supplies assurance alongside development your team already runs. Choose who owns implementation; keep the same model of intent, risks, evidence and decisions.
The Software Intent Graph gives each new task the obligations and lessons retained from earlier work. Agents can retrieve that context through MCP. A later change must refresh any evidence whose basis changed. See the context an agent receives.
Start with a bounded component and an owner of intended behavior. Agree the deliverables and authority before work begins. Inspect a sample engagement or discuss which route fits your team.
11 · Onward