Proof’s Software Assurance Method: Intent to Evidence

01 / Scope

A claim is only as strong as its scope.

Every claim names three things first. The scope it holds inside. The requirements it was judged against. The evidence you can run yourself. Drop one, and “verified” means nothing.

Paperwork that arrives faster than anyone can read it is not evidence. A claim is verified when you can rerun it. You rerun the requirement it traces to, the check that enforces it, and the reproducer that pins the break. You do that on your tree, without us in the room.

Scope is the load-bearing word. A verified claim holds for one declared component, at one code and graph version, against requirements a person approved. It says nothing about the next module, the next release, or a behavior nobody wrote down. Every status here carries the version it belongs to. Section 09 says what happens when that version moves.

Every claim is published with the route to its evidence. A requirement you cannot open is a request to take our word for it. So is a check you cannot run. So is a reproducer you cannot execute.

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

Last reviewed

30 August 2026

Why it is dated

This page states a bar and a set of technical limits. Both can change. When a clause or a limit moves, the date moves with it.

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

Terminology · A promise is what the code owes its callers. Once it is approved at the assurance level you set, that promise is a requirement in the graph. Every obligation, test, and finding below it is attached to that requirement.

How the evidence gets made

Six steps, from what the code owes to a gate that enforces it

Recover the promises. Read the code, write down what it owes its callers, one sentence each.
Get them approved. A promise counts once it is approved at the assurance level you set for it.
Write the worst case. For each promise: what happens if it fails, and how bad.
Derive the obligations. What must be true under the promise, and the test that shows it.
Measure the evidence. Which test ran, and which conditions in the code it exercised.
Hold every commit to it. The same checks run on every change. A broken promise blocks the merge.

What you keep

In your repository, whether or not we are still involved

the promises, written down
approved promises, the approver recorded on each
a worst case for every promise
obligations, each tied to a test
the evidence, per condition, per commit
the gate, in your CI

The same six steps, and the graph they build → The instruments that run them →

02 / The bar

The specification is checked before code is judged.

A clause with no check behind it is a preference. Sections 02 to 07 are the bar. Each names the machine check that fails when the clause breaks, and the practice it comes from.

Clause 01 / 06 The specification checked before code

clause Every requirement in scope is written in structured English with formal semantics. It is proven realizable, consistent, and non-vacuous before any code is judged against it. A spec that contradicts itself is a defect. A spec a do-nothing system could satisfy is a defect. Those defects are found first.

the check Realizability, consistency, and vacuity are checked at spec time. Two independent proof engines do the work: the Kind2 model checker and the Z3 solver. A requirement that fails them never enters the audit.

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

03 / The bar

No reproducer, no finding.

Clause 02 / 06A finding you can run

clause Every finding ships with a runnable reproducer. It is run before delivery, and the result is recorded, or the finding does not ship. A finding you cannot rerun is an opinion with formatting.

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

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

04 / The bar

Every claim traces to code and evidence.

Clause 03 / 06 Every declared trace link resolves

clause Every requirement in scope links to the code that implements it and the test that verifies it. Every declared trace link resolves. Orphan-code analysis checks the other direction.

the check The annotation resolver walks every link on every run. A link that fails to resolve fails the gate. Code that answers to no requirement is flagged as orphan.

the anchor Bidirectional traceability is required by DO-178C in avionics and by ISO 26262 in automotive. It is required here for the same reason. Unlinked evidence cannot be audited.

Fig. 01 · Under each approved promise, what must be true, and the test that shows it. Every one of those links is walked on every run.

05 / The bar

Critical decisions get condition-level coverage.

Clause 04 / 06MC/DC on the decision logic under audit

clause The decision logic under audit gets condition-level MC/DC (modified condition/decision coverage). Every condition in every scoped decision is shown to change the outcome on its own. A test suite cannot look thorough while it exercises half the logic. With clause 3, coverage is counted twice. Once against the intent. Once against the code.

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

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

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

06 / The bar

People decide what machines may not.

