Model Checking — Interview Level¶

Roadmap: Formal Methods & Verification → Model Checking A model-checking interview rarely asks you to recite the BDD algorithm. It asks "how is this different from writing a thousand tests," then "your checker says PASS — what could still be wrong," and watches whether you can separate the model from the code, a counterexample from a stack trace, and safety from liveness. This page is the question bank, with model answers and a note on what each question is really probing.

How to Use This Page¶

Each question carries three things: Q (the prompt), what the interviewer is really testing, and A (a model answer at the depth a strong candidate gives). Don't memorize the answers — internalize the distinctions they keep returning to:

exhaustive vs sampled (every reachable state of a model vs the inputs your tests happened to pick)
model vs code (you verify the abstraction, not the bytes that ship)
safety vs liveness ("nothing bad ever" vs "something good eventually")
bug-finding vs proof (a counterexample is always real; PASS is only as strong as the model and the bound)

Nearly every question in this bank is one of those four distinctions wearing a costume. The candidates who do well are the ones who name the distinction before reaching for an algorithm.

Prerequisites¶

You'll answer better if you're comfortable with:

A state machine — states, transitions, an initial state, and the idea of an execution as a path through them.
Concurrency basics — interleavings, race conditions, why "it worked the 10,000 times I ran it" proves nothing about the 10,001st.
Propositional logic — ∧ ∨ ¬ →, and the difference between "for all" and "there exists."
Big-O intuition — enough to feel why a product of components is exponential, which is the whole drama of model checking.

You do not need to have used a specific tool, but knowing the names — TLA+/TLC, SPIN, NuSMV, CBMC — and what class each belongs to will read as senior.

Introduction¶

Model checking is the corner of formal methods most likely to come up in a systems, distributed, or hardware interview, because it's the one that found a real bug someone shipped. The questions cluster into five themes: the fundamentals (what it is, why a counterexample beats a green test suite), temporal logic (how you say "never" and "eventually" precisely), algorithms and the state-explosion problem (the differentiator — anyone can say "it checks all states"; few can say how and what to do when there are 10⁴⁰ of them), the limits (the abstraction gap, vacuity, decidability), and practice/scenarios (where it pays, the AWS TLA+ story, and "the checker passed — now what").

The trap throughout is overclaiming. A weak candidate says "model checking proves your code is correct." A strong one says "it exhaustively checks a finite model against a temporal property, and either hands me a concrete counterexample or tells me the property holds in that model under those assumptions" — and then can list everything those weasel-words are carrying.

Fundamentals¶

Q: What is model checking, and how is it different from testing?¶

Testing: The single most important framing in the topic. Do you grasp exhaustive over a model vs sampled over the real thing?

A. Model checking takes a finite-state model of a system and a property stated in temporal logic, and exhaustively explores every reachable state and every interleaving of the model to decide whether the property holds. If it doesn't, the checker produces a counterexample: a concrete execution that violates it.

The contrast with testing is two independent axes, and people usually only name one: - Coverage: a test exercises one path through one schedule with one set of inputs. Model checking covers all reachable states and all interleavings of the model. For a concurrency bug that needs a specific thread schedule, testing is a lottery; model checking is exhaustive. - Subject: a test runs the real code. Model checking runs a model — a deliberately simplified abstraction. So testing can catch bugs in code the model abstracts away, and model checking can catch bugs no realistic test schedule would ever hit.

So they're complementary, not competitors: model checking attacks the design-level concurrency/protocol bugs that are nearly impossible to test, and testing validates that the implementation matches the design model checking proved.

Q: Define state, transition, and state space.¶

Testing: Whether you can speak the vocabulary precisely instead of waving at "the system."

A. A state is a complete snapshot of everything the model tracks at one instant — every variable's value, each process's program counter, the contents of channels. A transition is an allowed single step from one state to another (an action firing, a message delivered, a process advancing one line). The state space is the directed graph of all reachable states with transitions as edges; model checking is, mechanically, a graph search over it.

The number that matters is the size of that graph. If you have n boolean variables and p processes each with k program-counter positions, the state space is on the order of 2ⁿ · kᵖ — it's a product, so it grows exponentially. That product is the source of every hard problem in the field.

Q: What is a counterexample, and why is it called the killer feature?¶

Testing: Whether you understand what makes model checking usable by working engineers, not just provable-in-principle.

A. A counterexample is a concrete, replayable execution trace that violates the property — the exact sequence of states and transitions, step by step, that leads to the bad state. For a safety violation it's a finite path to the bad state; for a liveness violation it's a lasso: a finite prefix leading into a cycle the system can loop in forever without the good thing happening.

