Agents
Code is not enough context.
Proof gives coding agents the requirements, dependencies, hazards, historical defects, reproducers, and verification obligations surrounding every change.
01 · Read
Navigate through intent
A code graph tells you what calls what. Proof tells you what depends on what being true.
An agent that reads only the repository has to infer the promise from the implementation. It guesses, and the guess never appears in the diff.
In Proof the agent opens the component, reads what the component promises, and walks the intent above and below it. Three questions are answered before it writes a line: what does this component promise, why does this behavior exist, and what depends on it.
02 · Reach
Understand blast radius before editing
The agent asks what a change can reach, and gets an answer before the first edit, not after review.
The answer is not a file list. It is the intent the change touches, the code and tests bound to that intent, the hazards that constrain it, and what already went wrong in the same place.
An edit that looks local but breaks a parent requirement is visible at the start of the work. That is the difference between a review that catches it and a release that ships it.
Returned to the agent
Relevant intent
SYS-REQ-009 · SYS-REQ-069 · SYS-REQ-110
Blast radius
1 component · 5 files · 13 tests · 3 hazard obligations
History
1 related defect record · 2 known issue classes
03 · Evidence
Start from executable evidence
A Proof finding arrives with a reproducer, so the agent can observe the failure before it touches the implementation.
A bug report describes a symptom. A reproducer is a test that pins the broken behavior: it either fails until the fix lands, or asserts the break while it is live and flips at the fix. The agent begins from the failing test, so the first thing it learns is what the software does, not what somebody remembered.
The finding also names what closing it requires. The agent does not have to invent a completion test, and it cannot quietly choose an easier one.
- Violated requirement
- SYS-REQ-009
- Reproducer
- a test that pins the break, in your repository
- Observed
- unrelated structure is corrupted
- Required to close
- the reproducer passes, and the obligations on the requirement run again
Give the agent the evidence, not the bug report.
04 · Change
Create evidence-backed changes
Every feature and every fix leaves behind an evidence-backed change record.
The agent does not close its work by writing a summary. It closes it by producing what the requirement asked for: the tests, the properties, the documentation update, and the review the change needed. All of it stays attached to the intent that moved.
When a known issue is fixed and the closure is verified, Proof creates a verified defect record that preserves the fix and its evidence. A passing reproducer establishes that the known instance is gone. Closing the wider class needs the broader obligations, the sibling sweep, and the hazard evidence as well.
- Kind
- feature
- Intent
- Support nested array updates.
- Requirements
- 2 added, 3 affected
- Evidence
- 8 tests, 2 properties, hazard review
- Approved by
- a named maintainer
05 · Re-proof
Know what must be re-proven
The graph does not silently preserve yesterday's confidence. It knows what needs to be proven again.
When the agent changes code, Proof identifies the relationships and the evidence that may no longer be current. It does not declare the requirement false. It withdraws yesterday's confidence until the affected obligations are reviewed or run again.
So the agent is told what its own change invalidated. Done means those obligations ran again, not that the tests which already existed still pass.
06 · The boundary
Human approval stays explicit
An agent can propose a requirement. It cannot approve one.
Everything an agent writes carries a draft mark. Normative intent, the statement of what the software must do, becomes approved only when a named person approves it, and the name is recorded with the approval. Machine output is never counted as approved intent.
This is not a setting the agent can talk its way past. It is the reason the graph is worth reading in the first place: an agent that could approve its own requirement would be grading its own work, and every answer downstream would inherit the grade.
An agent may
- propose a requirement, as a draft
- attach evidence to an obligation
- run the obligations again
- open a known issue
Only a person may
- approve intent
- sign the promises and the bar
- decide that a miss gets published at all
07 · Your agent
Use the agent you already have
Proof does not ship a coding agent, and it does not ask your team to replace the one it already uses.
The agent connects to the graph of your repository and keeps its own workflow, its own prompts, and its own habits. Nothing in the model belongs to a particular agent, and nothing in your repository has to be rewritten to suit one.
claude codecursoryour own tooling
Illustrative. Proof does not require a particular agent.
Bring any coding agent.Proof gives it the accumulated understanding of the software.
08 · Architecture
MCP architecture and permissions
This is the delivery mechanism, not the product. Proof serves the graph to your agent through an MCP server that runs against your repository. What follows is the surface we are building toward, not a published API. The shipped server today exposes a different tool set, and on the write side a broader one than this list: it can update and delete requirement files. Our roadmap schedules the MCP surface for removal (MCP-4), and our approved requirements cite that track when they decline to add new obligations to it — how agents reach the graph is likely to change. We describe the shape here because the shape is the commitment; the tool names are not.
The seven sections above describe what the agent receives. This one describes how it arrives: a read surface that is wide, an action surface that is narrow and logged, and one boundary that is neither.
Read surface
the graph, at a stated version
- components
- requirements and their dependencies
- hazards
- obligations
- evidence, and its freshness
- known issues and reproducers
- change records and defect records
- blast radius for a proposed change
Action surface
narrower, and written to the log
- propose a requirement, as a draft
- attach evidence to an obligation
- run the obligations again
- open a known issue
Approval of intent is not on this list. It stays with a named person.
- Graph version
- Every read is answered against a stated version of the graph, so two answers taken at different moments can be told apart.
- Evidence freshness
- Evidence is never returned as current on its own. It is returned bound to the code version and the graph version it was produced against, and it carries its state: verified, or stale and waiting for a rerun.
- Audit log
- Every action an agent takes is recorded with the actor that took it. The log lives in your repository, next to the evidence, and it is readable without us.
- Approval boundary
- Approval is not an action an agent can take. Proof marks agent-written intent as a draft, and only a named person moves it to approved.
The tool names and the exact permission scopes are settled when Proof is installed on a repository, because they follow the shape of that repository. This page describes the shape of the interface: what can be read, what can be written, and what stays with a person.
See it run against a real repository.
One component, one change, and the answer the agent gets back before it edits anything.