Harness First
Build the model, the oracle and the fault injector before the application, and see what they find
Table of Contents
- Overview
- A page nobody owns alone
- The harness, in the order it was built
- Who may read what
- What it found that a finished application would hide
- A checker that shares the code sees nothing
- A rule the model implied and nobody wrote
- The specified model could not be checked
- Faults surface where the customer stands
- Wrong is not the same as shown wrong
- Some rules can only be checked on the server
- Faults in the page itself
- Green can mean never tried
- Every live fault, every layer that could see it
- A note on screenshots
- What it took, and what it does not cover
- When to build the harness before the application
- Limits
Overview
A finished application hands you code. It does not hand you a way to tell whether your checks would notice that code going wrong. This note builds a small shop the other way round: the model, the oracle, the invariants, the fault injector and the drivers came first, and the store and the page came after. Then fifteen faults were planted on purpose, most of them while it ran.
The shop is Bestiary Books, which sells books certified readable by household monsters. A customer picks a creature through a cascading selector (year, genus, species, attributes), searches, opens a book, and saves the creature to their Menagerie. Every book is badged fits, no-fit or unknown for that creature.
A clean frame from the browser explorer. The index is one version behind the catalogue; a saved hydra whose species was removed is struck through, and its Activate button is disabled. Both are correct behaviour, and both are states a test has to expect.
The design and the method came from Live mutants; the reasons to build this before the application are in When hardening comes due.
A page nobody owns alone
Four parties change what the page shows, and only one of them is the customer.
| party | what it does | why it is hard to test afterwards |
|---|---|---|
| catalogue | rewrites fit rules, withdraws and restores books, every 1.5 s | each change is a new version; a bug shows only for some creatures |
| indexer | brings the search index up to the catalogue, up to two versions at a time | the list page reads the index, which lags; stale and wrong look alike |
| taxonomy | adds and removes species, every 6 s | a removal can invalidate a selection or a saved creature mid-session |
| customer | selects, searches, opens details, saves (Bombadil, a property-based browser explorer) | the only party a UI test drives; the other three move underneath it |
The list page is the product of the customer's selection and the index, never the catalogue. Given only the finished application, you could click through it, see sensible badges, and learn nothing about whether a lagging index, a vanished species or a misread fit rule would be caught.
The harness, in the order it was built
Each layer exists before the thing it checks, so nothing it says was shaped to fit the code.
- Model. A TLA+ specification of the whole shop: catalogue versions, index lag, taxonomy changes, the selection cascade, the list, the detail page and the Menagerie. TLC checked it exhaustively before any store code existed.
- Oracle. The checker's own statement of the rules, written from the model. It never calls the store's domain code, so a bug there cannot also change the answer key.
- Invariant table. Fifteen invariants, each named once and mapped to every place it is checked: the model, the test harness, a browser law, a production monitor.
- Store with named decisions. Every decision a bug could live in is its own function: how the index applies a change, where a detail page reads from, how saved creatures survive a taxonomy change. Each is a place a fault can be swapped in while the program runs.
- Live mutants and a probe. Seven faults, each redefining one of those functions in the running process at a recorded time. A probe runs the original beside the mutant on every call and counts when they differ. It never decides pass or fail.
- Drivers. The catalogue, indexer and taxonomy as seeded background parties, changing the shop only through the store's own operations. Every step from every party, the customer's included, is checked against every invariant, and the first violation of each is kept with its time, party and command.
- Page laws. Ten temporal laws over the page's data attributes, checked by Bombadil on every state it reaches, plus one that relays the server's verdicts. A reach count shows each law had something to check: in a clean run, from 170 states (a stale saved creature) to 1,539 of 1,540 (the selector).
Who may read what
Most of the harness's value comes from what each part may not see. A checker that can read the code under test, or a page that can read the checker, will agree with itself.
| part | responsible for | never | enforced by |
|---|---|---|---|
| model | what may happen, as states and actions | depends on implementation details | written and checked first |
| oracle | the expected list, badge and cascade | calls the store's domain functions | a separate module; a control run measures what sharing costs |
| store | state transitions, one named function per decision | reads the oracle or the probe | pure functions that import neither |
| probe | whether a mutant changed an output, and when | decides pass or fail | the checker never reads it |
| checker | every invariant after every step, from any party | reads the probe | one lock per step, so a probe call is never counted twice |
| drivers | changing the world through the store's own operations | write state directly | a raw write can build a state the program never could |
| page | rendering what the server returns | reads the oracle channel or the driver routes | the run script refuses to start if it does |
| driver routes | reset, start, stop, apply a mutant, read the log | answer anything but loopback in a test environment | a gate on every route |
| a mutant | one wrong decision, letting the rest run | coexist with another, or survive a reset | one at a time; restored on every exit path |
What it found that a finished application would hide
A checker that shares the code sees nothing
The original specification's harness checked the store with the store's own cascade and
badge. Mutants in those two functions survived all 300 generated runs. With the separate
oracle they were caught in 4 and 279. A completed application usually ships its tests written
against its own helpers, so this is the failure you get by default.
A rule the model implied and nobody wrote
A taxonomy change that silently deleted saved creatures violated none of the model's eight
invariants and none of the harness's fourteen checks. The model forbade it only as
UNCHANGED saved inside one action. Written down as an invariant, it was caught in 108 runs.
The first TLA+ property written for it was too loose: it allowed any one removal, to leave room
for Forget, and with one saved creature a removal by the taxonomy looked exactly like Forget.
The planted fault showed that; the property now ties the frame to the actions.
The specified model could not be checked
The original model configuration ran for 30 minutes, reached 9.06 million states and did not finish. A smaller configuration (one year, one book) finishes in 6 minutes at 2,008,080 states, with no error, and catches six planted design faults in 3 to 10 steps each. A spec you cannot check is a document; the bound is part of the deliverable.
Faults surface where the customer stands
The faults sat in the indexer, the fit-rule interpreter and the taxonomy cascade. Of the 29 first violations recorded across the browser runs, 25 appeared on a customer's search, select, detail or save. A test that drives only the UI sees the symptom and nothing about which party's code caused it; the per-step party log says.
The detail page reads the catalogue while the list reads the index. The list says no-fit (index v12); the detail panel for the same book says fits (catalogue v13).
Wrong is not the same as shown wrong
That mutant changed what a detail page read within 63 to 364 ms of going in. In one run, nothing the page displayed differed for another 27 seconds. Without a probe beside the mutant, that run reads as "fault applied, tests green".
Some rules can only be checked on the server
Four of the seven mutants were first caught by server invariants relayed to the browser, not by a page law. The page's data contract carries no index membership or selection validity, so "only live books are listed" cannot be checked from the page at all. That is a gap in the contract, found before any user hit it.
Saving a creature twice puts it in the Menagerie twice. The page laws catch this one directly.
A reindex with nothing to do moves the index back one version. The footer had shown index v16
a moment before; indexVersionMonotonic, a law the original page contract left to a monitor,
catches it.
Faults in the page itself
Two faults went into the page's own code, and both are invisible to the server.
The detail panel shows the badge a book had the first time it was opened. The list says fits; the panel still says unknown. Caught in 3 of 3 runs.
A stale saved creature keeps an enabled Activate button. Compare the clean frame at the top, where the same state has it disabled. Caught in 2 of 3 runs; the third never had a stale creature on screen.
Green can mean never tried
The saved-creature fault was reached once in three browser runs, 33 ms before the run ended, and the server saw it but the page did not. Reach counts and the probe make that visible. A pass/fail report would have called it a survivor, or a pass.
Every live fault, every layer that could see it
Left to right: the property-based harness (300 generated command sequences), one 600-command run with the fault applied at command 150, and the browser under Bombadil (three 60-second runs, fault applied at 20 s). The clean shop ran three times with no violation.
| fault | harness, 300 runs | mid-run: infected → caught | page laws | server invariants | shared oracle |
|---|---|---|---|---|---|
pdp-reads-catalog-head |
4 runs | 218 → 256 | 1/3 | 3/3 | |
cascade-keeps-genus |
4 runs | 207 → 207 | 0/3 | 3/3 | survived 300 |
save-no-dedupe |
43 runs | 397 → 397 | 3/3 | 3/3 | |
indexer-skips-deletes |
3 runs | 154 → 162 | 0/3 | 3/3 | |
badge-ignores-years |
279 runs | 372 → 372 | 0/3 | 3/3 | survived 300 |
taxo-change-drops-saved |
108 runs, once its invariant existed | never reached | 0/3 | 1/3 | |
index-version-rollback |
4 runs | 178 → 178 | 3/3 | 3/3 |
Six design faults went into the TLA+ model: a detail page reading the catalogue head, search ignoring "fits only", an index running ahead, a taxonomy change skipping the cascade, a stale active creature, and deleted saved creatures. TLC caught each in 3 to 10 steps, in about a second each; the last only after the frame property existed.
A note on screenshots
Bombadil's screenshot for a state can lag the page it checked by a frame or two. At the state
where savedDistinct first failed, the extractor read two Menagerie entries and the screenshot
still showed one; the duplicate is on screen two states later. The frames above were chosen at
the first state where the violation is visible, which is the lab's standing rule: open the
screenshot before believing a first violation.
What it took, and what it does not cover
The model, oracle, store, harness, session, page, laws and run scripts come to about 1,700 lines. The exhaustive model check takes 6 minutes and the browser matrix 35.
- The exhaustive model has one year and one book; the larger configuration needs symmetry or simulation to say anything.
- The browser relays server verdicts through a one-second poll, so a fault caught in the last second of a run reaches the server but not the page.
- The drivers are seeded but share one random stream across threads: runs repeat in kind, not step for step.
- Production telemetry, the contract's change control and a shadow reference implementation are specified but not built.
When to build the harness before the application
- More than one party writes the state a user sees: imports, background jobs, administrators, other users.
- A derived view (a search index, a cache, a replica) lags its source, and users act on the view.
- Users save things that depend on reference data someone else can change.
- Two pages show the same fact, and disagreement would cost money or trust.
- You are buying or inheriting the application, and its tests were written by the same hands, against the same helpers, as its code.
Ask for the oracle, the invariant table and the fault list with the application. If the supplier cannot plant a fault and show which check catches it, you are taking the code's word that it works.
Limits
One shop, one lab, one day of runs: experiment 018, phases 0 and 1, run 4 November 2026. Model checked with TLC 2.19; harness in Clojure with test.check 1.1.3 at seed 18; browser runs with Bombadil 0.7.10. Mutation outcomes follow the reach, infection, propagation and revealability model. No other application has been checked this way yet, so every number here is from this one.