From informal spec to checkable property: why a precise model catches bugs an English spec hides

How to read this document. Full notes for a 100-minute session, self-sufficient: every derivation is on the page, and the six parts are timed as they would run in the room. Where the text says Reproduce in Workbook §N, the companion notebook prints the exact digits quoted here. All workbook numbers are in-silico (toy models, fixed seed); the case studies are historical fact; the four lab incidents are real events from this research group's practice.

What this discipline is — in one sentence

Formal modelling is the discipline of writing down what a system must do so precisely that a machine can check whether it does it. Everything in this course is detail underneath that single sentence.

This is the opening week of FM505, and it assumes only the course prerequisites: basic logic, comfort reading state machines, and Python. Before any temporal logic or model checker appears, we ask one question: what does a precise specification buy you that a careful English paragraph does not? The answer comes from three directions at once. From history: some of the most expensive and most lethal engineering failures of the computer age were failures of specification, not of coding. From mathematics: the two great classes of correctness claims — safety and liveness — have provably different refutation logic, which dictates what a counterexample even looks like. And from this lab's daily practice: four times in the past year, a requirement that lived only as prose hid a bug or invited a misreading, and four times, restating it as a checkable property caught the problem mechanically. The workbook re-executes all four, in miniature, on transition systems a dozen lines of Python long.

Part 1 · The problem nobody ordered (0:00–0:15)

A machine that killed with software

Between June 1985 and January 1987, a radiation-therapy machine called the Therac-25, built by Atomic Energy of Canada Limited, massively overdosed six patients. Several of them died of the injuries. The machine had two modes: a low-current electron-beam mode, and a high-current X-ray mode in which the beam was supposed to pass through a metal target that spread and attenuated it. The accidents happened when the machine delivered the high-current beam without the target in place — raw, at roughly a hundred times the intended dose.

The immediate cause, reconstructed in Nancy Leveson and Clark Turner's 1993 investigation (the canonical case study of software safety, and your first item of further reading), was a race condition. If the operator entered the treatment data and then edited it quickly — within seconds, faster than the machine's setup tasks completed — one concurrent task read the edited values while another had already latched the old ones. The turntable and the beam current could end up in an inconsistent configuration that no one had ever written down as impossible, because no one had ever written down the set of possible configurations at all.

Three facts about Therac-25 matter for this course, and they are not the facts people usually reach for.

First, the code that killed was not new. It was substantially reused from the earlier Therac-6 and Therac-20 machines — where the same software fault existed but was masked, because those machines had hardware interlocks that physically prevented the dangerous configuration. The Therac-25 removed the hardware interlocks and trusted the software. The fault did not appear in the new machine; the specification of what the software had to guarantee changed, silently, and nobody re-derived the requirements.

Second, testing did not and could not have saved it. The race required a specific, fast sequence of operator edits, timed within seconds. The failure was not on any test plan because no one had enumerated the state space in which it lived. When a state is not representable in your description of the system, you cannot test for it, because you do not know it exists.

Third — and this is the point of the whole week — the failure was a specification failure before it was a coding failure. The safety requirement "the high-current beam shall never fire without the target in place" is a perfectly crisp statement. It is, as we will name it in a few minutes, a safety invariant over the machine's states. Nobody stated it as one. It existed as an assumption distributed across prose documents, hardware that no longer existed, and the heads of engineers who had moved on.

Hold that pattern. We will see it again over the Atlantic coast of French Guiana, inside an Intel floating-point unit, and on the surface of Mars — and then, at much lower stakes, in this lab's own simulation configs.

Most failures are spec failures

The uncomfortable claim of Week 1 is this: most software failures worth talking about are failures to decide what "correct" means, not failures to implement a decision correctly. The bug in the code is downstream of a hole in the spec. Leslie Lamport — whose temporal logic we meet in Week 3 and whose specification language TLA+ appears later today — has spent four decades making a version of this argument: the primary value of a formal specification is not the machine-checking, it is that writing it forces you to think precisely about the system above the level of the code, and that thinking is where the design errors are found. A specification, then, is not paperwork. It is the act of deciding what "correct" means — and deciding it early, while it costs a document edit instead of a recall.

Verification is not validation

Before we can do anything precise, one distinction that the literature is disciplined about and everyday speech is not. A model checker, in the standard definition, is a tool that verifies a system description against a specification — it answers whether the model you wrote satisfies the property you stated (wedyan2017_50ae ↗). That activity is verification: did we build the thing right, where "right" means "as specified"?

It answers nothing about whether the model resembles the world. That second question — validation, did we build the right thing — cannot be answered by any amount of logic, because it is a question about correspondence with reality, and reality is not a formal object. A protocol model can satisfy every property you state and still be a poor description of the deployed protocol; a crowd model can be internally impeccable and still walk like no human ever walked.

The trap to avoid, this week and always: a model checker proves that the model satisfies the property. It does not prove the system correct. The gap between model and system is validation's problem, it is closed by evidence rather than proof, and it never disappears. Therac-25 is precisely a validation gap wearing a verification costume: even a verified Therac-25 control program would have been verified against a spec that never mentioned the target position, because the hazard lived in a part of reality the model did not represent. This course spends eleven weeks sharpening verification precisely because that sharpening is cheap and mechanical — while flagging, every time, where validation quietly takes over.

