A formal run ends with one of three answers: proven for the stated model and assumptions, a counterexample trace, or inconclusive. Behind those answers sit several engines: bounded search that unrolls the design, induction that generalises from a window of states, clause-learning engines that build the invariant themselves, and liveness machinery that turns an infinite obligation into something checkable. This section opens each engine far enough that you can read its verdicts, then teaches the convergence discipline: diagnose first, then reduce, split or strengthen, and report an honest bound when nothing closes.
Topic | What it covers | After it you can... |
|---|---|---|
States, reachability, how sets of states are stored, the engine menu | Say what each engine proves, refutes and costs, and why two runs can differ. | |
Unrolling by hand, choosing a depth, what a bounded pass licenses | Derive a depth from reset, trigger and latency, and report bounded to N honestly. | |
Base case and step, counterexamples to induction, helper invariants, discovery | Read a CTI, write the helper that excludes it, and prove every helper. | |
Frames, blocking, propagation, over-approximation, reading engine output | Explain how a learning engine finds the invariant without a hand-written helper. | |
Weak and strong fairness, lasso counterexamples, counter-based substitutes | Write a bounded-response check, read a lasso, and spot fairness that hides starvation. | |
Diagnose before tuning, case splits, lemma stacks, when to stop | Turn an inconclusive run into a plan instead of a longer timeout. |
Suggested order: top to bottom. The first two topics fix vocabulary every later lesson relies on: states and reachability, then what a bound does and does not buy. K-induction is the workhorse you will actually drive, so it comes third with the decade counter as its running example. The concept-level engines topic explains what happens when the tool learns the invariant itself. Liveness needs all of that vocabulary before fairness makes sense. Convergence tactics close the section because every tactic refers back to an engine behaviour taught earlier. Readers chasing one failure can start at its topic, but the k-induction topic assumes the bounded-results topic.
Yes: the first run says only that no violation exists within 8 steps, and the deeper run looked further, so they answer different questions about the same model. If both runs used the same model, assumptions, reset and bound, a pass and a counterexample could not both be right, and a counterexample would win. The first topic of this section teaches that rule; the last teaches how to stop the confusion arising.