It's the killer feature because it converts an abstract "your design is wrong" into "here is how." A theorem prover that says "not provable" leaves you stuck; a model checker hands you a numbered trace you can read like a screenplay — "process 1 reads, then process 2 reads the stale value, then both write." That trace is always real with respect to the model: unlike a flaky test, a counterexample can't be a false positive of the search. It's the difference between "there's a bug somewhere" and a debugger sitting on the exact line. It also doubles as a regression test and as the clearest possible bug report to a teammate.

Q: Distinguish safety and liveness properties. Give an example of each.¶

Testing: The classification that determines which algorithm runs and whether you need fairness.

A. A safety property says "something bad never happens" — it's violated by a finite prefix, the exact moment the bad thing occurs. Examples: "two processes are never in the critical section at once" (mutual exclusion), "the balance never goes negative," "we never deadlock." A safety violation is a finite trace to a bad state, which is why safety checking is "just" reachability — search the graph for a state where the bad predicate holds.

A liveness property says "something good eventually happens" — it can only be violated by an infinite execution that goes on forever without the good thing. Examples: "every request is eventually answered," "the lock is eventually acquired," "the system eventually terminates." A liveness violation is a cycle you can get stuck in forever — the lasso counterexample.

The practical punchline: safety = reachability (find a bad state), liveness = cycle detection (find a reachable loop that starves the good event). They use different algorithms, and liveness almost always needs fairness assumptions to be checkable at all.

Temporal Logic¶

Q: What is temporal logic and why do you need it instead of ordinary assertions?¶

Testing: Whether you understand that properties are about executions over time, not single states.

A. An ordinary assertion (assert balance >= 0) is a predicate on a single state. But the interesting properties are about whole executions: "after every request there is eventually a response," "we never reach deadlock on any path." You can't say "eventually" or "on all future paths" with a state predicate — you need operators that quantify over time and over the branching of possible futures. Temporal logic is propositional logic plus those operators, and it's the language model checkers actually consume.

Q: Contrast LTL and CTL.¶

Testing: The single most common temporal-logic question. Linear time vs branching time.

A. LTL (Linear Temporal Logic) reasons about a single timeline at a time: a property holds if it holds along every execution path, but each formula talks about one path. Its operators: - □φ (globally / always) — φ holds at every step. - ◇φ (finally / eventually) — φ holds at some future step. - X φ (next) — φ holds in the next state. - φ U ψ (until) — φ holds until ψ becomes true (and ψ does become true).

CTL (Computation Tree Logic) reasons about the branching tree of futures, pairing a path quantifier with each temporal operator: - A (for all paths) and E (there exists a path). - So AG φ = "on all paths, always φ"; EF φ = "there exists a path on which eventually φ."

The key difference: LTL can't say "there exists a path where..."; CTL can (E). CTL can express reset reachability — AG(EF reset) ("from every reachable state, it's possible to get back to a reset state"), which LTL simply cannot say. Conversely LTL can express strong fairness and certain path properties CTL can't. They're incomparable — neither subsumes the other — which is why some tools speak LTL (SPIN, TLA+'s temporal fragment), some CTL (classic NuSMV), and some both (CTL). For most protocol* work, engineers reach for LTL because "on all executions, X" is the natural shape of the spec.

Q: Express "the two processes are never both in the critical section" and "every request is eventually answered."¶

Testing: Whether you can go from English to formula — and classify each.

A. Mutual exclusion is a safety property:

□ ¬(inCS₁ ∧ inCS₂)

"Always, it is not the case that both are in the critical section." Equivalently in CTL, AG ¬(inCS₁ ∧ inCS₂).

"Every request is eventually answered" is a liveness property, and the clean way to say it is a response pattern:

□ (request → ◇ response)

"Always: whenever a request occurs, eventually a response occurs." Note the shape — a □ wrapping an implication whose consequent is ◇. That nesting (□(p → ◇q)) is the canonical "response" template and is worth recognizing on sight; it's the most common liveness property in real specs. As a CTL approximation you'd write AG(request → AF response).

Q: Why does liveness need fairness, when safety doesn't?¶

Testing: The subtlest temporal-logic point, and a frequent staff-level differentiator.

A. Because without fairness, the model contains pathological infinite executions that no real scheduler would ever produce, and liveness properties are violated precisely by infinite executions. Concretely: model "every request is eventually answered," but let the scheduler be free to run process A forever and never schedule process B. Then B's request is never answered — and the checker correctly reports a liveness violation. But that "bug" is an artifact: a real OS scheduler won't starve a runnable thread forever.