Stop and convince yourself (concept check 1). A colleague says: "Our autopilot model passed 4,000 model-checked properties, therefore the autopilot is safe." Name the two distinct gaps in that inference. (One is the model–system gap: the properties were proved of the model, not the aircraft. The other is the spec-completeness gap: passing the 4,000 properties you thought of says nothing about the property you did not think of — the Therac-25 gap.)

Part 2 · A language for behaviour (0:15–0:30)

The words you need

A handful of terms recur all semester. Each is defined here in plain language; every one comes back in context.

• Specification (spec) — a statement of what a system should do. Informal specs are prose; formal specs are mathematical objects.
• Model — a simplified, precise description of a system's possible behaviours. This course's models are mostly transition systems: states plus arrows saying which state can follow which.
• Trace — one possible run of a model: a sequence of states s_0 s_1 s_2 \ldots following the arrows.
• Property — a predicate over traces: a yes/no question a machine can ask of any run.
• Verification — checking that an implementation or model meets its spec. "Did we build the thing right?"
• Validation — checking that the model corresponds to reality. "Did we build the right thing?"
• Invariant — a condition that must hold in every reachable state, such as "occupancy never exceeds capacity".
• Safety property — "nothing bad ever happens". Violated, if at all, by a finite trace.
• Liveness property — "something good eventually happens". Violated only in the limit; no finite prefix can refute it.
• Guard — a condition on a transition that forbids it from firing. Guards are how a model makes bad states unrepresentable.
• Lasso — the shape of a liveness counterexample in a finite-state system: a finite stem leading into a cycle that repeats forever.

Two of these — safety and liveness — carry the intellectual weight of the whole course. The distinction looks academic and is in fact intensely practical: it determines what kind of evidence can ever refute your claim, and therefore what kind of check you must build.

The object underneath: transition systems

Let us give the vague word "model" its mathematical body, because everything this semester is defined over it. A transition system is a triple

where S is a set of states (for us this week, finite or countable), S_0 \subseteq S is the set of initial states, and \rightarrow\; \subseteq S \times S is the transition relation: s \rightarrow s' means the system can move from s to s' in one step. Nothing more. No code, no time units, no probabilities yet — just "what states exist" and "which can follow which".

A trace (or run) of \mathcal{T} is a sequence \sigma = s_0 s_1 s_2 \ldots with s_0 \in S_0 and s_t \rightarrow s_{t+1} for every t. Write \mathrm{Traces}(\mathcal{T}) for the set of all of them. A state s is reachable if some trace visits it.

And now the definition that makes the whole course possible. A property P is simply a set of traces — the acceptable ones. The system satisfies P when

Read that inclusion slowly, because it is the entire subject in one line: every behaviour the model can produce lies inside the set of behaviours the spec permits. Verification, from here to Week 12, is the study of ways to establish (or refute) one subset relation. A counterexample is a witness to its failure: a single trace \sigma \in \mathrm{Traces}(\mathcal{T}) \setminus P. Much of the practical power of model checking comes from the fact that the tool does not just say "no" — it hands you that trace, and the trace is a story you can read.

The cheapest formal method in existence

You do not need temporal logic to start benefiting from this discipline. The lightest formal spec is a typed schema: an explicit, machine-readable definition of which inputs are well-formed at all. And here the course switches from history to this lab's own practice, because the first two of our four lab incidents were caught by exactly this.

Consider a requirement the lab actually wrote, in prose, for a simulation scenario: "after dwelling in a room, the agent walks to its next target." An author transcribed this into a configuration file and — reasonably, reading the prose — named the timing field after_dwell. The schema's name for that field is after. Nothing in the English sentence distinguishes the two; both are faithful transcriptions of the same prose. The configuration was wrong, and prose review would not have caught it, because the prose is exactly what the author implemented.

What caught it was the typed schema: the scenario validator rejected the config at submission time, before any simulation compute was spent. The same validator caught a subtler defect in the same authoring loop: a target written as {kind: exit}. That value is perfectly legal in one slot of the schema (as a state intent — "this agent intends to leave") and illegal in another (as a linear-leg target — a leg must aim at a room, door, or waypoint). No syntax highlighter flags it; only a schema that knows which values are legal where can. The workbook's Section 1 reproduces both rejections in about thirty lines of Python and prints the tally: 2 of 3 example configs rejected at zero compute cost. Reproduce in Workbook §1.

This is the cheapest formal method in existence, and it already exhibits the course's central move: a wrong configuration was not detected so much as made unrepresentable. The set of valid configurations was defined precisely, and everything outside it stopped existing as an input. Hold onto that phrase — wrong states unrepresentable — because the rest of the week generalises it from configurations to behaviours.

An industrial aside: types as certified specs

The idea scales far past config files. In avionics, the certification standard DO-178C (2011) governs airborne software, and its formal-methods supplement DO-333 explicitly allows formal analysis to replace certain categories of testing as certification evidence — a regulator agreeing, in writing, that a machine-checked property can stand where a test campaign once stood. The language most associated with that world is SPARK, a contracts-annotated subset of Ada whose toolchain proves, among other things, the absence of runtime errors — no overflow, no out-of-range access — for the whole program. Note the shape of the guarantee: not "we tested for overflow and found none", but "overflow is unrepresentable in any execution". It is the schema idea, industrialised. Surveys of how these techniques reach this lab's application domain — IoT stacks and their protocols — are in krichen2023_e60e ↗ and hoferschmitz2020_1b73 ↗.

