Why it matters

A team ran full proofs per commit, each taking hours, and within a month engineers stopped waiting and stopped committing cleanly. Another team ran nothing per commit and found every breakage at release. Both failed the same way: the wrong set at the wrong cadence. The per-commit set must finish in minutes; the nightly set may take hours; both must report the same three outcomes.

Job of this lesson: split the two sets, describe the job that runs them, and build the gate between its ledger and the commit.

The core idea

The per-commit set holds small bounded checks and every required cover: it answers whether the obvious still holds, fast. The nightly set holds the full proofs to their planned depths: it answers whether everything still holds, thoroughly. Both are one CI job, described in generic terms by four things: the tasks it runs, how they run in parallel, where the ledger lands, and what fails the build. A timeout is inconclusive, never a pass, and a newly inconclusive proof blocks the build like a failure until it is triaged:

Worked example: the gate

The script below implements the gate exactly as specified. A property row ends proven, counterexample or inconclusive. A cover row ends reached, or inconclusive when it was not reached within its depth; it is never called unreachable without an engine proof of that. The gate fails on any counterexample, any required cover not reached, any proof that was proven before and is inconclusive now, any row that ran on another RTL revision, and any status outside the allowed ones. The clean ledger goes through; the failing ledger, with one counterexample, one cover not reached and one newly inconclusive proof, is rejected on all three counts, and each of the other rules is tested on its own:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45

OUTCOMES = ("proven", "counterexample", "inconclusive")
COVER_OUTCOMES = ("reached", "inconclusive")

def gate(run, previous, revision):
    prev = {p["name"]: p["status"] for p in previous}
    failures = []
    for p in run:
        allowed = COVER_OUTCOMES if p["kind"] == "cover" else OUTCOMES
        if p["status"] not in allowed:
            failures.append(p["name"] + ": unknown status " + p["status"])
        elif p["status"] == "counterexample":
            failures.append(p["name"] + ": counterexample")
        elif p["kind"] == "cover" and p["status"] != "reached":
            failures.append(p["name"] + ": required cover not reached within its depth")
        elif p["status"] == "inconclusive" and prev.get(p["name"]) == "proven":
            failures.append(p["name"] + ": newly inconclusive")
        if p["rtl"] != revision:
            failures.append(p["name"] + ": row from another revision")
    return failures

def row(name, kind, status, rtl="r7"):
    return {"name": name, "kind": kind, "status": status, "rtl": rtl}

previous = [row("a_conserve", "proof", "proven", "r6"), row("c_stall", "cover", "reached", "r6"),
            row("a_data", "proof", "proven", "r6")]
good = [row("a_conserve", "proof", "proven"), row("c_stall", "cover", "reached"), row("a_data", "proof", "proven")]
assert gate(good, previous, "r7") == []

bad = [row("a_conserve", "proof", "counterexample"), row("c_stall", "cover", "inconclusive"),
       row("a_data", "proof", "inconclusive")]
caught = gate(bad, previous, "r7")
assert len(caught) == 3
assert any("newly inconclusive" in f for f in caught)
assert any("cover not reached" in f for f in caught)

sneaky = [dict(r) for r in good]
sneaky[2]["status"] = "timeout-pass"
assert any("unknown status" in f for f in gate(sneaky, previous, "r7"))
unreached = [dict(r) for r in good]
unreached[1]["status"] = "unreached"
assert any("unknown status" in f for f in gate(unreached, previous, "r7"))
stale = [dict(r) for r in good]
stale[0]["rtl"] = "r6"
assert any("another revision" in f for f in gate(stale, previous, "r7"))
print("PASS: clean ledger passes; counterexample, uncovered cover, drift, stale row and odd labels all fail")

What the review looks for

• The per-commit set is timed in minutes and the nightly set in hours across parallel tasks.

• The gate fails on counterexamples, required covers not reached, newly inconclusive proofs and rows from another revision.

• No status outside the allowed ones can pass the gate; unknown labels fail loudly.

Verify and debug

Test the gate quarterly with a seeded failing ledger: one counterexample, one cover not reached, one timeout. If any of the three passes the gate, the reporting chain is broken upstream of the gate and no result downstream can be trusted. Keep the previous run used for comparison pinned to a revision hash; comparing against a floating baseline hides drift.

Related topics

• Next: Result Triage and Trends

• VFP: Drills

• VFP: Sign-Off