Most industrial proofs are bounded: the design is too large for induction to close, and the sign-off rests on a bound that must be defended. This topic turns that defence into paperwork that holds: a bound derived from reset, trigger length and worst-case latency; a ledger where every row carries its status, justification and source hash; a waiver process with teeth; and a staleness check that reruns everything on every change. The decade counter and the arbiter carry the numbers.
Lesson | After it you can... |
|---|---|
Derive the minimum defensible bound and show a bug that needs all of it. | |
Keep a machine-checked ledger where inconclusive never counts as proven. | |
Handle an open proof with reduction, depth, backup or a waiver with real evidence. | |
Tie every result to a source revision and rerun on change. |
Suggested order: top to bottom. The bound first, because everything else quotes it; the ledger next, because it is where the bound is recorded; waivers next, because they are the escape hatch with rules; staleness last, because it guards the whole package over time.
Inconclusive for sign-off purposes. The bound is a number without an argument; until reset plus trigger plus latency or an equivalent argument covers 20, the row cannot support the release.