Sign-off by slide deck rots: a result copied from an old run, a bounded row quoted without its bound, a timeout counted as a pass. The ledger replaces prose with rows a script checks: one per property, with the status in the three-word vocabulary, the bound with its justification, the assumptions used, the covers its trigger needs, and the source hash. Inconclusive never counts as proven, and the script enforces that before any human reads the package.
Exactly three statuses exist: proven for the stated model and assumptions, counterexample with its trace, and inconclusive covering time-outs, depth limits and open inductions. A bounded result is an inconclusive row that also carries a bound and a justification; with both it is accepted as bounded evidence, without them it is an open row. Every row also names the assumptions active during the run, because a proof belongs to its assumption set as much as to its source revision, and every property with a trigger names the covers that show the trigger occurs.
The script below checks an eight-row ledger twice: once with a fault planted in every row but the first, once repaired. The faults are the ones that recur: a bounded row without a justification, a row marked proven on bounded evidence only, a trigger property with no cover, a cover that was not reached, an open counterexample, a row with no assumptions recorded, and a row whose source hash has moved on. Two more calls reject a status outside the three words and an inconclusive row with no bound at all. Each fault fails the gate with a message that names the row and the rule.
# the proof-status ledger gate: every row machine-checked
STATUSES = ("proven", "counterexample", "inconclusive")
def row(prop, status="proven", evidence="induction", bound=None, just=None, trigger=False,
covers=None, assumptions=("reset at step 0",), hash="a41f"):
r = {"prop": prop, "status": status, "evidence": evidence, "bound": bound, "just": just,
"trigger": trigger, "covers": covers or {}, "hash": hash}
if assumptions is not None:
r["assumptions"] = list(assumptions)
return r
def gate(rows, current):
faults = []
for r in rows:
p = r["prop"]
if r["status"] not in STATUSES:
faults.append(p + ": unknown status")
if r["status"] == "counterexample":
faults.append(p + ": open counterexample")
if r["status"] == "proven" and r["evidence"] != "induction":
faults.append(p + ": marked proven on bounded evidence")
if r["status"] == "inconclusive" and not (r["bound"] and r["just"]):
faults.append(p + ": bounded without justification" if r["bound"] else p + ": open, counts as not proven")
if "assumptions" not in r:
faults.append(p + ": assumptions not recorded")
if r["trigger"] and not r["covers"]:
faults.append(p + ": no antecedent cover")
for c, outcome in r["covers"].items():
if outcome != "reached":
faults.append(p + ": cover " + c + " not reached")
if r["hash"] != current:
faults.append(p + ": stale source hash")
return faults
bad = [row("a_range"),
row("a_data", "inconclusive", "bmc", bound=25),
row("a_wt1", evidence="bmc"),
row("a_push_inc", trigger=True),
row("a_valid_hold", trigger=True, covers={"c_stall": "not reached within 4"}),
row("a_ovf_ign", "counterexample", "cex"),
row("a_both", assumptions=None),
row("a_tc", hash="a41e")]
assert gate(bad, "a41f") == [
"a_data: bounded without justification", "a_wt1: marked proven on bounded evidence",
"a_push_inc: no antecedent cover", "a_valid_hold: cover c_stall not reached",
"a_ovf_ign: open counterexample", "a_both: assumptions not recorded", "a_tc: stale source hash"]
assert gate([row("a_x", "bounded")], "a41f") == ["a_x: unknown status"]
assert gate([row("a_open", "inconclusive", "timeout")], "a41f") == ["a_open: open, counts as not proven"]
ok = [row("a_range"),
row("a_data", "inconclusive", "bmc", bound=25, just="reset 1 + trigger 23 + latency 0 + 1 = 25"),
row("a_wt1"), row("a_push_inc", trigger=True, covers={"c_push_only": "reached"}),
row("a_valid_hold", trigger=True, covers={"c_stall": "reached"}),
row("a_ovf_ign"), row("a_both"), row("a_tc")]
assert gate(ok, "a41f") == []
print("PASS: gate names all seven planted faults, rejects bad statuses, ships the clean ledger")Read the gate's verdicts as policy: the unjustified bounded row is not evidence, the inconclusive row is not a pass, a cover that did not fire voids its property, and only the fully clean ledger ships. The bound 25 in the repaired row is illustrative, as is its justification string. The ledger lives in version control beside the sources and is rerun in regression, which the methodology lessons own.
One row per property, statuses drawn only from the three-word vocabulary, bounded rows carrying bound and justification.
Every inconclusive row is open, waived, or backed up, never silently counted; every trigger row names its covers.
The assumption set per row matches the run logs, and the hash column matches the current sources.
Treat the ledger as code: review diffs to it like design diffs. A row that flips from proven to inconclusive without a design change means the environment or the bound changed and needs its own justification. A row whose hash lags the sources is stale by definition and is rerun before any discussion of its content. The gate runs on every change; human review covers what the gate cannot, which is whether the justifications are true.
The run hit a limit it previously cleared: a time-out, a memory cap, or a slower machine. The result is honest and the row is open; investigate the convergence before rerunning, and never restore the old status by hand.