Methodology · Proof

01 / Preamble

Why “verified” needs a definition.

When paperwork can be generated faster than it can be read, the artifact stops being evidence, and the word “verified” carries no information unless whoever says it publishes what it means. Here is what we mean. A claim is verified when you can re-run it: the requirement it traces to, the check that enforces it, and the reproducer that pins the break, all executable by you, on your tree, without us in the room.

That is why every claim on this site is published with the route to its evidence attached. A requirement you cannot open, a check you cannot run, and a reproducer you cannot execute are three ways of saying the same thing: take our word for it.

Scope note: this is the bar we hold ourselves to, not a certification scheme. Nobody accredits it and nobody is asked to adopt it. It is published so you can hold us to it.

See a claim and its evidence → Open a live graph ↗ seeded showcase branch; read the labels first

02 / The clauses

Six clauses, each with the check that enforces it.

A clause without an enforcement mechanism is a preference. Each clause below names the machine check that fails when the clause is broken, and the external practice the clause is drawn from.

Clause 01 / 06The bar

1 · Requirements are proven before code is judged

clauseEvery requirement in scope is written in structured English with formal semantics, then proven realizable, consistent and non-vacuous before any code is judged against it. A spec that contradicts itself, or that a do-nothing system could satisfy, is a defect in its own right, and it is found first.

the checkRealizability, consistency and vacuity are discharged at spec time by two independent proof engines: the Kind2 model checker and the Z3 solver. A requirement that fails them never enters the audit.

the anchorNASA's FRET program, which gave structured English requirements machine-checkable semantics. In FRET's published research, a realizability check caught an eVTOL spec defect that permitted backwards flight, in 14 seconds.

Clause 02 / 06The bar

2 · No reproducer, no finding

clauseEvery finding ships with a runnable reproducer, run before delivery, with its result recorded, or it does not ship. A finding you cannot re-run is an opinion with formatting.

the checkThe reproducer is executed before delivery and its result recorded. A reproducer pins the finding one of two ways: it fails until the fix lands, or it asserts the broken behavior while that behavior is live and flips when the fix lands. The record says which. No recorded run, no ledger entry.

the anchorCoordinated-disclosure practice in security research: proof of concept before report, so the recipient can verify before they triage.

Clause 03 / 06The bar

3 · Traceability at 100% precision

clauseEvery requirement in scope carries links to the code that implements it and the test that verifies it. Every link that exists is machine-checked to resolve: precision, not recall.

the checkThe annotation resolver walks every link on every run; a link that fails to resolve fails the gate, and code answering to no requirement is flagged as orphan from the other direction.

the anchorBidirectional traceability, required by DO-178C in avionics and ISO 26262 in automotive, for the same reason it is required here: unlinked evidence cannot be audited.

Clause 04 / 06The bar

4 · MC/DC on the decision logic under audit

clauseThe decision logic under audit gets condition-level MC/DC (modified condition/decision coverage): every condition in every scoped decision is shown to independently affect the outcome, so a test suite cannot look thorough while exercising half the logic. Together with clause 3, this is coverage counted twice: once against the intent, once against the code.

the checkMC/DC instrumentation measures coverage on the scoped decisions. The number is measured, never estimated.

the anchorDO-178C Level A, the coverage bar avionics sets for software whose failure is catastrophic.

Clause 05 / 06The bar

5 · People sign the bar and the promises that require a person, and decide that a miss gets published

clauseMachines check everything, every time; a person validates every finding before it reaches you; findings derive their authority from a runnable reproducer, not from a signature. People sign the methodology bar, and every promise whose assurance level requires a person’s judgment. The level is declared on each requirement, and you set it; below the levels you reserve, an agent may approve its own requirement, and the record names the agent and the level. Publishing a miss is also a person’s decision, though the postmortem itself carries no signature.

the checkThe gate refuses to count a requirement without a recorded approval identity — a person’s name at the levels that demand one — and refuses to deliver a finding without its reproducer run and its result recorded. A person then validates the finding before it reaches you. There is no delivery path that skips any of the three.