Stop and convince yourself (concept check 2). The schema rejected {kind: exit} in one slot and accepted it in another. Express this in transition-system vocabulary: what plays the role of S, and what did the schema change — the states, or the transition relation, or something before either? (Something before either: the schema defines which configurations exist as inputs at all — it shrinks the space of representable models, before any state or transition is generated. The same value in two slots is two different points of that space, and only one of them survives.)

Part 3 · Safety: nothing bad ever happens (0:30–0:52)

The shape of the claim

Almost every prose requirement you will ever write decomposes into two classes with fundamentally different refutation logic. We take them in turn, and we take safety first because it is the class your intuition already owns.

Informal spec: "the room never holds more than 12 people."

Checkable property: over every trace s_0 s_1 s_2 \ldots of the occupancy process,

In plain words: at every step of every run, the occupancy count stays at or below twelve. One bad step anywhere breaks it.

Now the formal definition, because it does the work. A property P is a safety property when every violating trace announces its violation in finite time: if \sigma \notin P, there is a finite prefix \sigma[0..k] — a bad prefix — such that no infinite extension of \sigma[0..k] lies in P. The bad prefix is a complete, self-contained refutation. If occupancy hits 13 at step 26, the argument is over: nothing at step 27 or later can repair it. This finiteness is why safety is the easy class to check: run the system — or, from Week 4, exhaustively explore its state space — and watch for the first bad state. The checker's job is a search for a short certificate.

Building the model on the board

Let us build the occupancy model honestly, symbol by symbol, because it is the first real model of the course. The state is a single integer, the current occupancy: S = \{0, 1, 2, \ldots\}, S_0 = \{0\}. Each time step, two things happen:

• with probability p_a = 0.9, one person arrives;
• each current occupant independently departs with probability p_\ell = 0.07.

So if A_t \sim \mathrm{Bernoulli}(p_a) is the arrival indicator and D_t \sim \mathrm{Binomial}(\mathrm{occ}_t,\, p_\ell) counts departures, the update is

Every symbol is now defined: p_a and p_\ell are per-step probabilities (dimensionless), A_t \in \{0,1\}, D_t \in \{0, \ldots, \mathrm{occ}_t\}, and occupancy can never go negative. This is a stochastic transition system — the arrows carry probabilities — but the safety property ignores the probabilities entirely: it asks only whether a trace visiting \mathrm{occ} = 13 exists.

Deriving trouble before running anything

Here is the habit this course wants to build: before you simulate, interrogate the model analytically. Take the conditional expectation of the update given the current state \mathrm{occ}_t = n:

Define the drift d(n) = p_a - n\,p_\ell: the expected change in occupancy per step, as a function of where you are. Set it to zero and solve:

For n < n^\* the drift is positive (the room fills), for n > n^\* it is negative (the room drains): the process is mean-reverting around n^\* \approx 12.9. And 12.9 > 12. One line of algebra has told us the process lives above the capacity line: the invariant is not merely at risk, it is doomed. Because the chain has positive probability of an arrival with no departures from any state n \le 12, the state 13 is reachable from everywhere below it, and a chain that hovers around 12.9 forever will visit 13 not occasionally but almost surely — and quickly.

The workbook checks the invariant over 200 generated traces of 300 steps, and the derivation's prophecy lands in full: all 200 of 200 unguarded traces violate the invariant, with the median first violation arriving at step 29. Each violation is a finite witness: a specific trace, a specific step, occupancy 13. (In-silico numbers, seed 7.)

The guard: removing the bad state from the universe

Then one guard is added to the transition relation: an arrival is rejected when the room is at capacity. Formally, the transition on A_t becomes conditional — \mathrm{occ}_{t+1} = \mathrm{occ}_t + A_t \cdot \mathbf{1}[\mathrm{occ}_t < 12] - D_t. The result is not that violations become rare. It is that 0 of 200 traces violate — and no trace ever could, because the transition relation no longer contains any arrow leading to occupancy 13. The reachable state space is now \{0, \ldots, 12\} by construction; the proof is an induction so short it fits in a breath: occupancy starts at 0, and no transition increases it past 12. The bad state is unrepresentable. This is the schema idea again, lifted from configurations to behaviours: the guard does not catch the bad state, it removes it from the model's universe.

Reproduce in Workbook §2 — including the 200/200 and 0/200 counts and the median first-violation step of 29.

Notice what just happened methodologically, because it is the deepest lesson of the section. We made three different kinds of correctness argument about the same invariant, in increasing order of strength: a heuristic derivation (the drift says trouble), statistical evidence (200 sampled traces, all violating), and a proof (the guarded system cannot represent occupancy 13, by induction on the transition relation). The whole apparatus of Weeks 4–10 exists to move claims from the middle category to the third.

Case study: Ariane 5, flight 501 (4 June 1996)

Thirty-seven seconds after its maiden launch, the European Space Agency's Ariane 5 veered off course and self-destructed, taking its payload of four Cluster science satellites with it. The inquiry board, chaired by Jacques-Louis Lions, delivered one of the most instructive failure reports ever written.

The proximate cause was a single arithmetic operation in the inertial reference system: a conversion of a 64-bit floating-point value — a quantity related to the rocket's horizontal velocity — into a 16-bit signed integer. On Ariane 5's trajectory the value exceeded what 16 bits can hold; the conversion raised an unhandled operand error; the inertial reference computer shut down. Its backup, running identical software, had shut down for the identical reason an instant earlier. The guidance system, flying blind, commanded the fatal deviation.