Fairness assumptions rule out those degenerate runs so the checker only considers realistic infinite behaviors: - Weak fairness: if an action is continuously enabled, it eventually fires (no thread that's always ready is ignored forever). - Strong fairness: if an action is infinitely often enabled, it eventually fires (handles actions that flicker in and out of being enabled).

Safety doesn't need fairness because a safety violation is a finite prefix — it happens at a definite moment regardless of what the scheduler does forever-after. You only argue about infinite futures for liveness, so fairness is a liveness-only concern. A candidate who says "my liveness check fails" and immediately asks "did you state your fairness assumptions?" is signaling real experience.

Algorithms & State Explosion¶

Q: How does explicit-state model checking work for a safety property?¶

Testing: Whether you can reduce "checks all states" to a concrete graph algorithm.

A. For safety it's reachability via graph search. Maintain a visited set (typically a hash table of state fingerprints) and a frontier (a stack for DFS or queue for BFS). Start from the initial state(s); for each state, compute its successor states (fire every enabled transition), check the safety predicate on each, and if a successor is new, add it to visited and the frontier. If you ever reach a state where the bad predicate holds, the path that got you there is the counterexample. If the frontier empties with no violation, the property holds in the model — you've proven it, because you visited every reachable state.

The two costs are time (number of transitions explored) and memory (size of the visited set) — and memory is almost always the binding constraint. The whole field is about not storing or not visiting states you can avoid.

Q: How does liveness checking work — the automata / Büchi / nested-DFS approach?¶

Testing: The differentiator. This is where breadth between "I read about it" and "I understand it" shows.

A. Liveness is checked via the automata-theoretic approach. You negate the LTL property and translate ¬φ into a Büchi automaton — a finite automaton over infinite words whose accepting condition is "visits an accepting state infinitely often." You take the product of this automaton with the system's state graph. Now the question "does the system have an execution violating φ?" becomes "does the product have a reachable accepting cycle?" — an infinite run that hits an accepting (i.e., property-violating) state infinitely often.

You find such a cycle with nested depth-first search: an outer DFS reaches accepting states; from each, an inner DFS looks for a cycle back to that same state. A found cycle is a lasso — a finite stem into a loop — and that lasso is the liveness counterexample: "the system can do this prefix, then loop here forever, never answering the request." SPIN is the canonical tool built on exactly this (LTL → Büchi → product → nested DFS). The elegance is that it unifies safety and liveness under one umbrella — both become "is there a reachable bad structure in a product graph," a state vs a cycle.

Q: What is symbolic model checking, and why was it a breakthrough?¶

Testing: Whether you know there's a fundamentally different attack on state explosion than "visit states faster."

A. Explicit-state checking enumerates states one at a time. Symbolic model checking instead represents sets of states and the transition relation as boolean formulas, and manipulates whole sets at once. The classic encoding uses BDDs (Reduced Ordered Binary Decision Diagrams), a canonical compressed form for boolean functions. Reachability becomes repeated image computation — "given this set of states, what's the set reachable in one step?" — as BDD operations, iterated to a fixpoint. The win: a BDD can represent 10²⁰ states in a structure with a few thousand nodes when the state set has regularity to exploit. This is what made hardware verification practical in the 1990s (Clarke, McMillan, SMV) — circuits have enormous but highly structured state spaces that BDDs compress beautifully. The catch: BDD size is exquisitely sensitive to variable ordering (a bad order is exponentially larger), and some functions — multipliers are the textbook example — have no compact BDD at all.

Q: What is bounded model checking, and when is it a proof versus just bug-finding?¶

Testing: A crucial, often-missed nuance — BMC is sound for bugs but not automatically for correctness.

A. Bounded model checking (BMC) asks a narrower question: "is there a counterexample of length ≤ k?" It unrolls the transition relation k times into one big boolean/arithmetic formula — Init ∧ Trans(s₀,s₁) ∧ … ∧ Trans(s_{k-1},s_k) ∧ (a bad state occurs within k steps) — and hands it to a SAT or SMT solver. If the solver finds a satisfying assignment, that is a concrete counterexample of length ≤ k. If it's UNSAT, there's no bug within k steps.

The critical nuance: UNSAT at depth k does not prove the property — it only proves no violation happens within k steps; a bug at step k+1 is untouched. So plain BMC is a bug-finder, excellent and fully automatic, but unsound for correctness claims. It becomes a proof when you also establish the completeness threshold (a k provably large enough that no longer counterexample can exist — e.g., k ≥ the diameter of the state graph), or when you use an inductive/interpolation-based extension (k-induction, IC3/PDR) to close the gap. The honest one-liner: "BMC found nothing up to k" means "no bug in k steps," not "no bug."

Q: What is IC3/PDR?¶

Testing: Awareness of the modern algorithm that often beats BDDs and BMC — a strong senior signal.

A. IC3 (also called PDR, Property-Directed Reachability) is a SAT-based algorithm that proves a safety property without unrolling the whole transition relation. It incrementally builds a sequence of over-approximations of the states reachable in i steps, each represented as a set of learned clauses, and uses the SAT solver to either push them toward an inductive invariant that excludes the bad states (a proof) or discover a counterexample. Its appeal: it's frame-incremental, often dramatically more memory-efficient than BDD-based methods, and it can prove properties (find the inductive invariant), not just bound them like raw BMC. It's the workhorse of modern hardware model checkers and a common answer to "what beats BMC and BDDs in practice today."

Q: Name the main ways to fight state explosion.¶

Testing: Breadth on mitigations — the practical core of the topic.

A. State explosion is the central problem: the state space is a product, so it's exponential in the number of components and variables. The mitigations attack it from different angles:

Technique	Idea	Best for
Symbolic / BDD	Represent state sets as compressed boolean formulas	Structured, regular spaces (hardware)
Bounded MC (SAT/SMT)	Only search depth ≤ k; never materialize the full space	Bug-finding, deep designs
IC3 / PDR	Build an inductive invariant via SAT, no full unroll	Modern safety proofs
Partial-order reduction	Skip redundant interleavings of independent concurrent actions	Concurrency / message passing
Symmetry reduction	Collapse states identical up to permuting interchangeable components	N identical processes/nodes
CEGAR (abstraction)	Verify a coarse abstraction; refine only when a counterexample is spurious	Software with huge data domains

Partial-order reduction and symmetry reduction are the two most worth naming for concurrency/distributed work: independent actions (e.g., two threads touching unrelated variables) can be reordered without changing the outcome, so you explore one representative ordering instead of all n!; and if you have N identical workers, states that differ only by which worker is in which role are equivalent, so you keep one per equivalence class. Both can turn an intractable space tractable.

Q: Explain CEGAR.¶

Testing: Whether you understand the abstraction-refinement loop that lets model checking attack software.

A. CEGAR — Counterexample-Guided Abstraction Refinement — is the loop that makes model checking real programs feasible despite enormous data domains. You start with a deliberately coarse abstraction (e.g., predicate abstraction: track only a handful of boolean predicates over the program's variables, ignoring exact values). You model-check the abstraction. Three outcomes: (1) it holds → since the abstraction over-approximates the real system, the property holds for the real program too — done. (2) The checker finds a counterexample → you check whether it's real in the concrete program. If real, it's a genuine bug. (3) If the counterexample is spurious (an artifact of the abstraction being too coarse), you use it to refine the abstraction — add the predicate(s) that rule out that spurious trace — and re-check. Loop until proof or real bug. CEGAR (pioneered in SLAM/BLAST, behind Microsoft's Static Driver Verifier) is how you get model checking to scale to C code: never track more detail than a counterexample forces you to.

Q: Why is state explosion fundamental and not just an engineering problem?¶

Testing: Whether you can name the complexity reality without despair.

A. Because the state space is a Cartesian product of component states — n boolean variables alone give 2ⁿ states, and concurrent processes multiply their local spaces and their interleavings. It's exponential by construction, not by sloppiness. The decision problems are genuinely hard (LTL model checking is PSPACE-complete in the size of the formula and system). The mitigations above don't eliminate the exponential — they exploit structure (regularity → BDDs, independence → POR, symmetry → symmetry reduction, irrelevance → CEGAR) to make the practically interesting cases tractable. The honest framing: model checking is "decidable but expensive," and the engineering is all about which structure your particular problem has that you can exploit.

Limits¶

Q: A model checker says your protocol is correct. What did it actually verify?¶

Testing: The abstraction gap — the most important humility in the whole field.

A. It verified that your model satisfies the properties you wrote, under the assumptions you encoded, within the bounds you set. That is not the same as "the code is correct." The gap has several named edges: - Model vs code: you checked an abstraction, hand-written in TLA+/Promela/etc. The implementation can diverge from the model — the code can have a bug the model abstracted away, or the model can be subtly unfaithful to the design. - The properties you wrote: the checker can't verify a property you didn't state. It only proves what you asked. - Vacuity: the property might be trivially true (satisfied because its premise never fires), so PASS means nothing. - The bounds: if it's finite/bounded (fixed N processes, BMC depth k), a bug at N+1 or step k+1 is invisible.

So the correct claim is narrow and load-bearing: "the design, as modeled, has no violation of these properties for these configurations." That's enormously valuable — it kills whole classes of design bugs — but anyone who says "model checking proved my system correct" is overselling, and a good interviewer will press exactly there.

Q: What is vacuity, and how do you guard against it?¶

Testing: A specific, sharp failure mode that catches careless modelers.

A. A property is vacuously true when it's satisfied for a degenerate reason rather than the reason you intended — classically, an implication whose antecedent is never true. □(request → ◇response) is vacuously satisfied if request never occurs in your model: the implication is true at every state because its premise is always false, so the checker reports PASS while having verified nothing about responses. You introduced the vacuity by over-constraining the model (maybe you guarded requests behind a condition that's never met).

