Proof · Engineering practice
AI writes the specs and code. Who verifies the intent?
Intent needs an accountable authority: the person or policy entitled to decide what the software must do. An agent can recover and propose requirements, and may approve within explicit delegation. Neither a plausible specification nor passing tests alone authorizes a new product promise.
Separate observed behavior from the intended promise
Consider a policy service whose code assumes its store is available. A generated specification that repeats that assumption can omit the entire unavailable-store case. The useful question is whether callers are promised an error, retry or some other result when the dependency is absent.
| Record | Meaning |
|---|---|
| Observation | The implementation dereferences the store without handling absence. |
| Candidate intent | If the store is unavailable, return a defined error without changing session state. |
| Conflict | Existing retry or availability guarantees may require a different response. |
| Authorized resolution | The responsible owner or delegated policy approves the applicable behavior and revision. |
| Verification | A test actually creates the failure condition and checks the error and unchanged state. |
This is an illustrative reasoning sequence. For an inspectable public case of missing modeled behavior, read the jsonparser gap postmortem. It shows why a successful measurement can leave an unmodeled obligation unanswered.
Recover candidates and reconcile them with existing intent
Start with contracts, product decisions, documentation, tests, code and earlier incidents. Preserve each source and distinguish promises from observations. A newer ticket may request a change; it does not silently retire an earlier obligation.
Ask for a decision only when ambiguity, conflict or a consequential amendment requires it. Within an already approved scope, an agent can investigate, implement and test without asking someone to rewrite every clause. An implementation agent cannot gain authority by changing the policy it is being evaluated under.
Review and verification can be agent-assisted. Inspect the assertion’s oracle and the executed result rather than using human authorship as a proxy for correctness.
Approval follows the saved project policy
Inspect project.approval in proof.yaml. Current initialization writes agent_autonomous_for.all: true at every assurance level. This permits agent approval broadly; it is not the recommended higher-assurance default and does not establish independent verification or release authority.
The supported general-development recommendation is human approval at A/B and agent approval permitted at C–E, with other delegation explicit. Apply these fields within the existing configuration, retaining role and comment requirements:
project:
approval:
required_for:
assurance_levels: [A, B]
agent_autonomous_for:
all: false
assurance_levels: [C, D, E]
Read proof help assurance-level for the policy example and applicability details. Requirement approval uses the saved requirement level; do not assume a component classification propagates automatically. Regulated work must also follow its applicable assurance plan, including required human signoffs and independence.
Approve the requirement, then establish its implementation
proof audit --check acceptance_criteria_witnessed
proof audit --check tests_pass
The witness check examines acceptance-evidence structure. The test check runs configured commands. Neither command decides what the product ought to promise. Retain the approved requirement revision, supporting executions and any remaining uncertainty, then make acceptance under the applicable policy.
For the developer workflow, see verifying agent-written code. For the persistent requirement model, see the Software Intent Graph.