The specification lesson is sharper than "an overflow happened". That conversion had been analysed — for Ariane 4. On Ariane 4's gentler trajectory, engineers had satisfied themselves the value physically could not exceed the 16-bit range, and, to save processor budget, deliberately left the conversion unprotected. The code was then reused on Ariane 5, whose trajectory was different — and the assumption did not travel with the code. The overflow was not a coding error: the code did exactly what was written, on the rocket it was written for. It was a specification error — an environmental precondition that was true of one system and silently false of its successor. To close the wound: the alignment function computing the value was not even needed after liftoff; it kept running into flight as a convenience inherited from Ariane 4 operations.

Note the family resemblance to Therac-25: reused component, changed environment, unstated assumption. In our vocabulary: a safety property ("the converted value always fits in 16 bits" — an invariant, refuted by one finite trace 37 seconds long), whose proof was valid for one model of the environment and was never re-checked when the environment changed. Range analysis of exactly this kind is routine and automated today — one of the things SPARK's runtime-error proofs discharge mechanically.

Case study: the Pentium FDIV bug (1994)

In the summer of 1994, Thomas Nicely, a mathematics professor computing sums of reciprocals of twin primes, noticed his Pentium-based machines returning slightly wrong divisions. The cause, once the story became front-page news: the Pentium's floating-point division used a table-driven algorithm (radix-4 SRT division), and five entries of the lookup table had been omitted — cells the designers' analysis had concluded could never be accessed. For most operand pairs the division was exact; for rare specific pairs, the quotient was wrong from about the fifth significant digit.

Two things make this a Week 1 case study. First, the error class: like Ariane, a "this case cannot occur" argument, made informally, was wrong — and everything downstream was built on it. Second, the aftermath. After first offering replacements only to users who could demonstrate need, Intel yielded to public pressure, replaced unconditionally, and took a charge of approximately 475 million dollars against earnings. The engineering response outlasted the financial one: Intel, and the industry with it, invested permanently in formal verification of arithmetic hardware — machine-checked proofs, by theorem provers and symbolic methods, that division and square-root meet the IEEE-754 specification for all inputs, not the inputs a test plan sampled. Divider bugs of the FDIV class have not recurred in shipped silicon since. When someone tells you formal specification is academic, the counterexample is inside the machine they said it on.

Stop and convince yourself (concept check 3). "The converted value always fits in 16 bits" was proved for Ariane 4 and failed on Ariane 5. In the verification/validation vocabulary of Part 1, which kind of failure is that, exactly? (Verification was sound: the proof was correct for the stated environment model. The environment model itself — the trajectory envelope — no longer corresponded to reality when the code moved to Ariane 5. A validation failure of an assumption, invalidating a verification that was never re-run.)

Part 4 · Liveness: something good eventually happens (0:52–1:16)

The inversion of refutation

Informal spec: "every agent eventually exits the building."

Checkable property: for every trace,

In plain words: for each agent there is some future step at which it has left. The spec names no deadline — only "eventually".

Now the refutation logic inverts. No finite prefix can refute a liveness property: after any finite number of steps, the optimist can always say "just wait a little longer." Formally, a property P is a liveness property when every finite sequence of states can be extended to some infinite trace in P — no finite prefix is ever a lost cause. Compare that, symbol for symbol, with the safety definition: safety says every violation has a finite bad prefix; liveness says no finite prefix is bad. The two definitions are mirror images, and they are the two ends of a genuine theorem. Alpern and Schneider (1985) proved that every linear-time property is the intersection of a safety property and a liveness property — the decomposition is not a taxonomy of convenience but an exact algebra. The distinction itself is older: Lamport (1977) introduced safety and liveness to split program correctness into its two classical halves — partial correctness ("if it answers, the answer is right": safety) and termination ("it answers": liveness).

The practical consequence of "no finite refutation" is the shape of the counterexample. Verifying liveness requires reasoning about nonterminating, infinite executions (alur1999_8e22 ↗). An infinite object cannot be printed. But for a finite-state system there is a saving grace: any infinite trace over finitely many states must eventually revisit a state, so a liveness counterexample can always be reported as a lasso — a finite stem leading into a cycle that the run then repeats forever, never reaching the good state. The lasso is the finite name of an infinite failure, and it is what every model checker from Week 4 onward will hand you when liveness breaks.

Variant A: a real confound, miniaturised

The workbook makes this concrete with a looping agent state machine that reproduces, in miniature, a real experimental confound from the lab's simulation work — our third lab incident. Variant A has states ENTER -> DWELL -> WALK -> DWELL -> ..., where the schedule's last leg points back to its first — a plausible authoring slip.

How do we check it? Not by simulating — by reachability, the first genuine verification algorithm of the course. Define the set of states reachable from the start as the least set R satisfying

— start from the initial state, keep adding one-step successors until nothing new appears. Because S is finite, this fixpoint computation terminates; the ten-line worklist implementation in the workbook is the entire algorithm. For variant A it returns R = \{\mathrm{ENTER}, \mathrm{DWELL}, \mathrm{WALK}\}: EXIT is unreachable, and the lasso is the stem ENTER -> DWELL followed by the cycle DWELL -> WALK -> DWELL. This is a proof about the model, obtained without simulating a single step. Simulation agrees with the graph argument: 100% of 200 agents are still inside at the 500-step horizon (in-silico). In the lab's original incident this exact shape — looping agents that never left — silently distorted headcounts until the loop was found.

