A proof is true of the RTL it ran on and of nothing else. Every edit after that run silently unproves it until it is rerun, and a signoff that cites a stale proof cites fiction. This topic puts formal into regression: a fast set that blocks bad commits, a full set that runs nightly, a ledger that records what changed, and a map from the course flow onto whatever tool the project uses.
Lesson | After it you can... |
|---|---|
Split per-commit and nightly sets and gate commits on a three-outcome ledger. | |
Tell a real bug from assumption drift, setup change, and new inconclusiveness. | |
Map tasks, parallelism, and results onto any tool and evaluate a flow honestly. |
Suggested order: top to bottom. The gate first, then the triage it feeds, then the tool map that generalises both.
Because the RTL changed around it: a proof belongs to the exact revision it ran on, and only a rerun on the current revision keeps the signoff honest.