The course runs on one open flow: tasks, depths, and a three-outcome ledger. The reader's project may run on another tool entirely, with its own engines, applications, and dashboards. Without a map between the two, every lesson feels tool-specific and none of it transfers. This lesson is the map: concepts first, tool mechanics second, and a checklist that evaluates any flow honestly.
Job of this lesson: map the course flow onto any formal tool and say what scale changes.
Every formal flow has the same skeleton whatever its name: setup scripts that build the model, task definitions that say what runs at which depth, parallelism across tasks, a results database with the three outcomes, trace viewing, and application packages for connectivity, registers and deadlock. The mapping table below carries each course concept across. What changes at scale is capacity and breadth: larger cones, engine portfolios that pick strategies per property, application packages that generate properties from tables, and dashboards that must still refuse to count a timeout as a pass. Two behaviours differ silently between tools and are worth a row of their own: how a combinational loop is broken, and what happens to constructs that only mean something in simulation.
Course concept | What any formal tool provides | What to check when evaluating |
|---|---|---|
Proof header with depth | Task definition with bounds | Depths recorded per task, rerun on change |
Bounded check, induction, covers | Engine portfolio and cover tasks | Which engine proved what, at which depth |
Three-outcome ledger | Results database | Timeouts land inconclusive, never proven |
Counterexample trace | Trace viewing and minimisation | Traces replayable and minimised |
Table-driven connectivity | Connectivity application | All modes and configurations covered |
Assumption list | Constraint management | Every assumption reviewed and discharged |
Combinational loops | A rule for breaking each loop | Loops are reported, not cut silently at an arbitrary point |
Simulation-only constructs | A rule for delays, initial blocks, forces | Every ignored construct is reported, and the report is read |
The script below scores a flow against eight non-negotiable capabilities: recorded depths, named engines, three-outcome results, replayable traces, reviewed assumptions, hash-pinned reruns, reported loops and reported ignored constructs. It also reads the flow's status mapping, the table that turns the tool's own words into the three outcomes, and rejects a mapping that sends a timeout to proven or that invents a fourth outcome. The test shows each failure caught on exactly its own row:
REQUIRED = ["depths-recorded", "engines-named", "three-outcomes", "traces-replayable",
"assumptions-reviewed", "hash-pinned-reruns", "loops-reported", "ignored-constructs-reported"]
OUTCOMES = ("proven", "counterexample", "inconclusive")
NEVER_PROVEN = ("timeout", "undetermined", "unknown", "bounded")
def check_flow(flow):
problems = ["missing: " + c for c in REQUIRED if c not in flow["has"]]
for raw, mapped in flow["status_map"].items():
if mapped not in OUTCOMES:
problems.append("status " + raw + " maps outside the three outcomes")
elif raw in NEVER_PROVEN and mapped == "proven":
problems.append("status " + raw + " maps to proven")
return problems
good = {"has": list(REQUIRED), "status_map": {"pass": "proven", "fail": "counterexample", "timeout": "inconclusive"}}
assert check_flow(good) == []
thin = dict(good, has=["depths-recorded", "engines-named", "traces-replayable"])
assert check_flow(thin) == ["missing: three-outcomes", "missing: assumptions-reviewed", "missing: hash-pinned-reruns",
"missing: loops-reported", "missing: ignored-constructs-reported"]
relabelled = dict(good, status_map={"pass": "proven", "timeout": "proven"})
assert check_flow(relabelled) == ["status timeout maps to proven"]
fourth = dict(good, status_map={"pass": "proven", "pass-with-warnings": "pass"})
assert check_flow(fourth) == ["status pass-with-warnings maps outside the three outcomes"]
print("PASS: complete flow accepted; thin, relabelled and four-outcome flows are each rejected on their own row")No lesson depends on a tool-specific behaviour; every result is stated as proven, counterexample, or inconclusive with its model and depth.
The evaluation checklist is applied to the project's own flow before signoff work starts.
Scale changes are named: capacity, engine choice, applications, and dashboards, not new semantics.
When moving flows, rerun the course's own proof pairs on the new tool first: the passing and failing partners must reproduce before any project property is trusted there. If a result differs, suspect assumption or reset handling first, in this order: initial state, reset modelling, assumption semantics, then the engine. Read the loop report and the ignored-construct report on the first run: a loop cut at the wrong place or a delay ignored without a message changes the model without changing the result's label.
Under inconclusive until it is understood: only proven, counterexample, and inconclusive enter the ledger, and anything else fails the gate loudly.
Its cost and its organisation: capacity, engines, applications, parallelism. A proof still means proven for the stated model and assumptions, whatever the tool.