Pause on the asymmetry, because it previews Week 4: the reachability argument examined four states and settled the question for all runs of any length; the simulation examined 100,000 agent-steps and settled it only for the runs it happened to sample. That trade — exhaustive analysis of a small model over sampling of a large one — is the entire business case for model checking.

Variant C: "almost surely" is not "surely"

A third variant, C, sharpens the "no finite refutation" point from the other side. Give each agent a small per-step exit probability p = 0.005, independently each step. Then the time to exit is geometric, and the probability an agent is still inside at step t is the survival function

Derive the number before looking: \ln(0.995) \approx -0.005013, so (0.995)^{500} = e^{500 \ln 0.995} \approx e^{-2.506} \approx 0.0816. Theory says 8.16% of agents remain at the 500-step horizon; the workbook's 200 sampled agents give 10.0% remaining, against the theoretical 8.16% — sampling noise of exactly the size you would expect from 200 draws (in-silico). The survival curve decays geometrically and never quite reaches zero.

Here liveness holds — with probability 1, every agent eventually leaves, since \lim_{t\to\infty}(1-p)^t = 0. And yet no finite observation window certifies it: at any horizon some agents are expected to remain, and a skeptic watching the building can never distinguish "will leave, hasn't yet" from "will never leave". The claim is genuinely about the limit — which is why liveness needs different machinery, and why probabilistic model checking (Week 10) is its own discipline.

Reproduce in Workbook §3 — the reachability proof, the 100% stuck fraction, and the 10.0% vs 8.16% comparison.

The engineering fix: buy back checkability with a bound

Pure liveness is expensive to check precisely because its counterexamples are infinite. The standard engineering response is to strengthen "eventually" into "within T" — a move the real-time verification literature formalises as bounded liveness, the class of property that tools like UPPAAL check natively (alur1999_8e22 ↗).

And here is the observation that ties the whole lecture together, so it gets its own paragraph. Bounded liveness is a safety property. "Every agent exits within 150 steps" is violated by a finite prefix — namely, any prefix that reaches step 151 with an agent still inside. By naming a deadline you have moved the claim from the hard class to the easy class: the infinite counterexample became a finite witness, the lasso became a bad prefix, and every safety technique of Part 3 applies again. The price is that you must defend the bound itself — a validation question: is 150 steps actually acceptable in reality? The mathematics cannot pick T for you.

The lab's version of this move is the time_after(T) exit guard, and it is the fourth real incident this lecture re-derives — the repair of variant A's confound. When the looping-agent bug was found, the fix was not to hunt down every possible cyclic schedule. It was a timeout guard: once an agent's elapsed time exceeds a threshold, its next transition is forced to EXIT. Variant B of the workbook implements exactly this with a threshold of T_{\text{guard}} = 120 steps and dwell legs of at most 30 steps. The consequence is provable by inspection: the guard can fire no later than step 120, and the agent can then be mid-dwell for at most the maximal dwell length, so no agent remains past

Simulation confirms the proof — 100% of agents exit, the latest at step 148, inside the bound of 150 (in-silico). Headcount is matched by construction: everyone who enters, exits, not because the schedules were audited but because the transition relation no longer permits an infinite stay.

Reproduce in Workbook §3 — the exit-step histogram and the 148-versus-150 bound check.

Notice the pattern across all three fixes so far: schema, admission guard, timeout guard. In each case the informal spec said "X should not happen", and the formal move was not to test for X harder but to redefine the object so that X has no representation. That is the week's thesis in one line: a formal spec makes wrong states unrepresentable.

Case study: Mars Pathfinder (July 1997)

Days after NASA's Pathfinder lander began operating on Mars, the spacecraft started resetting itself, each reset losing a portion of the sol's data. The fault, diagnosed at the Jet Propulsion Laboratory, has become the textbook instance of priority inversion.

Pathfinder's software ran on a real-time operating system with fixed-priority scheduling. A high-priority bus-management task shared a mutex with a low-priority, infrequent meteorological task. The lethal interleaving: the low-priority task acquires the mutex; medium-priority tasks — with no interest in the mutex at all — preempt it and run at length; the high-priority task blocks on the mutex, waiting on a task that cannot run. A watchdog timer, observing the missed deadline, concluded the system was hung and reset it. In our vocabulary this is a liveness failure: "the bus-management task eventually runs" — violated not by any bad state but by an unbounded wait, an interleaving in which the good thing is postponed forever. Exactly the class of property no snapshot can refute, and exactly what temporal-logic model checkers search for as a lasso.

Two codas make the story canonical. First, the diagnosis: JPL engineers reproduced the failure on a ground replica by replaying execution traces with instrumentation enabled — the flight software had shipped with tracing support, and that decision saved the mission. The fix was a single flag: the operating system's mutexes supported priority inheritance (the low-priority holder temporarily inherits the blocked task's priority); it had simply been left disabled, and was enabled by patching the running spacecraft from Earth. Second, the pedigree: priority inversion had been described and solved in the real-time-systems literature years earlier (the priority-inheritance protocols of Sha, Rajkumar, and Lehoczky), and interleavings of precisely this shape are what model checking explores exhaustively and test runs happen to miss. The broader lesson: concurrency bugs live in the space of interleavings, the one space human review is worst at searching.

