Requirements that test themselves.

Intent → Evidence → Verified

The moving graph behind this headline is drawn from the public jsonparser project. It centres on the requirement SYS-REQ-009. Around it are the requirements that requirement rests on, the source files and test files that implement and verify it, the change that touched it, and the known issue and defect record that strengthened it. Every identifier in the graph is real and can be checked in the repository. The same requirement is set out in full in the next section.

Proof builds a living graph of what your software must do, what depends on it, and what proves it. The same graph guides your engineers and coding agents.

Watch Proof work Explore public proof Explore public proof →

On real software

We audit the software everyone depends on.

The catalogues are public, the findings carry reproducers, and the misses are published beside the wins.

rsync

Thirty years old, on virtually every Linux system. Audited continuously through the development of the 3.5.0 security release — and still running.

99 findings filed by the audit · 10 of them in the code since the first release in 1996 · the 3.5.0 security release shipped 33 fixes, from this audit, a fuzzing pass, and external researchers together

Read the rsync audit →

On rsync we worked alongside Trail of Bits, through its Patch the Planet program.

We have run Proof on more of the software everyone depends on — jsonparser, google/grpc-go, graphql-hive/router and wundergraph/graphql-go-tools. See what we found and fixed → the public roster.

One living requirement

Live from the jsonparser audit

A requirement is not documentation anymore.

In Proof a requirement is an object in the system, not a paragraph in a document. It names its component, the intent it rests on, the code that implements it, the tests that verify it, the obligations it still owes, and the defects that changed it.

Open live requirement in the portal ↗

SYS-REQ-009

Approved

When Set is called with a provided path, the parser shall either replace the existing addressed value, create a type-consistent missing path and return the updated JSON document, or return KeyPathNotFoundError when the requested mutation path is not usable for the provided input.

Component: parser
Rests on: STK-REQ-005 Review not approved yet: a candidate, and nothing is judged against it
Implemented by: 4 source files
Verified by: 12 test files
Obligations: 4
Defect history: 3 records name it, latest DEFECT-260727-WWWY

OBLIGATIONS — the specific checks this requirement must keep passing to stay approved.

Two graphs

A code graph tells you what calls what.Proof tells you what depends on what being true.

Select a component, requirement, issue, or change. Proof shows the intent it rests on, the promises downstream, and the code, tests, documents, and contracts that may need to be reconsidered.

Code graph

3 nodes · one kind of edge

Proof

6 nodes · five kinds of edge

Fig. 01 · Example service · The same system, seen two ways. Colour carries state: green is verified knowledge, the hazard branch marks how the requirement could fail, and grey is structure with nothing proving it.

See the blast radius before you touch the code.

Change this. What else did you change?

Select a requirementfour of them are live in this figure

If this changesPAY-042PAY-18PAY-61PAY-94

5 files · 13 tests · 1 parent requirement · related obligations

2 files · 5 tests · 1 parent requirement · related obligations

1 file · 3 tests · 1 parent requirement · related obligations

2 files · 5 tests · 1 parent requirement · related obligations

Fig. 02 · Example service · One requirement, walked out to everything that rests on it. The PAY-* service is invented, and so are its counts.

Explore the live graph ↗See the graph model → seeded showcase branch; read the labels first

Change and defect lineage

Every change should explain itself.

A commit says what text moved. A Proof change record says why the behavior moved, what it touched, and which evidence made the result acceptable.

Change recordfeaturerefactorbehavior changedefect fix

Fig. 03 · Four kinds of change record. Two are shown below — a routine feature, and the real defect fix the evidence section walks end to end.

CHANGE-1042

Verified

KINDfeature

INTENT

Support nested array updates.

COMPONENTS

parser

REQUIREMENTS

2 added · 3 affected

requirements this change added or touched

IMPLEMENTATION

4 files

DOCUMENTATION

1 document updated

EVIDENCE

8 tests · 2 properties · hazard review

the checks that had to pass before approval

APPROVED BY

maintainer

DEFECT-260726-MFPA

Covered by requirement

KINDdefect fix

ORIGIN

Known issue KI-3

the known issue that opened this record

VIOLATED INTENT

SYS-REQ-009

the promise this defect broke

REPRODUCER

pins the break on the affected revision

FIX

parser.go

INSTANCE

fixed

DEFECT CLASS

evidence attached / status explicit

the class stays open until sibling evidence lands

REGRESSION

permanent test retained

Open problems remain known issues. When the fix is verified, Proof creates a defect record using the same evidence-bearing model as any other change. The issue closes; the proof stays.

See a change move through Proof →

Self-invalidation

The graph knows when it needs to be proven again.

Software knowledge becomes dangerous when it silently goes stale. When code, a requirement, or documentation changes, Proof identifies the relationships and evidence that may no longer be current.

It does not automatically declare the requirement false. It withdraws yesterday’s confidence until the affected obligations are reviewed or rerun.

Change recordCHANGE-1042

EVIDENCE REQUIRED

VERIFIED

Fig. 04 · One requirement and the three things attached to it, before the change, at the moment the change lands, and after verification runs. The record stays open until the affected obligations are reviewed or rerun.

Proof does not just remember what was true.It knows what must be checked again.

Agents

Give your agents the same understanding.

Your agent shouldn’t have to rediscover your system every time. Coding agents query the intent graph directly — the same components, requirements, dependencies, hazards, issues, changes, reproducers, and verification obligations that your engineers see.