Guards: (1) write sanity properties that should fail and confirm they do — e.g., assert □¬request and expect a counterexample, proving requests can actually happen; (2) check that key transitions are reachable (the checker can report unreached states or actions); (3) use vacuity detection if the tool offers it; (4) inspect coverage — TLC can report how many distinct states each action generated, and an action that fired zero times is a red flag. The discipline: a PASS you didn't try to break is a PASS you can't trust.

Q: Model checking is "decidable" — so why can't it verify everything?¶

Testing: Whether you understand the finiteness boundary and infinite-state reality.

A. Model checking is decidable for finite-state systems — that's the deal: bounded states, terminating search. The moment the system is infinite-state — unbounded integers, dynamically allocated data structures, arbitrary numbers of processes, real-valued time — full automatic verification can become undecidable (it bumps into the halting problem and Rice's theorem). The field handles this with the techniques above: abstraction (CEGAR collapses an infinite data domain to finite predicates), bounding (fix N, fix depth k), and for unbounded-parameter systems, specialized parameterized verification that sometimes proves "correct for all N" via a cutoff theorem. But in general: finite or finitely-abstracted is the price of full automation; go truly infinite and you trade automation for interactive proof assistants.

Q: When does a passing bounded model check give false confidence?¶

Testing: The "bound too small" trap, distinct from vacuity.