Stop and convince yourself (concept check 4). Classify each as safety, liveness, or bounded liveness (hence safety): (a) "the two inertial units never disagree by more than 1 degree"; (b) "every request is eventually acknowledged"; (c) "every request is acknowledged within 200 ms"; (d) "the mutex is never held by two tasks at once". (a: safety — finite trace showing a disagreement refutes it. b: liveness — refutable only by an infinite wait, reported as a lasso. c: bounded liveness, hence a safety property — a 201 ms silent prefix refutes it. d: safety — the classic mutual-exclusion invariant.)

Part 5 · Properties beyond programs (1:16–1:32)

Specifying a research claim: the defeater clause

The discipline of "state the property before you look" is not limited to programs, and this lab applies it to its own science. Every living hypothesis in the lab's knowledge base carries defeater clauses: pre-stated, falsifiable conditions of the form "if X is observed, the claim falls." A defeater is a property over future evidence, locked in before the evidence exists — precisely what a pre-registered analysis does for a statistical study. Its value is the same as the schema's: it removes the discretion to reinterpret an awkward outcome after the fact. A hypothesis without a defeater is prose; a hypothesis with one is checkable. The parallel to Popper's demarcation line is exact: a claim no observation could refute is not an empirical claim at all. A defeater clause is falsifiability made machine-readable.

TOST, derived from scratch

Equivalence testing deserves the week's closing worked example for two reasons: it is the purest statistical instance of "the property is declared before the data", and the lab has a documented incident — the fourth and last — of the misreading it exists to prevent.

The scientific question: two arms A and B (two pipelines, two sensors, two model variants) — are their mean outcomes equivalent for practical purposes? Classical null-hypothesis testing cannot answer this: failing to find a difference may just be evidence of small samples. Equivalence must be stated as its own property, with its own margin \Delta, declared in advance:

where \mu_A, \mu_B are the true (unknown) means. The two one-sided tests (TOST) procedure checks it as follows. Estimate the difference \hat d = \bar{y}_B - \bar{y}_A from samples of sizes n_A, n_B with sample variances s_A^2, s_B^2. Its standard error, allowing unequal variances (Welch),

with degrees of freedom from the Welch–Satterthwaite approximation. Now split the negation of the property into its two one-sided halves and attack each:

Each is an ordinary one-sided t-test at level \alpha. TOST passes — equivalence is certified — only if both nulls are rejected; the overall p is the larger of the two. There is a picture worth more than the algebra: rejecting both one-sided tests at level \alpha is exactly the condition that the 100(1-2\alpha)\% confidence interval of the difference — for \alpha = 0.05, the 90% CI — sits entirely inside (-\Delta, +\Delta). The margin is the property; the interval is the evidence; the check is set containment. You have seen this shape before, this very hour: \mathrm{Traces}(\mathcal{T}) \subseteq P.

The asymmetry is the entire point:

• A pass certifies the property: the data support equivalence within the declared margin.
• A fail proves nothing. It does not demonstrate a difference. The usual cause is simply an interval too wide for the margin — insufficient data, not a detected effect.

The executed verdicts

The workbook runs both outcomes on synthetic data whose ground truth is known to be equivalent (true difference 0.01, margin \Delta = 0.05). The adequately powered scenario (n = 120 per arm) yields a difference of +0.022 with 90% CI [−0.001, +0.044] and TOST p = 0.0205: equivalence certified within the margin. The underpowered scenario (n = 8 per arm), drawn from the same equivalent distributions, yields a difference of −0.063 with 90% CI [−0.154, +0.029] and TOST p = 0.5943: no conclusion (both in-silico). Reading that second result as "the arms differ" — or a failed TOST anywhere as "the test confirmed the difference" — is the documented error this section exists to teach against. The property was |\mu_B - \mu_A| < \Delta; a fail means the property was not certified, never that its negation was.

Reproduce in Workbook §4 — including both intervals and both p-values.

Case study: Amazon and TLA+ (2011–2015)

If the week so far suggests that formal specification is for rockets and radiation machines, the counterexample is the most commercial software on Earth. In a 2015 Communications of the ACM article, Chris Newcombe and colleagues described how engineering teams at Amazon Web Services had been using Lamport's specification language TLA+ since 2011 on the systems underneath S3, DynamoDB, and other core services. The headline finding: model checking their specifications found subtle, serious bugs — one requiring a trace of 35 high-level steps to manifest — that had survived design review, code review, and testing, and that the engineers judged no plausible test campaign would have reached. Thirty-five steps of specific interleaving is not a place human imagination visits; exhaustive search visits it routinely. Their second finding echoes Lamport's argument from Part 1: writing the spec was valuable independent of checking it — precision surfaced design ambiguities early, and the spec became the durable documentation of how the system actually works. And their third finding removes the standard excuse: working engineers, not verification specialists, learned enough TLA+ to write useful specs in weeks.

Case study: seL4 — the far end of the spectrum

Finally, the outer limit of what "verified" can mean today. seL4 (Klein et al., 2009, and a decade of work since) is an operating-system microkernel — roughly ten thousand lines of C — with a machine-checked proof, in the Isabelle/HOL theorem prover, that the C implementation refines its formal specification: every behaviour of the code is a behaviour the spec allows. The proof effort ran to many person-years — far more than the effort of writing the kernel itself; later work extended the guarantee down to the compiled binary and up to security properties. seL4 flies today in safety- and security-critical systems.

