proof-verify

Proof Verify

Plan-based verification: freeze acceptance criteria BEFORE building, verify AFTER with independent agents.

When to Use

• After completing a feature/fix that was built from a plan
• When you need independent confirmation that work meets spec
• When the builder should NOT verify their own work
• Trigger phrases: "verify against plan", "check the implementation", "proof check", "independent review"

The Pattern

PHASE 1: PLAN (before any code)
  Create .proof/PLAN.md with numbered acceptance criteria
  Each AC: testable, specific, has a verification command or check
  Plan is FROZEN - no changes during build

PHASE 2: BUILD (normal work)
  Implement against the plan
  Mark progress in .proof/PROGRESS.md
  Builder does NOT self-verify

PHASE 3: VERIFY (after build, independent agent)
  Fresh agent reads PLAN.md (never saw the build process)
  Walks through each AC, runs verification commands
  Writes .proof/VERDICT.md with PASS/FAIL per criterion
  If any FAIL → .proof/PROBLEMS.md with specific fixes

PHASE 4: FIX (if needed)
  Builder reads PROBLEMS.md, makes minimal fixes
  Back to PHASE 3 (re-verify)
  Loop until all PASS

Stage Ledger - only when proof feeds another stage

For a release, integration, migration, hardware, signer, or other multi-stage task, a green check is not enough. The next stage needs a stable input, not a summary that the previous stage once looked good.

1. Freeze the stage contract and its scope before building it.
2. Run the focused proof and obtain the fresh verdict as usual.
3. Write the stage to .proof/stage-ledger.json as VERIFIED or SEALED. A sealed stage records its source commit/tree, contract digest, named input and output digests, fresh verdict digest, and invalidation keys.
4. A downstream stage names the sealed parent and exact output digest it consumes. It must not consume a merely VERIFIED or BLOCKED stage.
5. If an external dependency is missing, record BLOCKED with the exact missing prerequisite. Do not invalidate the sealed upstream code.
6. If code, contract, or an input digest changes, add a SUPERSEDED successor and re-run proof for that successor; do not overwrite the old receipt.