A. When the bound is smaller than the shortest counterexample. BMC says "no bug in ≤ k steps"; if the real bug needs k+3 steps (a violation that only manifests after a longer handshake, a queue filling up, a third retry), it sails through clean. Likewise, checking a protocol with N = 2 nodes can pass while the bug only appears at N = 3 (the classic "two-node systems are deceptively well-behaved" phenomenon — many distributed bugs need a third party to create the problematic interleaving). The mitigations: push k toward the completeness threshold / system diameter so UNSAT becomes a real proof, ramp N up to a researched small-model bound (often 3–5 suffices for many protocol classes), and treat any "passed at the smallest config" result as provisional until you've justified why that config is sufficient.

Practice & Scenarios¶

Q: Where does model checking actually pay off?¶

Testing: Whether you can target it instead of treating it as a universal hammer.

A. It pays off exactly where the bugs are concurrency/interleaving-driven, low-probability, and catastrophic — the bugs testing is worst at and the blast radius is worst: - Distributed protocols — consensus, replication, leader election, cache coherence, two-phase commit. These have astronomically many interleavings, a handful of which corrupt data or lose a committed write. - Concurrency primitives — lock-free algorithms, memory-model reasoning, synchronization protocols where one bad schedule in a billion deadlocks or violates an invariant. - Hardware / circuits — the original killer app; structured state spaces, and a respin costs millions, so exhaustive proof is worth it.

The common thread: the design has subtle global invariants, the bug needs a specific rare schedule, and a field failure is expensive or unrecoverable. It pays least on straight-line business logic with simple, testable data transformations — there, examples and property-based tests are cheaper and catch the same bugs.

Q: Tell me about the AWS / TLA+ story and what it demonstrates.¶

Testing: Whether you know the canonical industrial proof point and why it matters.

