A sign-off question in an interview or a release review always takes the same shape: what evidence would you require? The answer is a checklist, and each line names its evidence, not its aspiration. This lesson is that checklist, with every line pointing at the lesson that teaches the technique behind it, so no line can be waved through.
Seven lines, each with a pass criterion a script or a reviewer can verify. Every property proven, bounded with justification, or waived with evidence; all required covers reached with witnesses read; the assumption register reviewed with each assumption discharged; cone and mutation coverage reported; coverage numbers paired with their bounds; results tied to the final source hash; waivers reviewed with owners and expiries. A package missing any line is not a partial sign-off; it is not a sign-off.
Line | Evidence required | Taught in |
|---|---|---|
Every property proven, or bounded with justification, or waived with evidence. | Ledger rows with statuses and justification references; no inconclusive row unaccounted. | |
All required covers reached. | Cover witnesses read and recorded; missed covers inconclusive, never silent. | Antecedent Covers and Witness Traces, Bounded Cover Miss Is Inconclusive. |
Assumption register reviewed and each assumption discharged. | Influence table; every assumption an assertion elsewhere or a reviewed constraint. | Assumption Influence and Coverage, Over-Constraint Seen Through Covers. |
Cone and mutation coverage reported. | Union-of-cones with uncovered blocks owned; mutation score with survivors owned. | Proof Core and Cone Coverage, Mutation-Based Formal Coverage, Vacuity by Mutation and Sensitivity. |
Coverage numbers paired with bounds. | No coverage row without its bound and justification. | |
Results tied to the final source hash. | Hash gate passing on the release candidate. | |
Waivers reviewed with evidence, owners and expiries. | Waiver file with invariant or constraint references; expired waivers reopened. |
Each line resolves to a document or a script result, never to a verbal assurance.
The drill-down works: from any line to the run, the witness, or the proof behind it in one step.
The package fits the release candidate exactly: hash, file list and ledger agree.
Rehearse the defence before the review: pick any three lines and produce the evidence cold. If producing it takes more than minutes, the package is not assembled, only described. Common holes are covers nobody read, assumptions nobody discharged, and a ledger whose hashes lag the tree; the gate scripts in the linked lessons catch all three mechanically.
No. The proofs are conditional on undocumented terms, so their meaning is unknown. The register is not paperwork; it is part of the result.