Its place in this lecture is calibration. Between the thirty-line schema validator at one end and seL4 at the other runs a single continuous spectrum — schema checks, contracts, property-based tests, model checking, full refinement proof — trading effort for strength of guarantee. Every point on it is the same activity: deciding what correct means, writing it down precisely, and letting a machine hold you to it. This course lives in the middle of that spectrum; know that the far end exists, is real, and ships. For the proof-oriented end in a modelling idiom, see Event-B and its Rodin toolset (abrial2010_b911 ↗).

Stop and convince yourself (concept check 5). Your TOST fails with 90% CI [−0.11, +0.02] against margin ±0.05. A colleague writes "the arms were shown to differ." Give the two-sentence correction, and say what would actually license a difference claim. (The fail certifies nothing: the interval is simply too wide for the margin — compatible with equivalence and with difference alike. A difference claim needs its own test — e.g. the CI excluding zero — which this interval also does not support.)

Part 6 · The week in one picture (1:32–1:40)

Four property classes, each executed against the workbook's own traces:

Reproduce in Workbook §5 — the panel text is generated from the executed numbers, so figure and notebook cannot disagree.

The columns are ordered by refutation cost. A safety violation is one bad state. A liveness violation is an infinite object, which only a finite-state argument (the lasso) makes reportable. Bounded liveness buys back finite refutability by paying with a deadline — and thereby becomes a safety property. And the TOST column is the statistical analogue: a property with an asymmetric verdict, where only one of the two outcomes carries information.

What you can now do

Concretely, after this session and the workbook, you can:

• classify a prose requirement — safety, liveness, or bounded-liveness-hence-safety — and state what its counterexample looks like (bad prefix, lasso, deadline miss);
• write a requirement as an executable predicate over traces and check it against generated runs;
• interrogate a stochastic model analytically before simulating (the drift calculation), and say which of the three argument types — heuristic, statistical, proof — a result is;
• make a bad state unrepresentable with a schema or a guard, and prove a resulting bound by inspection;
• read a TOST verdict correctly, and attach a defeater clause so a claim is falsifiable before the data arrive;
• and diagnose, in each historical failure of this lecture, where the specification hole was, independent of where the code broke.

Where this goes

This course's throughline is that a model you can check beats a description you can only argue about, and this week supplied the raw distinctions the rest of the semester builds on. The immediate next steps:

• Week 2 — logic refresher. Every predicate this week was written in ad-hoc Python. Week 2 rebuilds the substrate properly: propositional and predicate logic, satisfiability, and what a proof is.
• Week 3 — temporal logic. The quantifiers "\forall t" and "\exists t" over traces get their own notation: LTL and CTL. The occupancy invariant becomes \mathbf{G}\,(\mathrm{occ} \le 12), the exit property becomes \mathbf{F}\,\mathrm{EXIT}, and the informal words "always" and "eventually" stop being informal.
• Week 4 — model checking. This week sampled 200 traces and got lucky that the bugs were dense; the reachability argument of variant A was a first taste of doing better. Model checking replaces sampling with exhaustive exploration of the state space — every reachable state, every cycle — and meets its own enemy, state-space explosion.

Further down the arc, the lab's MQTT stack becomes the running example: published work has model-checked MQTT itself, expressing deadlock-freedom as a safety formula and delivery as liveness, which is exactly the Week 8 exercise (houimli2017_4680 ↗; see also the incremental Maude-based treatment in rodrguez2019_cc22 ↗). Petri nets (Week 6) and timed automata (Week 7) extend the state-machine vocabulary to concurrency and real time (murata1989_d3ec ↗; alur1999_8e22 ↗).

One caution travels with us the whole way, stated once more because everything this course proves is conditional on it: model checking proves that the model satisfies the property. Whether the model deserves your trust is validation's question, and formal methods sharpen it without ever answering it for you.

Exam-style questions

Attempt these before looking at the sketches. Each is answerable from this week's material alone.

Q1 (classification). Classify each requirement as safety, liveness, or bounded liveness, and describe the exact shape of a counterexample to it: (a) "no two trains ever occupy the same track segment"; (b) "every buffered message is eventually delivered"; (c) "the pump shuts off within 5 s of a leak signal"; (d) "the counter is monotonically non-decreasing".

Sketch: (a) safety; counterexample = finite trace ending in a state with two trains on one segment. (b) liveness; counterexample = infinite trace (lasso) on which some message is buffered on the stem and never delivered on the cycle. (c) bounded liveness, hence safety; counterexample = finite trace containing a leak signal followed by 5 s without shutoff. (d) safety; counterexample = finite trace with one decreasing step. Full marks require the counterexample shapes, not just the labels.

Q2 (drift derivation). A queue admits one job per step with probability 0.6; each queued job completes with per-step probability 0.05. The requirement is "the queue never exceeds 10". Derive the drift, find its zero, and predict whether the invariant survives. What single change to the transition relation enforces it by construction?

Sketch: d(n) = 0.6 - 0.05n; n^\* = 12 > 10, so the process hovers above the cap and the invariant fails almost surely. Guard: reject admissions when n = 10; then reachable states are \{0,\ldots,10\} by induction and the invariant holds by construction.