A. AWS engineers used TLA+ (Lamport's specification language, model-checked by TLC) to model core services — DynamoDB, S3, EBS, internal replication and locking protocols. The reported results (Newcombe et al., "How Amazon Web Services Uses Formal Methods," CACM 2015) are the field's best industrial evidence: - TLC found subtle bugs in designs that had passed extensive review and testing — including a bug requiring a specific 35-step sequence of events, far beyond what any human reviewer or test would explore. - Engineers reported the specs paid off twice: catching bugs and as precise, executable design documentation that let them refactor aggressively with confidence. - Crucially, this was practicing engineers (not formal-methods PhDs) applying it to real production systems at the design stage.

What it demonstrates: model checking the design — at the RFC/whiteboard stage, before code — catches deep concurrency bugs cheaply, and the technique is accessible to ordinary strong engineers, not just academics. That's the line to land: model the design, not (only) the code, and do it before you build.

Q: How do you read and act on a counterexample?¶

Testing: Whether you treat a counterexample as a debugging artifact, calmly.

A. A counterexample is a numbered sequence of states; you read it like a screenplay. The discipline: 1. Find the last good state and the transition that crosses into the violation — that's the precise moment the invariant breaks. 2. Read the trace as a story: "process 1 reads X, process 2 reads the same X before 1 writes, both increment, one update is lost." Concurrency counterexamples almost always reveal a specific interleaving you didn't think about. 3. Decide the category: is it a real design bug (fix the design and re-check), or a modeling error / missing fairness / wrong property (fix the spec)? A surprising number of first counterexamples are "my property was wrong," and that's also valuable — it sharpened your understanding. 4. Minimize: prefer the shortest counterexample; BFS-based search gives you the shortest trace, which is the easiest to understand. 5. Keep it as a regression — re-run after the fix to confirm it's gone.

The mindset that reads well: a counterexample is a gift — it's the exact failing schedule served on a plate, which is precisely what you can never get reliably from testing a concurrency bug.

Q: Compare model checking, property-based testing, and proof assistants.¶

Testing: Whether you can place model checking on the spectrum of rigor vs effort vs automation.

A. They sit on a spectrum of rigor and scope vs automation and cost:

	What it checks	Exhaustive?	Automation	Best for
Property-based testing	Real code against properties, on generated inputs	No — sampled	Fully automatic	Implementation-level invariants, round-trips
Model checking	A model against temporal properties, all states/interleavings	Yes — within the model/bound	Mostly automatic (push button + write spec)	Concurrency/protocol design bugs
Proof assistants (Coq/Isabelle/Lean)	Anything expressible, including infinite-state, against full theorems	Total proof	Interactive — human guides it	Foundational, infinite-state, highest assurance

The decision: property-based testing for "is my code right on lots of inputs," cheaply and continuously in CI. Model checking for "is my design free of concurrency/protocol bugs," done once at design time on a finite model. Proof assistants for the rare crown-jewel components (a compiler, a crypto primitive, a kernel) where you need a machine-checked theorem over all cases and can afford person-years. They compose: model-check the design, property-test the implementation against the same invariants, and reserve proof for the parts that justify the cost.

Q (Scenario): Model two processes contending for a critical section. State the safety and liveness properties.¶

Testing: Can you actually set up a model and write the properties — the staple whiteboard exercise.

A. Each process cycles through three control states — idle → trying → critical → idle — and shares whatever coordination state the algorithm uses (a lock flag, turn variable, etc.). A global state is the pair of program counters plus the shared variables; transitions are "process i takes its next step," and the checker explores all interleavings of the two processes' steps.

Sketched in TLA+-flavored pseudocode:

VARIABLES pc1, pc2, lock      \* pc ∈ {"idle","trying","critical"}

Init == pc1 = "idle" /\ pc2 = "idle" /\ lock = FALSE

\* Process 1's steps (process 2 symmetric)
Try1   == pc1 = "idle"    /\ pc1' = "trying"   /\ UNCHANGED <<pc2, lock>>
Enter1 == pc1 = "trying"  /\ ~lock /\ lock' = TRUE  /\ pc1' = "critical" /\ UNCHANGED pc2
Exit1  == pc1 = "critical"/\ lock' = FALSE /\ pc1' = "idle" /\ UNCHANGED pc2

Next == Try1 \/ Enter1 \/ Exit1 \/ Try2 \/ Enter2 \/ Exit2

The properties:

\* SAFETY — mutual exclusion: never both in the critical section
Safety  ==  [] ~(pc1 = "critical" /\ pc2 = "critical")

\* LIVENESS — no starvation: a process that wants in eventually gets in
Live1   ==  [] (pc1 = "trying" => <> (pc1 = "critical"))
Live2   ==  [] (pc2 = "trying" => <> (pc2 = "critical"))

I'd also note: the liveness properties are only meaningful under weak fairness on each process's Enter action — otherwise the scheduler can starve a process forever and the checker reports a "violation" that's really just an unfair schedule. Checking this tiny model exhaustively will, for a naive lock, often surface a real starvation lasso — which is exactly the point of the exercise.

Q (Scenario): The model checker says PASS. What could still be wrong?¶

Testing: The capstone humility question. This is the one that separates levels.

A. A PASS is only as strong as four things, and I'd enumerate all four: 1. Vacuity — the property may be trivially true because its premise never fires (requests never happen, so "every request answered" is empty). Guard: assert sanity properties that should fail and confirm they do. 2. Bound too small — if it's bounded (BMC depth k, or N = 2 processes), the bug may live at k+1 or N = 3. Guard: justify the bound (completeness threshold, small-model theorem) or ramp it up. 3. Wrong abstraction — the model may not faithfully represent the design/code: I may have abstracted away the very mechanism that's buggy, or modeled an idealized network with no message loss/reorder when the real one drops packets. Guard: review model fidelity, model the adversarial environment explicitly. 4. Wrong property — I may have verified the wrong thing: a property that's too weak, or subtly mis-stated, so it passes while the real invariant I care about is untouched. Guard: peer-review the properties as carefully as the model.

The summary line: "PASS means this model satisfies these properties under these assumptions within these bounds — every one of those four is a place the real system can still be wrong." That sentence, said unprompted, is what a staff-level answer sounds like.

Q (Scenario): Your model checker runs out of memory before finishing. What do you do?¶

Testing: Whether you can apply the state-explosion mitigations as concrete moves, in order.

A. Out-of-memory means the visited-state set outgrew RAM — the state space is too big for explicit enumeration. I'd attack it in roughly this order, cheapest-first: 1. Shrink the model. Most state explosion is self-inflicted: reduce the number of processes/nodes to the smallest that can still exhibit the bug class (often N = 3), shrink data domains (model a queue of capacity 2, not 1000), and remove variables that don't affect the property. A smaller faithful model is the highest-ROI move. 2. Symmetry reduction. If components are interchangeable (N identical workers), enable symmetry reduction so states equal up to permutation collapse to one representative. 3. Partial-order reduction. For concurrency, turn on POR so independent interleavings aren't all explored — often a massive cut. 4. Switch technique. Move from explicit-state to symbolic/BDD (if the space is structured) or to bounded model checking with SAT/SMT (search depth ≤ k without materializing the whole space) — accepting that BMC gives bug-finding, not a full proof, unless I reach the completeness threshold. 5. Abstract. Apply predicate abstraction / CEGAR to collapse a large data domain to a few booleans. 6. Engineering knobs. State compression / hashing (SPIN's bitstate hashing trades completeness for memory), more RAM, or disk-based search — last resorts.