the anchorThe oldest norm in professional practice: an audit opinion carries the engagement partner's name, an engineering drawing carries the stamp of the engineer who answers for it.

Clause 06 / 06The bar

6 · The gate re-runs, and runs without us

clauseThe audit gate re-runs on every change and runs without us. If the evidence could only be checked in our presence, it would be testimony, and this page promised you evidence.

the checkThe gate runs in your CI, on your infrastructure, with no network dependency on us and no license check. If we disappear, it keeps running.

the anchorThe reproducibility norm in experimental science: a result only the original lab can produce is not yet a result.

Where the bar applies · The six clauses were written for the engagement that installs Proof, which is where the bar is first applied. They bind the standing gate afterwards in exactly the same way. The instruments behind the checks are documented separately.

The engagement built on this bar → The instruments →

03 / The method

How the evidence gets made.

Six steps turn the clauses into artifacts. Each step leaves something you keep, in your repository, whether or not we are still involved.

Terminology · A promise is what the code owes its callers. Once it is approved at the assurance level you set — the critical ones by a person who owns the code — that promise is a requirement in the graph, and everything below is attached to it.

Step 01

Recover the promises.

We read the code and write down what it promises, one sentence each, in plain words.

You keep · the promises, written down, in your repo

Fig. 01 · Promises found in the code, written down.

Step 02

Your engineers sign them.

A promise counts when it is approved at the assurance level you set. The levels you reserve wait for a person who owns the code; below them an agent may approve, on the record.

You keep · approved promises, the approver recorded on each

Fig. 02 · Three signed. One agent draft waits for a person, because its level demands one.

Step 03

Write the worst case.

For each promise, what happens if it fails, and how bad.

You keep · a worst case for every promise

Fig. 03 · A worst case per promise. The bigger diamond hurts more.

Step 04

Turn it into obligations.

What must be true, and what test shows it.

You keep · obligations, each tied to a test

Fig. 04 · Under each promise, what must be true, and the test for it.

Step 05

Show the evidence.

Every obligation carries its evidence: the test that ran, and which conditions in the code it exercised.

You keep · the evidence, per condition, per commit

Fig. 05 · Each condition is shown to matter on its own, not just that the test passed.

The formal name for this measure is MC/DC, modified condition/decision coverage.

Step 06

Hold every commit to it.

The same checks run on every change. A broken promise blocks the merge.

You keep · the gate, in your CI

Fig. 06 · Four commits. Three pass. The broken one stops.

04 / Who decides

Who checks the checker.

Machines check everything, every time. People decide what a machine must not decide alone.

Swipe sideways to see the whole figure.

Fig. 07 · Above the line, machines run every check on every commit. Below it, people validate the finding and sign the promises that require a person.

Agents

Do the crunching: every check, every commit, at a volume no person could reach.

A person

Validates every finding before it reaches you, and signs the bar and the promises that require a person’s judgment.

Your engineers

Approve where the assurance level demands a person. Below that line an agent may approve its own requirement, and the record names the agent and the level. The level is yours to set.

The line between what a machine decides and what a person decides is written into the configuration, and you can move it.

05 / Agent policy

What an agent may do, and what it may not.

Drafting is machine-assisted, and nothing is trusted as drafted. What an agent may approve follows the assurance level you declare, per component and per requirement. That is the reason the word “approved” still means something in the graph: every approval records who or what approved, and at which level.

An agent may

Actions an agent takes without asking

read the graph: requirements, dependencies, hazards, known issues, reproducers, obligations
draft a candidate requirement, which stays marked as a draft
approve a requirement whose assurance level allows it — the record names the agent and the level
write a reproducer, and run it
propose a change with its evidence attached
rerun the obligations a change put in doubt
open a change record and fill it in

An agent may not

Actions reserved for a named person

approve above the line. A requirement whose assurance level demands a person waits for a person who owns the code
approve under any identity but its own
close a known issue
declare a defect class closed
mark evidence current without a code and graph version behind it
move the line between what a machine decides and what a person decides — the assurance level is that line