Q3 (reachability and lassos). For the FSM with edges ENTER→A, A→B, B→A, B→C, C→C, initial state ENTER and goal C: compute the reachable set, state whether "eventually C" can be violated, and if so exhibit the lasso.

Sketch: Reach = {ENTER, A, B, C}: C is reachable, so the property is not unsatisfiable — but "eventually C" is still violated by the lasso with stem ENTER→A and cycle A→B→A, which never takes the B→C edge. Reachability of the goal is necessary but not sufficient for liveness: fairness (Week 9) is exactly what rules such lassos in or out.

Q4 (bounded liveness is safety). Prove, from the definitions, that "every agent exits within 150 steps" is a safety property, and explain what is gained and what must now be defended.

Sketch: Any violating trace has an agent inside at step 151; the prefix up to step 151 is a bad prefix — no extension can repair it, since the deadline has already passed. Hence every violation has a finite bad prefix: safety. Gained: finite refutability, monitorable at runtime, checkable by state exploration. To defend: the choice of 150 — a validation question about the world, not a theorem.

Q5 (TOST asymmetry). Two TOST runs against margin Δ = 0.05: (i) n = 120/arm, 90% CI [−0.001, +0.044]; (ii) n = 8/arm, 90% CI [−0.154, +0.029]. State each verdict and what may be concluded. A report summarises (ii) as "arm B underperforms arm A". Correct it.

Sketch: (i) CI ⊂ (−0.05, +0.05): equivalence certified within the margin. (ii) CI exceeds the margin on both sides: no conclusion — the property was not certified, and nothing about its negation follows. The summary is wrong twice over: a failed TOST is not a difference claim, and the CI for (ii) includes zero, so even a difference test would not support it. The honest sentence is "the data are insufficient to certify equivalence within ±0.05."

Q6 (essay). "Therac-25 and Ariane 5 were both reuse failures, not specification failures." Argue for or against, using the vocabulary of this week. A strong answer will locate, for each incident, the property that was never stated formally, classify it, and identify the environmental assumption that changed between the original and reusing system.

Sketch: Against, with nuance: reuse was the mechanism, but what failed to travel was the unstated spec. Therac-25: safety invariant "high current implies target in place" — enforced by hardware in the predecessors, never stated as a software obligation. Ariane 5: safety invariant "value fits in 16 bits" — proved under Ariane 4's trajectory envelope, invalidated by the new vehicle. In both cases reuse was safe conditional on an assumption only a written spec could have carried across; the failure was that the condition existed nowhere a machine or a review could check.

Further reading

Annotated; the wiki-linked items are in the course vault, the rest are classics to find in any library.

• Alur (1999) — Timed Automata. The automata-theoretic account of safety versus liveness (liveness requires reasoning over infinite executions), timed guards, and the tool landscape including UPPAAL's safety and bounded-liveness checking. Background for Weeks 7 and 9. alur1999_8e22 ↗
• Wedyan et al. (2017) — Domain analysis of formal model checking tools. A survey of model checkers as tools that verify a system description against a specification; useful for the Week 4 tooling landscape. wedyan2017_50ae ↗
• Houimli et al. (2017) — Formal specification, verification and evaluation of the MQTT protocol in the Internet of Things. Models MQTT with probabilistic timed automata and checks reachability, safety (deadlock-freedom), and liveness in UPPAAL SMC — the published counterpart of this course's Week 8 running example, including a first sighting of state-space explosion. houimli2017_4680 ↗
• Rodríguez et al. (2019) — Formal Modelling and Incremental Verification of the MQTT IoT Protocol. The rewriting-logic (Maude) route to the same protocol — a useful contrast in modelling idiom for Week 8. rodrguez2019_cc22 ↗
• Murata (1989) — Petri nets: properties, analysis and applications. The classical survey of the Week 6 formalism: concurrency, tokens, and reachability analysis. murata1989_d3ec ↗
• Krichen (2023) — A Survey on Formal Verification and Validation Techniques for Internet of Things. Where the week's verification/validation distinction meets the lab's application domain. krichen2023_e60e ↗
• Abrial et al. (2010) — Rodin: an open toolset for modelling and reasoning in Event-B. The proof-obligation end of the spectrum sketched in Part 5. abrial2010_b911 ↗
• Leveson & Turner (1993) — An Investigation of the Therac-25 Accidents. IEEE Computer. The canonical software-safety case study; read it in full once in your career, this week being a good week.
• Lions et al. (1996) — Ariane 5 Flight 501 Failure: Report by the Inquiry Board. Short, readable, and devastating; the primary source for Part 3's account.
• Lamport (1977) — Proving the Correctness of Multiprocess Programs. IEEE TSE. The paper that introduced the safety/liveness split as partial correctness versus termination.
• Alpern & Schneider (1985) — Defining Liveness. Information Processing Letters. The exact definitions used in Parts 3–4 and the decomposition theorem: every property is a safety property intersected with a liveness property.
• Newcombe et al. (2015) — How Amazon Web Services Uses Formal Methods. CACM 58(4). The industrial-adoption case study of Part 5: the 35-step bug, the weeks-not-careers learning curve, specs as documentation.
• Klein et al. (2009) — seL4: Formal Verification of an OS Kernel. SOSP. The far end of the guarantee spectrum: machine-checked functional correctness of a running microkernel.