The framing that reads as senior: first make the model smaller and exploit its symmetry/independence; only then change the algorithm; only then throw hardware at it. Out-of-memory is usually a signal that the model is bigger than it needs to be, not that the problem is intractable.

Rapid-Fire¶

Short questions to check breadth. One or two sentences each.

Q: Model checking vs testing in one line? A: Exhaustive over all states/interleavings of a model vs sampled over a few runs of the real code.
Q: Safety vs liveness? A: "Nothing bad ever" (violated by a finite prefix) vs "something good eventually" (violated by an infinite run / cycle).
Q: What's a counterexample? A: A concrete, replayable trace that violates the property — the killer feature; always real with respect to the model.
Q: What's a lasso? A: A liveness counterexample — a finite stem leading into a cycle the system loops in forever without the good thing happening.
Q: □ and ◇ mean? A: □ = always/globally; ◇ = eventually/finally.
Q: LTL vs CTL in a phrase? A: LTL reasons over single linear timelines; CTL adds path quantifiers (A/E) to reason over the branching tree of futures.
Q: Write mutual exclusion. A: □ ¬(inCS₁ ∧ inCS₂).
Q: Write "every request eventually answered." A: □(request → ◇response).
Q: Why does liveness need fairness? A: Without it, the model contains starving schedules no real scheduler produces, giving spurious liveness violations.
Q: The state-explosion problem? A: The state space is a product of components, so it's exponential — the central obstacle.
Q: BMC — proof or bug-finding? A: Bug-finding by default ("no bug in ≤ k steps"); a proof only at the completeness threshold or with k-induction/IC3.
Q: What does symbolic/BDD model checking do differently? A: Represents sets of states as boolean formulas and explores them en masse, instead of one state at a time.
Q: What is CEGAR? A: Counterexample-guided abstraction refinement — verify a coarse abstraction, refine only when a counterexample turns out spurious.
Q: POR vs symmetry reduction? A: POR skips redundant orderings of independent actions; symmetry reduction collapses states equal up to permuting interchangeable components.
Q: Two famous tools and their class? A: SPIN (explicit-state, LTL/Büchi); TLA+/TLC and NuSMV (symbolic / state-enumeration for designs).
Q: One-line AWS takeaway? A: TLA+ found deep multi-step concurrency bugs in production-grade designs that survived review and testing.
Q: "PASS" — what's the catch? A: It holds for this model, these properties, these assumptions, within these bounds — not "the code is correct."

Red Flags / Green Flags¶

What interviewers infer from how you answer, not just whether you're right.