Machines and agents run every check on every commit. A person validates every finding before it reaches you. You never open a finding that nobody checked. People sign the promises that need a person’s judgment. They sign this bar. They decide which misses from public work get published.

Clause 05 / 06 Who signs, and who validates

clause Machines check everything, every time. A person validates every finding before it reaches you. A finding takes its authority from a runnable reproducer, not from a signature. People sign this bar. People sign every promise whose assurance level requires a person’s judgment. The level is declared on each requirement. You set it. Approval authority is configured, not assumed. Delegate lower-assurance work within a defined scope. Higher-assurance intent requires a person by default. Changes to delegation follow the previously approved policy. Every approval records who or what approved, and at which level. Publishing a miss from public Proof work is a person’s decision. The postmortem itself carries no signature.

the check The gate refuses a requirement with no recorded approval identity. At levels you reserve, that identity is a person’s name. At levels you leave open, it is the agent’s. The gate also refuses a finding with no recorded reproducer run. A person then validates the finding before it reaches you. No delivery path skips any of the three.

the anchor The 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.

Machines: your agent writes the code
The code: it enters the gate
People: your engineer signs the promise
The promise: it enters the gate
The gate: every check, every commit
Merge: the checks that pass go on
One fails: it drops below the line
A person decides here: and you can move it
Validates: a person validates it before it reaches you
Your dashboard: the reproducer. It pins the break.

Swipe sideways to see the whole figure.

Fig. 03 · Machines run every check on every commit. A person validates the finding and signs the promises that need a person.

Agents

Do the crunching. Every check, every commit, and the drafts under them.

A person

Validates every finding before it reaches you. Signs this bar and the promises that need a person’s judgment. Decides that a miss from public Proof work gets published.

Your engineers

Approve at the levels you reserve for a person. Proof reserves none by default. You name the ones you keep. Elsewhere an agent’s approval counts. The record names the agent and the level.

That line is the assurance level, declared per component and per requirement. It starts fully open. It is written into the configuration. Where it sits is your decision. That is why “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

draft a requirement, which lands marked as a draft
approve at any level your policy leaves open. That is every level, until you narrow it. The record names the agent and the level
write a reproducer, and run it
rerun the obligations a change put in doubt
propose a change with its evidence attached

An agent may not

Actions reserved for a named person

approve at a level you reserve. Narrow the policy, and a requirement at a reserved level 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 setting is agent_autonomous_for, under project.approval in proof.yaml. It moves in a commit you review

Drafting is machine-assisted. Recovered behavior is a candidate requirement, not automatically an approved promise. Review it against existing obligations and resolve material ambiguity with the appropriate owner. Agree approval authority before work starts. Delegate lower-assurance work to agents within a defined scope; reserve higher-assurance intent and consequential exceptions for a person. Changes to these boundaries follow the previously approved policy. A passing check supplies evidence. It does not grant permission to merge or deploy.

What the agent receives, and what it may touch → Where the names go →

07 / The bar

The gate reruns without us.

Clause 06 / 06 Evidence you can rerun yourself

clause The audit gate reruns on every change. It runs without us. If the evidence could only be checked in our presence, it would be testimony. This page promised you evidence.

the check The 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 anchor The reproducibility norm in experimental science: a result only the original lab can produce is not yet a result.

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

The requirements, the obligations, the reproducers, and the gate configuration are files in your repository. That is what makes the last clause enforceable. The evidence outlives the engagement that produced it. Anyone on your side can reproduce a claim without asking us.

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

The engagement built on this bar → The instruments →

08 / Change evidence

Every change carries its evidence.

Every change is a change record. The record names its kind first. A feature and a defect fix are held to different evidence.

Kindfeaturerefactorbehavior changedefect fix

A change record answers four questions. What am I accepting. What could it affect. Why should I believe it works. What remains unresolved. Belief can be a check, a scenario, an API exchange, a migration, or a narrated demo attached to the review. A green check is readiness. Acceptance is a separate decision.

A defect fix carries all of that, and more. It names the originating known issue, the original reproducer, and the root cause. It carries evidence that this instance is fixed, any evidence toward the wider class, a sibling-defect analysis, and a regression check that stays. A fix claims more than a feature does. Section 10 is the part of that claim most fixes have not earned.

