The fault matrix & exploration

Stages 2 and 3 of the verification model are how Faultbox generates work — turning a handful of declarations into hundreds of distinct executions. This page explains the four layers a fault can be injected at, the matrix that crosses faults with flows, and exploration — the search over everything you couldn’t enumerate by hand.

First: the four layers a fault lives at

A real failure can happen at very different depths. Faultbox injects at four, and a single spec composes any combination:

The target you pass decides the layer: a service (db) → syscall level (seccomp-notify); an interface (db.pg) → protocol level (transparent proxy). Same fault_assumption() builtin, different dispatch.

Rule of thumb: start at the syscall layer for “is X down / slow / broken?” — it’s one line and catches broad categories. Add protocol faults for “does this specific query/path/command fail correctly?” — they’re precise and keep the service otherwise healthy. Combine them via composition when you need both.

→ Decide which: Choosing fault levels

Stage 2 — The matrix: scenarios × fault assumptions

You don’t test one failure against one flow; you test the grid. Two reusable building blocks:

• A scenario is a probe — a function that exercises a flow and returns an observable result (create_order, health_check).
• A fault assumption is a named failure mode — composable, reusable, and carrying its own invariant monitors (db_down, disk_full, kafka_drop).

fault_matrix() crosses them into the fault generation matrix: N scenarios × M faults = N×M cells, from one declaration.

fault_matrix(
    scenarios = [create_order, list_orders, health_check],
    faults    = [db_down, db_slow, disk_full, cache_down],
    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),
    },
    exclude = [(health_check, disk_full)],   # health check never writes
)
# 3 scenarios × 4 faults − 1 excluded = 11 cells

Each cell inherits the monitors attached to its fault assumption, so safety checks scale with the grid automatically. The named fault assumptions are what make the report readable:

                 │ db_down      │ disk_io_error │ cache_down
─────────────────┼──────────────┼───────────────┼────────────
create_order     │ PASS (210ms) │ FAIL          │ PASS
list_orders      │ PASS         │ PASS          │ PASS (fallback)
health_check     │ PASS         │  —            │ PASS

Finding the cells worth filling: the dependency matrix

The practical technique for deciding what goes in the grid: list every service and its dependencies, then for each dependency enumerate three faults — down (connect refused), slow (delay), errors (I/O / disk full). That’s a strong starting grid. Prioritize the cells by data-loss risk, user impact, recovery difficulty, and production frequency — start in the top-left corner (high risk + high frequency) and work out. You’re never “100% covered,” and you shouldn’t aim to be; cover the high-impact failures and stop.

→ Do it: Fault testing methodology · Spec patterns by architecture

Stage 3 — Exploration: searching what you can’t enumerate

A matrix cell is still not a single execution. Inside one cell, real systems have branch points you can’t list by hand:

• which backend serves a read (primary vs replica),
• which of two concurrent requests wins the race,
• whether a retry fires before or after the original succeeds.

You name these unknowns in the spec, and Faultbox fans each cell out into a tree of leaves — one leaf per combination, each with a stable LeafID.

Two operators prune the tree so it stays tractable:

This is the bridge from “fault injection” to systematic exploration: the matrix says which failures, exploration says in which of all the possible ways. Together they turn a spec into a state-space search.

See the tree before you run it: faultbox plan

A combinatorial fan-out can explode. faultbox plan performs static analysis of the plan tree without launching a single service — so you see the shape and size first:

faultbox plan spec.star                       # render the leaf tree
faultbox plan spec.star --coverage            # which axes/cells are covered
faultbox plan spec.star --suggest             # propose faults you're missing
faultbox plan spec.star --check-cost --max-instances 500   # fail if it blows up

plan.json is written into every .fb bundle and surfaced in the report’s Plan tab, so the tree that was explored is auditable after the fact.

faultbox plan --suggest replaces the old faultbox generate command.

How the pieces nest

fault_matrix          →  cell (scenario × fault_assumption)
  └─ choose / nondet   →  leaf (one concrete combination)
       └─ interleaving →  leaf (one concrete ordering)
            └─ verdict →  PASS / FAIL / INCONCLUSIVE  + seed for replay

Each leaf is one deterministic execution — which only means something under a stated reproducibility contract.

→ Concept: Determinism & reproducibility

Next: Determinism & reproducibility → — why a leaf’s verdict is trustworthy and replayable.