Red flags: - "Model checking proves my code is correct" — collapsing the model/code gap. - Treating it as a faster test suite — missing exhaustive over all interleavings. - Saying BMC "proves correctness" with no mention of bounds or the completeness threshold. - Not knowing safety needs reachability and liveness needs cycle detection + fairness. - Hearing "the checker passed" and accepting it — no instinct for vacuity or a too-small bound. - "Just throw more RAM at the state explosion" as the first move. - Confusing a counterexample with a flaky test (a counterexample is always real in the model).

Green flags: - Naming the distinction (exhaustive/sampled, model/code, safety/liveness, bug-finding/proof) before any algorithm. - Treating a counterexample as the feature — the exact failing schedule on a plate. - Asking "what are the fairness assumptions?" the moment liveness comes up. - Saying "model the design at RFC stage," and citing the AWS/TLA+ result. - Attacking state explosion structurally (shrink the model, symmetry, POR) before changing algorithm or hardware. - Stating the four ways a PASS can lie (vacuity, bound, abstraction, property) unprompted. - Placing model checking correctly between property-based testing and proof assistants.

Cheat Sheet¶

WHAT          Exhaustively check a FINITE MODEL against a TEMPORAL property.
              PASS ⇒ holds in the model (under assumptions, within bounds).
              FAIL ⇒ a COUNTEREXAMPLE: a concrete, replayable trace.

PROPERTY KINDS
  Safety   "nothing bad ever"   violated by FINITE prefix   ⇒ reachability search
  Liveness "something good       violated by INFINITE run    ⇒ cycle detection
            eventually"          (a LASSO)                   ⇒ needs FAIRNESS

TEMPORAL OPERATORS
  □ φ  always      ◇ φ  eventually      X φ  next      φ U ψ  until
  LTL: single timeline ("on all paths, X")
  CTL: + path quantifiers  A (all paths)  E (exists a path)   e.g. AG, EF
  mutual exclusion:        □ ¬(inCS1 ∧ inCS2)
  every request answered:  □ (request → ◇ response)

ALGORITHMS
  Explicit-state    enumerate states, hash visited      (SPIN)
    liveness        LTL → Büchi → product → NESTED DFS → lasso
  Symbolic / BDD    sets-of-states as boolean formulas  (SMV/NuSMV) — hardware
  Bounded MC        unroll k, hand to SAT/SMT           bug-finder unless ≥ threshold
  IC3 / PDR         inductive invariant via SAT, no full unroll
  CEGAR             abstract → check → refine on spurious counterexample

STATE EXPLOSION (state space is a PRODUCT ⇒ exponential)
  shrink model → symmetry reduction → partial-order reduction
              → symbolic/BMC → CEGAR → (more RAM / bitstate) last

A "PASS" CAN STILL BE WRONG IF:
  vacuity (premise never fires) · bound too small (k, or N=2) ·
  wrong abstraction (model ≠ system) · wrong property (verified the wrong thing)

PLACEMENT
  property-based testing  → real CODE, sampled inputs, in CI
  model checking          → DESIGN, all interleavings, once at design time
  proof assistants        → infinite-state, total proof, crown-jewel components

Summary¶

The bank reduces to four distinctions, repeated in costumes: exhaustive vs sampled, model vs code, safety vs liveness, bug-finding vs proof. Name the distinction first; the algorithm follows.
Fundamentals: model checking exhaustively explores a finite model's reachable states and interleavings against a temporal property, returning a counterexample (a concrete, always-real trace) on failure. Safety = "nothing bad ever" = reachability; liveness = "something good eventually" = cycle detection (a lasso) and needs fairness.
Temporal logic: LTL (□ ◇ X U, single timeline) vs CTL (path quantifiers A/E, branching futures); □¬(inCS₁∧inCS₂) for mutual exclusion, □(request → ◇response) for response/liveness.
Algorithms & explosion: explicit-state reachability and the automata/Büchi/nested-DFS lasso approach; symbolic/BDD for structured spaces; bounded MC (SAT/SMT, k-unrolling — bug-finder unless you hit the completeness threshold); IC3/PDR; and the mitigations for the inherently exponential, product-shaped state space — symmetry reduction, partial-order reduction, CEGAR.
Limits: you verify the model not the code (abstraction gap), it's finite/bounded, and a PASS can be vacuous, under-bounded, mis-abstracted, or against the wrong property — all decidable-but-expensive realities.
Practice: it pays off on concurrency, distributed protocols, and hardware — model the design at RFC stage; the AWS/TLA+ result is the canonical proof that practicing engineers catch deep bugs this way. Read counterexamples like a screenplay; place model checking between property-based testing and proof assistants.