Skip to main content
A claim proven once stays proven until something it depends on changes. Re-proving is triggered by the diff, not by a schedule and not by a release boundary. Anything else asks a human to re-witness transcription quality because a login page moved, which is how a validation loop stops being run.

The mechanism

Three pieces, and the third is a set intersection.
  1. Every value declares a surface — the set of images, and config keys, whose bytes can affect the claim. It is part of the value, declared once, beside the claim itself.
  2. Every piece of evidence records the exact digests of that surface as they were when it ran. Not the release, not the date — the digests.
  3. At the next entry, the gate computes changed_digests ∩ surface:
Digest equality is the right to reuse. No prose justification, no reviewer judgment, nothing anyone can argue with: evidence binds to digests, and an unchanged digest is the same bytes, so the claim is still literally true of them. A reuse that needs an argument is not a reuse — it is a new claim.

What re-proves, per dimension

That last row is the one that makes the model affordable. The human judgments are attached to a pull request, and a pull request does not change.

Two guards

Surfaces are declared conservatively. A value about a seam — an integration, a protocol boundary, anything whose failure mode is interaction — claims more images than a localized one. Over-claiming costs an occasional unnecessary re-prove. Under-claiming silently ships an unproven claim wearing a green tick, so the asymmetry decides the default. Statistical rows keep watching regardless. Soak evidence is a rate over a live window, so it goes on measuring in production no matter what the diff said. That is the net under the surface declarations: an interaction nobody declared shows up as the rate moving, not as silence.

Worked example

An update ships a gateway auth change.
  • The diff touches the gateway image only. Transcription image digests are byte-identical to the previous entry.
  • The human witness on “transcription quality is acceptable” declares a surface of the transcription images. The intersection is empty.
  • The row inherits: inherited from seq 6 — surface digests unchanged. Nobody is asked to listen to audio because an auth header changed.
The next update bumps whisperlive.
  • That digest is in the transcription value’s surface. The intersection is non-empty.
  • The row drops to unproven and a witness session is queued. The diff summoned the human — not a calendar, not a release manager, and not the human’s own memory of when they last checked.
State: RULED, NOT BUILT. The surface field on a value and the intersection check at the gate are decided and unimplemented. Evidence today attaches to the entry that produced it and is not inherited; the digests it would intersect against are already recorded in the candidate map. See the evidence model for the full per-element state.
Next: How channel contracts compose · The station gate