A change record is worth more than a green pipeline. A pipeline reports the checks that ran. The record also names the ones that should have run and did not.

The complete record model, field by field → Where the record sits in the graph →

09 / Status

Stale is not violated.

Software knowledge goes bad when it goes stale in silence. Stale evidence means a check must run again. It does not mean the requirement is broken. A claim whose evidence stopped binding is not a claim a check has contradicted. 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. The evidence no longer binds to what is there now. Proof does not 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. The claim is not withdrawn. It is contradicted. 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. Two further outcomes sit beside these three. Not established means the evidence is missing, and it stays visible. Needs a decision means a person still has to accept the change. The evidence does not decide for them.

Evidence going stale, on a record → The four questions, on one review →

10 / Closure

One fixed instance is not a closed defect class.

A passing reproducer proves the known instance is gone. Closing the defect class takes broader evidence. The record says which of the two it has earned.

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. That is not closure of the class. The record does not pretend it is.

One known issue: seen in the first three releases
Its reproducer: no reproducer on those three
The reproducer stays: from the fourth release, it runs on every commit
Releases 4 to 10: that instance has not returned
Ten releases: the reproducer pins that instance. It does not close the class.

Swipe sideways to see all ten releases.

Fig. 05 · One known issue, ten releases. The reproducer pins that instance. It does not close the class.

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. Its reproducer stays in the suite. Read the record →

Rung 1

Reproducer passes

Established Individual instance fixed

Rung 2

Broader obligations pass
Sibling sweep
Hazard evidence
Blast-radius verification

Only then Defect class closed

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

What one public record carries / on the class question 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

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 · obligation attached to SYS-REQ-009 · the class is not declared closed

Read the last row against the two rungs. The record carries every field a complete defect record requires. It still does not claim the class. Completeness is what the record must say. Closure is what the evidence has earned. A record can pass the first and fail the second.

How it is counted · A known issue is not a defect record. Proof never mixes unresolved issues and verified defect records into one number, because the two say opposite things about the software.

Read against that record, the two rungs come apart. 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. The malformed_input obligation enforces the no-malformed-output invariant from here on. A sweep of the rest of the mutation surface is absent. A blast-radius verification of the class is absent. The honest reading is this. The instance is fixed. Class evidence has started. The class is not closed. That is the shape most fixes are in.

The two rungs on a record → Read the whole record ↗ More resolved records →

11 / Declared limits

The limits are part of the claim.

Assurance here is bounded on purpose. It holds inside a declared scope, for declared behaviors, with evidence matched to the consequence of failure. The table is the edge of that boundary, by failure class. It is published with the claims it bounds.

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. The work is white-box, and attack classes are named at scoping. This is 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 a customer review requires one, engage a security firm. Our evidence complements theirs. It 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 with the evidence. A reproducer you can run is worth more than a status we report.

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

12 / Accountability

Hold us to it.

Names go on three things. The promises whose assurance level requires a person’s judgment. This bar. The misses we publish from public work. A person validates each finding before it reaches you. You never open a finding that nobody checked. The finding takes its authority from a reproducer you can run.

A person decides that a miss gets published in public Proof work. Private engagement evidence stays private unless the customer authorizes disclosure. The postmortem carries no personal signature, so this page claims none. It does name the layer that should have caught each escape, and the blind spot that let it through. That is the part you can check against the code.

Our misses are published

On buger/jsonparser, two defects escaped the strict proof posture on that project. Set on an array index beyond the array's length overwrote the array instead of appending to it. A second empty-key panic site survived a hazard sweep that had reported all of them. The root-cause analysis is public and blameless. For each escape, it names the layer that should have caught it and the blind spot that let it through.

Filed as a blameless postmortem, dated 26 July 2026, attributed in the document to proof-gap review. It carries no case number and no personal signature. This page claims neither.

Read the root-cause analysis →

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

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

We scope a first use of Proof in your existing repo and agent workflow. 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. The requirements are approved under it.

How Proof verifies software changes.