/ docs
On this page

The verification model

This is the mental model the rest of the documentation zooms into. Every Faultbox run is the same pipeline, whether it’s one binary or a mesh of containers:

   ┌─────────────┐   ┌──────────────┐   ┌─────────────┐   ┌──────────────┐   ┌──────────┐
   │  1. SPEC    │──▶│ 2. FAULT     │──▶│ 3. EXPLORE  │──▶│ 4. CHECK     │──▶│ 5. REPORT│
   │  describe   │   │   MATRIX     │   │  the state  │   │  invariants  │   │  verdict │
   │  the system │   │ scenarios ×  │   │  space      │   │  & temporal  │   │ you trust│
   │             │   │ fault        │   │ (choose,    │   │  properties  │   │ & replay │
   │             │   │ assumptions  │   │  orderings) │   │              │   │          │
   └─────────────┘   └──────────────┘   └─────────────┘   └──────────────┘   └──────────┘
        spec.star      one cell per       one leaf per       per leaf:           plan.json
                       (scenario,fault)   (cell × choice ×    PASS / FAIL /       + HTML report
                                           ordering)          INCONCLUSIVE
        ╲___________________________________ determinism contract ____________________________╱
                        (L1–L5: what must be reproducible for the verdict to mean anything)

The five stages map one-to-one onto the rest of this section. Read this page to see how they connect; follow the links to go deep on each.

Stage 1 — Describe the system (the spec)

A Faultbox spec is one executable Starlark file. It declares topology (services and the interfaces they expose), scenarios (the flows you care about), fault assumptions (what can go wrong), invariants (what must stay true), and a determinism contract (how reproducible the result must be). Nothing is in YAML; the spec is code, so it composes and load()s.

A whole-system spec, end to end:

# --- determinism contract: declare up front how reproducible this must be ---
determinism(level = "L1")   # mediated-event determinism, strict mode on

# --- topology: services and the interfaces they expose ---
db = service("db",
    interface("pg", "postgres", 5432),
    image = "postgres:16",
    env = {"POSTGRES_PASSWORD": "test", "POSTGRES_DB": "shop"},
    healthcheck = tcp("localhost:5432"),
    observe = [observe.stdout(decoder = decoder("json"))],
)

api = service("api",
    interface("http", "http", 8080),
    image = "shop-api:latest",
    env = {"DATABASE_URL": "postgres://test@" + db.pg.internal_addr + "/shop"},
    depends_on = [db],
    healthcheck = http("localhost:8080/health"),
)

# --- scenarios: the critical flows, as probes that return a result ---
def create_order():
    return api.http.post(path = "/orders", body = '{"item":"widget","qty":1}')

scenario(create_order)

# --- invariants: properties that must hold no matter what (see Stage 4) ---
def confirmed_means_persisted(event):
    if event["type"] == "stdout" and event.get("status") == "confirmed":
        rows = events(where = lambda e: e.type == "wal" and e.data.get("action") == "INSERT")
        if len(rows) == 0:
            fail("order confirmed but never persisted")

persisted = monitor("confirmed_means_persisted", on = confirmed_means_persisted)

# --- fault assumptions: named failure modes, carrying their invariants (Stage 2) ---
db_down = fault_assumption("db_down",
    target = api, connect = deny("ECONNREFUSED"),
    monitors = [persisted],
)
disk_full = fault_assumption("disk_full",
    target = db, write = deny("ENOSPC"),
    monitors = [persisted],
)

# --- the matrix: cross scenarios with fault assumptions (Stage 2) ---
fault_matrix(
    scenarios = [create_order],
    faults = [db_down, disk_full],
    default_expect = lambda r: assert_true(r != None),
    overrides = {
        (create_order, db_down):   lambda r: assert_eq(r.status, 503),
        (create_order, disk_full): lambda r: assert_true(r.status >= 500),
    },
)

That single file is the whole input. Everything below is what Faultbox does with it.

→ Reference: Spec Language · Learn it: Tutorial Part 1

Stage 2 — The fault matrix

You rarely test one failure against one flow. You test the cross-product: every scenario against every fault assumption. fault_matrix() builds that grid for you — N scenarios × M faults is N×M test cells from one declaration. Each cell inherits the invariant monitors attached to its fault assumption, so safety checks travel with the failure mode, not with the test.

The matrix is how a spec scales from “I tested the obvious case” to “I covered the grid.” This is the fault generation matrix at the heart of the method.

→ Concept: The fault matrix & exploration

Stage 3 — Explore the state space

A cell is still not a single execution. Within a cell there may be choices you can’t enumerate by hand: which backend serves the read, which of two concurrent requests wins the race, whether the retry fires before or after the original. You name these unknowns — choose("backend", [primary, replica]), parallel(..., interleavings=...), nondet() — and Faultbox fans each cell out into a tree of leaves, one per combination, each with a stable LeafID.

faultbox plan shows that tree before you launch anything, so you can see how big it is and prune it (assume(), --max-instances N) instead of being surprised by a combinatorial blow-up at runtime.

→ Concept: The fault matrix & exploration

Stage 4 — Check invariants & temporal properties

While each leaf runs, Faultbox records a single ordered event log — syscalls, protocol messages, WAL rows, stdout lines, all vector-clocked. Two kinds of property are evaluated against it:

  • Invariants (safety): “this must never happen” / “if A, then B must have happened.” Encoded as monitor() state machines and assert_never().
  • Temporal properties (liveness & ordering): “this must eventually happen,” “A must always hold between two points,” “the system must reach a stable quiescent state.” Encoded with eventually(), always(), await_event(), await_stable().

A property that fires turns the leaf’s verdict to FAIL regardless of which scenario or fault triggered it. That’s the power: an invariant catches bugs in cells you never wrote an explicit expectation for.

→ Concept: Invariants & properties

Stage 5 — A verdict you can trust

Every leaf resolves to a three-valued verdict — PASS / FAIL / INCONCLUSIVE — and the run produces an HTML report plus a plan.json describing the tree that was explored. INCONCLUSIVE matters: it’s how Faultbox tells you a leaf neither confirmed nor refuted the property (the fault never fired, the system never reached the checked state) instead of lying with a green PASS.

A failing leaf replays deterministically from its seed — which is only meaningful because of the contract running underneath the whole pipeline.

→ Concept: Reading reports & verdicts

Underneath everything — the determinism contract

The dashed line in the diagram is the determinism contract (determinism()). It’s not a stage; it’s the foundation the verdict rests on. If a “FAIL” can’t be reproduced, it’s a rumor, not a bug report. The contract states which levels of non-determinism (clock, RNG, DNS, undeclared I/O, thread scheduling) are mediated by Faultbox versus allowed to leak — L1 through L5 — and at strict levels, any unmediated leak fails the test at the first occurrence rather than silently poisoning reproducibility.

→ Concept: Determinism & reproducibility

The whole story in one line:

Describe your system → generate a fault matrix → explore the state space deterministically → check invariants and temporal properties → read a verdict you can trust and reproduce.

Next: Invariants & properties →

Edit this page on GitHub