Requirements, reproducers and candidate findings are drafted with machine assistance, and deterministic checkers reject invalid work: requirements that fail realizability, reproducers whose recorded result is never checked, and links that do not resolve. What survives the checkers still does not lean on a signature. Findings derive their authority from a runnable reproducer, and people sign the bar and the promises that require a person’s judgment.

The enforcement is the same one clause 5 names: the gate refuses to count a requirement without a recorded approval identity. At the levels you reserve for a person, an agent identity does not clear that bar: the draft stays a draft, and the gate counts it as nothing. Below those levels an agent’s approval counts, and it is recorded as the agent’s, at that level — never as a person’s.

What the agent receives → Clause 5, and its check →

06 / Change evidence

What a change must carry.

Every change is a change record, whatever kind it is. A feature change and a defect fix are held to different evidence, and the record says which it is before it says anything else.

Kindfeaturerefactorbehavior changedefect fix

A feature change records

kind: feature

why the behavior changed
which component owns it
which requirements were introduced, changed, or affected
the implementation diff
documentation changes
blast radius
tests and other evidence
review and approval
final verification state

A defect fix records all of that, and

kind: defect fix

the originating known issue
the original reproducer
root cause
the evidence proving the individual instance is fixed
any evidence supporting closure of the wider defect class
sibling-defect analysis
permanent regression evidence
human or policy approval

A defect record is therefore an evidence-bearing change record with additional closure information. Nothing about a fix is a separate system; it is the same record with more required on it, because a fix makes a stronger claim than a feature does.

A change record is also worth more than a green pipeline for a reason that has nothing to do with fixes: a pipeline reports the checks that ran, and the record also names the ones that should have run and did not.

How change records are laid out → Where the record sits in the graph →

07 / Status

Stale is not invalidated.

Software knowledge becomes dangerous when it silently goes stale. Proof therefore separates a claim whose evidence stopped binding from a claim a check has contradicted. They are different states, and they ask you for different things.

Verified

The obligation ran and passed against a known code and graph version. The claim is current for that version and no other. what it asks of you · nothing

Evidence stale

The code, the requirement, or the document under the claim moved, so the evidence no longer binds to what is there now. Proof does not automatically declare the requirement false. It withdraws yesterday's confidence until the affected obligations are reviewed or rerun. what it asks of you · a rerun, or a review

Violated

A check ran against the current version and failed. This is the invalidated case: the claim is not withdrawn, it is contradicted, and there is a known issue with a reproducer that proves it. what it asks of you · a fix

Stale is a question. Violated is an answer.

How it is counted · A stale claim is never counted as verified and never counted as violated. It is counted as stale, and the change record carries the list of what must run, marked EVIDENCE REQUIRED, until somebody clears it.

Evidence invalidation, on a record → Watch a claim go stale →

08 / After a fix

The reproducer stays.

When a known issue is fixed, its reproducer stays in your suite and runs on every commit. That pins the instance: the release that would bring this one back turns the gate red instead. It is not the same as closing the class, and the record does not pretend it is.

Swipe sideways to see all ten releases.

Fig. 08 · One known issue, ten releases. Once its reproducer is in your suite, the release that would bring that instance back turns the gate red instead. The figure says nothing about the rest of the class; section 09 does.

KI-3 on buger/jsonparser is one. Set with an array-index path component under an object parent produced malformed JSON and returned it with a nil error. It is fixed, and its reproducer is retained in the suite.Read the record →

09 / Closure

Instance fixed versus class closed.

One passing reproducer can prove the known instance is gone. Closing the whole defect class takes broader evidence.

Rung 1

Reproducer passes

EstablishedIndividual instance fixed

Rung 2

Broader obligations pass
Sibling sweep
Hazard evidence
Blast-radius verification

Only thenDefect class closed

Until all four inputs are in, the record says the instance is fixed and says nothing about the class. Proof does not print DEFECT CLASS CLOSED because a test went green, and no page here will say a class cannot come back because one reproducer is retained.