Code tells an agent what the system does.Proof tells it what the system must not stop doing.

The connection

agent session proof · jsonparser

~/src/jsonparser

I need to change Set() for nested arrays.

What can this affect?

Proof

RELEVANT INTENT

SYS-REQ-009 · SYS-REQ-069 · SYS-REQ-110

BLAST RADIUS

1 component · 3 files · 8 tests · 3 hazard obligations

HISTORY

1 related defect record · 2 known issue classes

REQUIRED BEFORE COMPLETION

reproducer
boundary obligation
nested-mutation property
documentation review

answered from the intent graph

Fig. 05 · The answer is not a file list. It is the intent the change touches, what the change can reach, what already went wrong here, and the evidence the change has to produce before it can be called done. The requirement identifiers are real and published.

A normal issue hands the agent one reported sentence, and the work starts with archaeology: reproduce the problem, infer the intent, find the code, guess the blast radius. A Proof issue arrives with the violated requirement, the reproducer that pins the failure, the blast radius, and the evidence required to close it — no reproducer, no finding.

The agent begins at the fix loop,not at the archaeology loop.

Point your agent at the live jsonparser graph — over MCP →

Compounding knowledge

Every change makes the next change safer.

Features, fixes, incidents, misses, reproducers, approvals, and evidence stay attached to the intent they changed — so the next engineer, or the next agent, starts with the accumulated model instead of reconstructing it from raw code.

Fig. 06 · One lap. One line open beside the first step, seven beside the last; the band carries all of it back to the start.

Public proof

We ran it on real software.

Public project

github.com/RsyncProject/rsync

rsync — thirty years old, shipping on virtually every Linux and Unix system on earth — audited continuously through its 3.5.0 security release. The review filed 99 findings; the release shipped 33 security fixes, most of them credited to Leonid Bugaev by name in the release notes. The audit is still running.

Every fix shipped upstream — with a CVE ID and a regression test.

findings filed by the audit

security fixes in rsync 3.5.0

CVE IDs across the release cycle

Each fix carries a test that fails on the unfixed code.

Not an opinion, not a warning, not a suggestion.

We publish what we withdrew, and what we don't take credit for, next to what we found. That is the only way you can check us.

Don't take our word for it.

Read the rsync audit → Read the release notes ↗ Open the rsync project ↗

Want this on your own code? Request demo →

How Proof knows

“Verified” should mean something you can rerun.

The Proof CLI checks the requirement before it judges the code, connects the claim to implementation and evidence, analyzes how it can fail, and leaves the resulting checks in your CI.

01

APPROVE THE INTENT

Engineers sign what the component must do.
02

ANALYZE THE OBLIGATIONS

Formal semantics and hazard analysis define what evidence is needed.
03

BIND THE EVIDENCE

Code, documentation, tests, proofs, reproducers, and coverage attach to the claim.
04

RE-EARN THE RESULT

Changes invalidate affected evidence and the gate runs again.

Instruments

FRETish · Kind2 · Z3 · hazard analysis · MC/DC

FRETish spec language · Kind2 + Z3 model checkers

property tests · fuzzing · executable reproducers · CI gate

The whole method →

Accountability

Who checks the checker.

Machines check everything, every time. People decide what a machine must not decide alone. This limit is written in the configuration. You can move it.

Agents

Run every check, on every commit. The quantity is more than a person can read.

A person

One person validates each finding before it reaches you. People sign the bar and the promises that require a person’s judgment, and decide that a miss gets published. The published postmortem carries no personal signature, and we say so where we publish it.

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.

Fig. 07 · CI is green in the two pictures. The second picture is possible only after the promises are written down.

Our misses go on the same public register as the findings, with the proof gap named and the reproducer attached. Read the register →

Installation

Install Proof on one consequential component.

The Continuous Correctness Audit builds the first intent graph inside your software. We recover and formalize the requirements, your engineers approve them, and Proof binds the component to its hazards, code, documentation, issues, changes, and evidence. Scoping is confidential.

Continuous Correctness Audit

The installation

Scope

ONE COMPONENT

roughly four weeks
fixed fee after scoping

What you keep

approved requirements
intent graph
hazard analysis
executable findings
change and defect evidence
agent access
CI gate

You finish with the graph, the evidence corpus, and a gate in your CI. Everything that runs stays yours.

The audit is how Proof gets installed. Proof is what stays.

See the full engagement →

What you get is a file tree in your repository, not a PDF in your inbox.

Prove your software does what you promised.

What requirements are hiding in your codebase?

We run Proof on one public project each quarter, at our own cost. There is no invoice and no follow-up.

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

Leonid Bugaev · founder
sets the bar these promises are judged against, and publishes the misses on the same register

Requirements that test themselves.

We audit the software everyone depends on.

A requirement is not documentation anymore.

A code graph tells you what calls what.Proof tells you what depends on what being true.

See the blast radius before you touch the code.

Every change should explain itself.

The graph knows when it needs to be proven again.

Give your agents the same understanding.

Every change makes the next change safer.

We ran it on real software.

“Verified” should mean something you can rerun.

APPROVE THE INTENT

ANALYZE THE OBLIGATIONS

BIND THE EVIDENCE

RE-EARN THE RESULT

Who checks the checker.

Agents

A person

Your engineers

Install Proof on one consequential component.

Continuous Correctness Audit

Prove your software does what you promised.