Read against a real record, the two rungs come apart quickly. On KI-3 the instance is settled: the reproducer that produced malformed JSON now asserts valid output, and it runs on every commit. The class evidence is partial and the record says so. A malformed_input obligation was attached to the approved requirement, so the no-malformed-output invariant is enforced on every run from here. The symmetric case, an object key under an array parent, was checked and found already handled. A sweep of the rest of the mutation surface, and a blast-radius verification of the class, are not on the record.

So the honest reading of that record is: instance fixed, class evidence started, class not closed. That is what it says, and it is the shape most fixes are in.

The two rungs on a record → What the record must contain →

10 / Completeness

What a complete defect record contains.

A defect record is created when a known issue is fixed and the closure is verified. It is complete when every field below is present. A record missing a field is not a shorter record. It is an incomplete one, and the missing field is the part you would have had to take on trust.

Required field / what one public record carries DEFECT-260726-MFPA · buger/jsonparser

the originating issue

KI-3 · Set with an array-index path component under an object parent produces malformed JSON output

the original reproducer

set_spec_test.go:TestSetArrayIndexUnderObjectMalformedJSON_KI3

the fixing change

parser.go:Set · auto-coerce the container to the type the path expects, then insert

affected requirements and components

SYS-REQ-009 (strengthened) · SYS-REQ-110 (related) · component: parser, from the requirement (the defect record carries no component field of its own)

root cause

createInsertComponent emitted “,value” with no quoted object key, so the value was spliced into an object body where JSON requires a key

evidence the individual instance is fixed

TestSetAutoCoerce_KI3 · and the original reproducer, flipped to assert valid output

evidence toward closing the wider class

obligation class malformed_input attached to SYS-REQ-009, enforced on every run

sibling-defect analysis

the symmetric case, an object key under an array parent, checked and found already handled

permanent regression evidence

both tests retained in the suite

human or policy approval

reviewer human:buger · reviewed 26 July 2026

closure state on the record

covered_by_requirement · not “class closed”

Read the last row with section 09 · the record carries all ten required fields and still does not claim the class. Completeness is about what the record must say. Closure is about what the evidence has earned. They are different tests, and a record can pass the first and fail the second.

Read the whole record → Read the known issue → More resolved records →

11 / Declared limits

What this method does not see.

Assurance here is bounded on purpose: within a declared scope, for declared behaviors, with evidence commensurate with the consequence of failure. The table below is the edge of that boundary, by failure class.

Failure class	Coverage	Note
Logic and intent gaps	Covered	The core of the audit: behavior that violates an approved requirement, or a requirement the team never wrote down.
Boundary and error-path defects	Covered	Condition-level coverage forces the branches ordinary suites skip. Error paths are where most of these hide.
Concurrency interleavings	Partial	Modeled where declared, rarely exhaustive. The report states which interleavings were checked.
Performance under load	Not covered	We make no load, soak or latency claims. A correct system can still be a slow one.
Security-relevant behavior	Covered, in scope	Security promises inside scope are audited like any other requirement (white-box; attack classes named at scoping). Not a certified pen test: see the engagement exclusions and the row below.
Penetration testing and red-teaming	Not provided	We do not deliver a certified penetration test, black-box red-teaming, infrastructure testing, or social engineering. Where a compliance framework or customer review requires one, engage a security firm; our evidence complements theirs and substitutes for none of it.
Third-party dependency internals	Not covered	Dependencies are held to their declared contracts. We do not audit inside them unless that is scoped separately.

One more limit, and it is the largest · an approved requirement can be wrong. If the sentence a person signed is wrong, the gate will defend the wrong promise on every commit until somebody notices. That is why the requirements are published alongside the evidence, and why a reproducer you can run yourself is worth more than a status we report.

The same limits, in the words of the engagement → What we got wrong, in public →

12 / Hold us to it

Start with one component.

Pick the one you would least like to be asked about. The audit starts there, and the map and the gate are yours.

Request demo → Maintainer? Apply for an open-source audit →

Private early access: we take on a small number of engagements at a time. Private code stays private. We countersign your NDA before we read a line of your code.

Prefer a call? Ask for 20 minutes →

Leonid Bugaev
founder · this bar is published under his name, and the requirements are approved under it

What “verified” means here.