extla

# Decision Log

Design decisions with enough rationale that they do not get re-litigated every few
weeks. Each entry records what was decided, what it replaced, and what would justify
revisiting it.

Format: **D-*n*** — short title. Superseded entries stay, marked, because the reasoning
that was rejected is part of the record.

---

## D-1 — Constants are pinned (`^name`); atoms are always literals

**Decided.** A constant is referenced as `^accounts`. A bare atom is always a literal
atom.

**Replaced:** bare atoms standing for constants (`length(:accounts)`).

**Why:** the earlier form gave one syntax two meanings that cannot be separated in
general — `status = :idle` assigns a literal, `length(:accounts)` reads a constant, and
no rule distinguishes them without knowing every declaration and every function's
intent. The pin operator already means "a value from outside this scope" in Elixir, so
it reads correctly and parses unambiguously.

**Revisit if:** a syntax emerges that is both unambiguous and lighter. Ambiguity alone
is not a trade worth making for brevity.

See `02-dsl-semantics.md` §1.1.

**Pinned by:** `test/ex_tla/spec/diagnostics_test.exs` — a bare
name matching a constant is `:constant_without_pin`, and an atom in a spec body stays a
literal.

---

## D-2 — Action bodies are simultaneous, not sequential

**Decided.** Every RHS reads the pre-state, every LHS writes the post-state, unassigned
variables are `UNCHANGED`, and a variable may be assigned at most once.

**Why:** it is what TLA+ means, and it is the only reading under which
`x = y; y = x` swaps. The rule also makes an action body a pure function of
`(pre_state, params)`, which D-3, the symmetry canonicalization, and D-6 all depend on.

**Cost:** it surprises Elixir programmers, who read `=` as sequential rebinding. Paid
for with an explicit rule (§2), a compile error on double assignment, and `let` for the
sequential case.

See `02-dsl-semantics.md` §2.

**Pinned by:** `test/ex_tla/spec/diagnostics_test.exs` "a variable assigned twice is rejected, not
resolved last-write-wins" — the shape that would exist if bodies were sequential.

---

## D-3 — Nondeterminism lives only in `params:`

**Decided.** `params:` is the sole branching mechanism. Entries may draw from a
constant, a literal range or list, or a function of the pre-state and the params bound
before them. `choose/2` keeps TLA+'s deterministic `CHOOSE` semantics.

**Replaced:** `choose(set)` inside an action body, documented as "explores all valid
choices".

**Why:** two reasons, either sufficient. First, the name was wrong — `CHOOSE` in TLA+ is
deterministic Hilbert choice, so giving it branching semantics would mislead everyone
who knows the notation ExTLA is modeled on. Second, it could not be implemented: a
function returning one element cannot produce several successors. Folding the state-drawn
case into `params:` removes the construct rather than fixing it, and leaves the body
deterministic.

**Revisit if:** a spec in the acceptance corpus (`07-examples.md`) cannot be expressed. The
Raft example was the hard case and it fits.

See `02-dsl-semantics.md` §3.

**Pinned by:** `test/ex_tla/spec_test.exs` and `test/ex_tla/coverage_test.exs` — every binding of a `params:`
entry produces its own successor, and coverage counts them.

---

## D-4 — 64-bit fingerprints, not `phash2`

**Decided.** State identity is `:erlang.term_to_binary(state, [:deterministic])` hashed
with SHA-256, truncated to 64 bits by default. The collision estimate is reported in
every result.

**Replaced:** `:erlang.phash2`, chosen for sub-microsecond speed.

**Why:** `phash2`'s default range is 2^27-1. By the birthday bound a 10M-state run — the
stated target — would silently drop on the order of 372,000 states and report success;
even a 100K-state run loses about 37. A dropped state is an unexplored state, so the
tool would report verification over a space it never visited. That is the worst failure
mode a verification tool has, and it is not worth 1-2 microseconds per state. TLC uses
64-bit fingerprints for the same reason.

The `:deterministic` flag matters independently: plain `term_to_binary` on maps and
MapSets is not a guaranteed canonical encoding across OTP versions.

See `01-foundation.md` §`ExTLA.Fingerprint`.

**Pinned by:** `test/ex_tla/fingerprint_test.exs` — the width, and the collision estimate reported with it.

---

## D-5 — The graph stores parent pointers, not states

**Decided.** Each visited state contributes `{parent, action, params}` keyed by
fingerprint. States are regenerated by forward replay when a trace is needed.

**Replaced:** `states: %{state_id => ExTLA.State.t()}` retained for the whole run.

**Why:** at the 10M-state target and ~1KB per state that is ~10GB of RAM, which puts the
checker out of reach of ordinary machines. The fixed record is ~64 bytes regardless of
state size, so memory scales with state count rather than state size. Trace generation
happens at most once per run and pays the replay cost instead.

**Cost:** a spec with expensive actions pays that cost twice on the failing path. The
right place for it to fall.

See `04-layer2-model-checker.md` §State Graph.

**Amended 2026-08-30.** Parent pointers form a spanning tree, which has no cycles, so
this record alone cannot support liveness checking — the original entry did not say
so, and `04` specified `sccs/1` over it. Under `check_liveness: true` the graph
additionally records each state's out-edges and one ENABLED bit per fairness
constraint, both captured while the state is materialized. States are still never
stored; per-state memory grows by ~16 bytes per edge and stays independent of state
size, which is the property this decision exists to keep. This is the split TLC makes.
See `04-layer2-model-checker.md` §State Graph, "The liveness graph".

**Pinned by:** `test/ex_tla/action_property_trace_test.exs` — a trace
is regenerated by replaying actions forward, because the graph retains no states.

---

## D-6 — Layer 3 checks step legality, not just invariants

**Decided.** After each callback, the named spec action is applied to the abstract
pre-state and its result compared to the abstract post-state. An `:unmapped` message
must leave the abstract state unchanged.

**Replaced:** computing the abstract action and then using it only for logging, while
checking invariants and action properties on the projected state.

**Why:** the replaced design is not refinement checking. Under it an implementation may
take a transition no spec action permits, and pass as long as the invariants happen to
hold — which is every interesting implementation bug. `07-examples.md` §4 is a two-line
counter whose implementation the old design would have passed and the new one rejects.

Affordable because of D-2/D-3: one function application and one comparison, cheaper than
the invariants evaluated beside it.

See `05-layer3-conformance.md` §What conformance means here.

**Amended 2026-08-30.** `check_step!/5` accepts PARTIAL params and searches the unbound
ones. An implementation routinely resolves the spec's nondeterminism itself — it pops
its own queue — so the binding is not in the message and the mapping cannot supply
it; "one application, one comparison" was only true for fully-bound actions, and
`validate!/2`'s round-trip rule was unsatisfiable for any other. A step is legal if
some binding reproduces the post-state, which is still refinement.
See `05-layer3-conformance.md` §`ExTLA.GenServer.Runtime`.

**Pinned by:** `test/conformance/step_test.exs` — a state that satisfies every invariant and was
reached by an illegal step is a `:diverged` finding.

---

## D-7 — `concrete_message/2` on the refinement mapping

**Decided.** `ExTLA.Refinement` declares `concrete_message(action, params)`, the inverse of
`abstract_action/1`. Optional, but its absence forgoes counterexample replay and trace
validation.

**Why:** the earlier draft used it in a property-test example without ever declaring it.
It is what lets a spec-level behavior *drive* the implementation — replaying a
counterexample, or checking a captured production trace — which is the difference
between three tools that share a namespace and one pipeline.

**Amended 2026-09-22 (#176), pending #172.** The callback returns a *tagged* message —
`{:call, m}`, `{:cast, m}` or `{:info, m}` — with a bare term meaning a call, so every
mapping written against this decision keeps its meaning. Only the author knows how a
message reaches their server, and until the tag existed Layer 3 could check a
cast-handling implementation and could not drive one: the driver sent every message as a
`$gen_call`, so `spec/05`'s own canonical mapping, which handles two of four actions by
cast, was undrivable. How a cast's completion is observed is its own decision (D-30).

**Pinned by:** `test/conformance/conformance_test.exs` "a mapping whose two directions
disagree is caught by the round trip" — which is what makes the mapping's two halves each
other's inverse.

See `05-layer3-conformance.md` §`ExTLA.Replay`.

---

## D-8 — Model checker first; Layer 1 ships with Layer 3

**Decided.** Phase 1 is the DSL, the compile-time validator and the safety checker,
accepted against a differential corpus run through TLC. Layer 1 arrives in Phase 3.

**Replaced:** Layer 1 as the MVP.

**Why:** Layer 1 de-risks nothing about Layer 2 — the layers share almost no machinery,
and Layer 1's dependencies (`ExTLA.State`, `ExTLA.Config`) are trivial. Shipping it first
would enter a market already holding Corsa, Bond, Oath and ExContract with no
differentiator, while the actually unproven part — whether this DSL can be compiled and
checked at all — stayed untested. The prior-art survey records what happens to projects
here that spend early effort on breadth.

**Revisit if:** an adopter needs Layer 1 alone and is willing to fund it. It is a small
piece once the runtime checking engine exists; it is the sequencing, not the feature,
that is being decided.

See `06-architecture.md` §Implementation Phases.

**Pinned by:** nothing — this is a decision about build order, and the order it chose is history.

---

## D-9 — Differential testing against TLC is the acceptance criterion

**Decided.** The checker is accepted when it agrees with TLC on distinct state counts,
invariant verdicts and shortest-counterexample lengths across a corpus of classic specs.

**Why:** a model checker with no oracle cannot be trusted, and unit tests of a BFS loop
verify the loop, not the semantics. TLC plus the specs everyone has already written is a
free oracle, and a disagreement on state count is the most informative possible signal
that successor generation or state identity is wrong.

See `04-layer2-model-checker.md` §Differential testing against TLC.

**Pinned by:** `test/differential/differential_test.exs` — every corpus entry's verdict, counts and
counterexample length against TLC's `expected.json`.

---

## D-10 — Incomplete runs fail; coverage is reported

**Decided.** `max_states_reached` is exit code 2 and a test failure, not a warning.
Never-enabled actions and vacuously satisfied properties are reported by default and
fail under `--strict-coverage`.

**Replaced:** `IO.warn` on hitting the state limit, with the test passing.

**Why:** "we ran out of budget" is not "it holds". A suite that goes green on an
unverified spec teaches its users to believe something false, which is worse than having
no tool. The coverage report exists for the same reason one step further out: a spec
whose action is disabled by a typo'd guard verifies easily and means nothing.

**The escape hatch, recorded 2026-09-22 (#176).** `allow_incomplete: true` — and
`mix extla.check --allow-incomplete` — turns a bounded run's exit 2 into exit 0. It has
existed since the day this decision was written and this decision did not mention it,
which made the decision read as stronger than the code it describes.

It is right that it exists and right that it is opt-in: a model too large to exhaust is
a real situation, and a run that covered part of the space is worth something to the
person who asked for it. What it must never do is quiet: the coverage report still says
what bounded the run, `coverage.bounded_by` still carries it, and a temporal property
skipped because the budget stopped the search is still named in `warnings` (#208). The
flag changes the exit code and nothing else, which is the difference between accepting a
partial answer and being told a partial answer is a complete one.

**Pinned by:** `test/ex_tla/spec/test_test.exs` "flunks on a bounded run rather than
warning" and "allow_incomplete: true accepts a bounded run deliberately" — both halves of
the decision, since the flag existing and the flag being needed are separate claims.

See `04-layer2-model-checker.md` §Coverage and Vacuity, §ExUnit Integration.

---

## D-11 — Compile-time configuration, `defoverridable` wrapping

**Decided.** `ExTLA.Config.mode/0` is a `compile_env` macro; `:disabled` emits no wrapper
at all. Callbacks are wrapped with `defoverridable` and `super/1`.

**Replaced:** runtime `Application.get_env` with a `Mix.env()` default, and callback
renaming to `__original_handle_call__`.

**Why:** two separate bugs. `Mix` does not exist in a release, so the runtime default
raises there. And renaming breaks on multi-clause callbacks with guards — which is every
real GenServer — while `defoverridable` preserves them by construction. Compile-time
resolution is also what makes "zero production cost" true rather than approximate.

See `01-foundation.md` §Configuration, `03-layer1-invariants.md` §Compile-Time Transformation.

**Pinned by:** `test/ex_tla/invariant_modes_test.exs` — `:disabled` emits no wrapper at all, and the
wrapping is `defoverridable`/`super` rather than a rename.

---

## D-12 — A bounded temporal fragment, stated explicitly

**Decided.** `always`, `eventually`, `~>` and state predicates, composable as given in
`02-dsl-semantics.md` §5.1. No negation, conjunction or disjunction of formulas. A
formula outside the fragment is a compile error.

**Why:** the fragment is checkable by SCC analysis without building a Büchi automaton,
and it covers what people write. The alternative failure — accepting a formula and
checking something weaker than it says — is the kind of quiet unsoundness this project
cannot afford. Widening the fragment starts with §5.1, not with the checker.

**Amended 2026-08-30.** The fragment includes `Enum.all?(^constant, fn x -> formula end)`
— quantification over a constant, which every per-process property in the corpus
needs, and which is a conjunction of in-fragment instances checked independently.
`always(P ~> Q)` is accepted as a spelling of `P ~> Q`.

**Pinned by:** `test/ex_tla/model_checker/liveness_shapes_test.exs` — each shape in the fragment is
refuted by a spec that violates it, which is what makes the fragment's edge real.

---

## D-13 — Non-goals are written down

**Decided.** ExTLA is not a theorem prover, does not explore interleavings, does not
extract models from source, does not generate implementations, and has no real-time or
probabilistic extensions.

**Why:** the earlier specs never said what ExTLA was not, which is how a supervision-tree
DSL got designed before a working checker existed. Each non-goal has a better tool
already (TLAPS, Concuerror, Verlixir, Erla+), named in `00-prior-art.md`.

See `06-architecture.md` §Non-goals.

**Pinned by:** nothing — a list of non-goals is a statement of intent, and there is nothing to run.

---

## D-14 — No `spec do ... end` block

**Decided.** The specification formula `Init /\ [][Next]_vars /\ Fairness` is implicit.
There is no top-level `spec` block.

**Replaced:** a `spec do init(); always(next()); fair() end` block that echoed the TLA+
formula.

**Why:** it was never given a meaning, and could not usefully have one — `Init` is the
`init` blocks, `Next` is the disjunction of declared actions, `Fairness` is the
`fairness` declarations. The block could only restate what was already declared, with
the standing risk that someone writes one that disagrees and it must then either be
ignored or mean something unspecified.

**Revisit if:** a spec genuinely needs to vary the formula — no fairness at all, or
refinement of another spec. That is a new declaration with defined semantics, added to
`02-dsl-semantics.md` before the checker.

**Pinned by:** nothing — the shape this decision refused was never built, so no test can fail on it.
The DSL's macros being top-level declarations is the whole of the evidence.

---

## D-15 — Fairness is per action or per parameter binding

**Decided.** `fairness :strong, acquire_lock: [:p]` declares one constraint per binding
of the named leading params — `\A p \in P : SF_vars(AcquireLock(p))`. The bare
`fairness :weak, [:acquire_lock]` form remains and means whole-action fairness.

**Replaced:** whole-action fairness only.

**Why:** whole-action WF guarantees that *some* binding fires, which is consistent with
one process requesting forever while the others take turns. Every starvation-freedom
property in `07-examples.md` was unprovable under it. The per-binding form is what TLA+
writes, and the primer under `research/` already documented it. State-drawn params
cannot be quantified over — the set changes per state — so they are a compile error in
this position.

**Cost:** one ENABLED bit per binding per state in the liveness graph (D-5, amended).

See `02-dsl-semantics.md` §5.2.

**Pinned by:** `test/ex_tla/spec_test.exs` and `test/ex_tla/model_checker/liveness_test.exs` — a per-binding
fairness constraint, and the refusal of one over a state-drawn param.

---

## D-16 — Terminal states are declared with `terminal`

**Decided.** A `terminal :name do pred end` block names legitimate end states. A
successor-less state a `terminal` admits is not a deadlock; nothing else changes.

**Replaced:** `check_deadlock: false` as the only way to accept a terminating spec.

**Why:** two corpus specs terminate by design — the bounded buffer once `^max_items`
are consumed, Raft election once the term bound is exhausted — and both were reported
as deadlocks by their own acceptance tests. Turning deadlock detection off to pass them
would have hidden real deadlocks elsewhere in the same spec. TLC users add a
`Terminating` disjunct to `Next`; a declaration is the same idea without a stuttering
action showing up in coverage.

**Guard against misuse:** a `terminal` that admits a state with an enabled action is
reported by coverage as `terminal_but_live`.

See `02-dsl-semantics.md` §5.3.

**Pinned by:** `test/ex_tla/model_checker_test.exs` — a `terminal`-admitted state is not a deadlock, and
an unadmitted successor-less state is.

---

## D-17 — Symmetry soundness is the author's obligation, verified dynamically

**Decided.** The compiler does not check that a `symmetry:` declaration is sound.
`--verify-symmetry` runs the model with and without the reduction on request and fails
on any disagreement.

**Replaced:** a promised compile-time rejection of order-dependent uses of a symmetric
constant.

**Why:** the promise was undecidable — a constant flows into arbitrary Elixir — and any
conservative approximation rejects the `Enum.all?(^processes, …)` every corpus spec is
built from. A verification tool that claims a check it cannot perform violates design
principle 6 more badly than one that names the obligation. The dynamic check is cheap
on a small constant assignment and catches exactly the failure the static check was
for. The *n*! canonicalization cost is now stated alongside, so the reduction is
benchmarked rather than assumed.

**Amended 2026-09-22 (#176), for #190.** The check also **declines to answer** rather
than answering wrongly. `--verify-symmetry` compares the reduced run's verdict with the
unreduced one's, and both runs get the same `max_states` while the whole purpose of the
reduction is that the unreduced run is bigger — so on any model large enough to need
symmetry, the unreduced run truncated first and the difference read as unsoundness. The
declaration was fine and the message said it was not, with maximum confidence, on exactly
the models this feature exists for. A comparison where either side is
`:max_states_reached` or `:constrained` is now refused and says so: a truncation is not a
verdict difference.

**Pinned by:** `test/ex_tla/symmetry_test.exs` "verify_symmetry cannot answer a bounded
comparison" — the describe block, whose tests cover both the refusal and the unsound case
still raising.

See `04-layer2-model-checker.md` §Symmetry.

---

## D-18 — Descriptions are a `desc:` option, and only where one is read

**Decided.** A description is a `desc:` entry in a declaration's options keyword list,
never a positional string — and it is accepted only by the declarations that have a
reader for it: `invariant`, `action_property`, `terminal` and `temporal`. `action`,
`variable`, `constant` and `init` **refuse** it.

**Replaced:** `invariant(name, description \\ "", opts \\ [], do: block)` and the same
shape on `precondition`, `postcondition` and `action_property`.

**Why the option rather than a positional:** two trailing optional positionals cannot be
told apart — `invariant :x, callbacks: [...] do … end` bound the keyword list to
`description`. Layer 2's `temporal` already took `opts` while the examples passed it a
heredoc, so the two layers had drifted on the one API shape the spec said they shared.

**Amended 2026-09-22 (#176), and this half is the correction.** As written, this decision
said *every* declaration macro takes `desc:`. That was the syntax rule generalised into a
claim about the surface, and nothing ever built it: `action`, `variable` and `constant`
swallowed a description silently through `Keyword.pop/2` and no consumer read it. #160
closed that silence by recording what each declaration **consumes**, established by
reading the consumers — which made the promise above a compile error, in the same file
that cites this decision two hundred lines earlier.

The option map is right and this decision was wrong. A description is surfaced in a
violation message or a coverage report; a `variable`'s has no reader and no obvious one,
and accepting it would restore exactly the silence #160 removed. If a reader appears —
an `action`'s description in the coverage report is the plausible one — that is a change
to this decision and to the map together, which is what keeps them from drifting apart
again.

**Pinned by:** `test/ex_tla/spec/diagnostics_test.exs` "an unknown option names the key and
what the declaration accepts" — `desc:` on a `variable` raises `:unknown_option`.

See `03-layer1-invariants.md` §Macro Specification, `02-dsl-semantics.md` §7.

---

## D-19 — Type annotations are stored quoted and checked as `type_ok`

**Decided.** `type:` expressions are kept as quoted Elixir, resolved against the
constants at model-check time, and checked as an implicit invariant `:type_ok` in every
reachable state. The grammar — including `|` union, tuples and the `[d ~> r]` function
form — is written down.

**Replaced:** a `type_expr` typed as concrete values (`Range.t()`, `[term()]`) that
none of the corpus's constant-dependent types (`0..^max_val`) could have produced,
alongside `~>`/`|` type syntax used throughout the examples but specified nowhere.

**Why:** a type that mentions a constant has no value at compile time; the only honest
representation is the expression itself. Checking types as an invariant rather than
using them to prune makes a type error a reported violation rather than a silently
narrower search.

See `02-dsl-semantics.md` §1.5.

**Pinned by:** `test/ex_tla/spec/type_test.exs` — the type grammar, and the implicit `type_ok` invariant
checked from it.

---

## D-20 — `f[x]` is strict function application, everywhere in a spec block

**Decided.** Inside a spec block, `f[x]` compiles to `ExTLA.Spec.Helpers.at/3`, which
raises `ExTLA.Spec.DomainError` outside the domain of `f` — for a map, for a sequence
(1-indexed, as in TLA+), and for anything that is neither. The rule has no exceptions:
it holds for a variable, a local, an `action_property`'s `old.`/`new.`, and a `params:`
generator's own state argument.

**Replaced:** `Access.get/2`, which is what `f[x]` means in ordinary Elixir.

**Why:** `Access.get/2` returns `nil` outside the domain, and `nil` is not an error.
Erlang's term order makes every comparison between types total and sorts atoms above
integers, so §8's own `require balances[from] >= amount` is **`true`** for an account
that does not exist. The guard succeeds, the action fires from a state where it was
never enabled, and the checker explores a state space the spec does not describe —
reporting success over it. That is precisely the failure `01-foundation.md` rules out
for `ExTLA.State.get/2`, `prime/3` and `ExTLA.Function.except/2`, and `[]` was the last
remaining hole in the syntax the worked example uses.

**Cost:** a keyword list indexed by its key inside a block now raises, since a list is a
sequence and `:mode` is not an index. That is the intended reading in a spec, where
state is maps and sequences.

**Why the rule has no exceptions:** the narrower version — strict on spec variables,
lax on `old.`/`new.` and on a generator's state argument — was rejected. Those are
exactly the places where a spec reaches into a collection it did not build itself, so
they are where the hole would be worth the most; and a rule an author has to remember
the shape of is one they will guess wrong.

See `02-dsl-semantics.md` §1.6 and `ExTLA.Spec.DomainError`.

**Pinned by:** `test/ex_tla/spec/guard_order_test.exs` and `test/ex_tla/spec/helpers_test.exs` — `f[x]`
raises outside the domain rather than answering `nil`, everywhere in a spec block.

---

## D-21 — Collections are element-typed with `set(t)` / `seq(t)`, and records with `%{k: t}`

**Decided.** §1.5 gains three forms: `set(t)` and `seq(t)` for a collection whose
elements are all of type `t`, and `%{k: t, …}` for a record — a map with exactly those
keys, each value of its type. Range bounds gain arithmetic (`0..(^max_items - 1)`) and
negatives (`-1..^max_ballot`).

**Replaced:** bare `:set` and `:seq`, which say nothing about what a collection holds.
They keep that meaning; the new forms are additions.

**Why:** the differential corpus found four entries typing a variable weaker than the
TLA+ they are checked against. `msgs \subseteq Message` in `two_phase_commit` and
`paxos`, `messages \subseteq Message` and `votesGranted \in [Servers -> SUBSET Servers]`
in `raft_election`, `buffer[i] \in Item` in `bounded_buffer` — all `:set` or `:seq` on
the ExTLA side. Both sides held, so no comparison was wrong; but the corpus is the
project's only oracle, and an entry that checks *less* than its oracle can agree with it
for the wrong reason. All four now check what TLC checks.

**Why a call form:** `{:set, t}` is terser and collides — it is already a legal tuple
type of the literal atom `:set` and a `t`. `[t]` collides with "one of these literals"
whenever the list has one element. `set(t)` reads like the `ExTLA.Spec.Helpers`
constructor of the same name and costs one grammar rule.

**Why records came too:** a set of records is what a message set is. `set(t)` with no
way to write `t` for a message would have closed the gap for `set(^servers)` and left
every message set where it was.


**Pinned by:** `test/ex_tla/spec/type_test.exs` — `set(t)`, `seq(t)` and record types, and their arity.
See `02-dsl-semantics.md` §1.5.
---

## D-22 — Symmetry reduction and liveness checking are refused together

**Decided.** A run that declares `symmetry:` and asks for `check_liveness: true` raises.
Safety is checked under the reduction; liveness is checked in a run without it.

**Why:** the quotient graph identifies states, so a path that leaves an orbit and a path
that returns to it look the same, and the quotient can hold cycles the real state space
does not. A cycle is precisely what a liveness verdict is read off
(`04-layer2-model-checker.md` §`ExTLA.ModelChecker.Liveness`), so a temporal property could
be reported as refuted by a behavior the spec does not have — or, with the fairness
constraints reading ENABLED bits of a merged state, as holding when it does not.

TLC warns about the same combination and runs anyway. A warning is not what this project
does with an unsound answer (design principle 6): the two reductions are each sound on
their own, and asking for both is asking for an answer neither of them supports.


**Pinned by:** `test/ex_tla/model_checker/parallel_test.exs` "what a parallel run refuses" and the
symmetry half beside it — the pairing is refused with a message naming the reason.
See `04-layer2-model-checker.md` §Symmetry.
---

## D-23 — A temporal operator over a finite trace returns three verdicts, not a boolean

**Decided.** `ExTLA.Temporal`'s operators return `:holds | :violated | :inconclusive`, and
take the index a lasso's cycle returns to.

**Replaced:** `01-foundation.md` typing every operator `:: boolean()`.

**Why:** a behavior is infinite and a trace is a prefix of one. A prefix can refute `[]P`
and can satisfy `<>P`, and can do neither the other way round — P may fail after the trace
ends, or hold after it. A boolean forces "P held throughout the states I saw" to be
reported as "`[]P` holds", which is claiming more than was checked (design principle 6),
one level below where `max_states_reached` makes the same distinction.
`05-layer3-conformance.md`'s `check_temporal_properties/2` already specified these three
verdicts, so the two documents disagreed and this settles it in favor of the honest one.

A lasso removes the doubt: prefix plus repeating cycle describes an infinite behavior with
finitely many states, and every operator then answers definitely. Without one, `<>[]P`,
`[]<>P` and `P ~> Q` are `:inconclusive` for every trace.

The same section also amends `ExTLA.Temporal.Fairness` to take `ENABLED` as its own
argument. `ENABLED <A>_v` quantifies over every state `A` could lead to, and a behavior
holds only the states that happened, so no function of the observed steps can answer it —
the original three-argument signature was not implementable as specified.

See `01-foundation.md` §`ExTLA.Temporal`.

**Pinned by:** `test/ex_tla/temporal_test.exs` — `:inconclusive` is returned rather than collapsed into
`:holds`, which is the whole of this decision.

---

## D-24 — A state machine's state is the `{state_name, data}` pair, and its message is the event content

**Decided.** In a module instrumented through `handle_event/4`, `invariant` and
`action_property` bind `state`, `old` and `new` to the `{state_name, data}` pair, and a
`precondition` or `postcondition` pattern matches the event **content** — not
`{event_type, content}`, and not the data alone.

**Why the pair:** `:gen_statem` splits what TLA+ calls the state across two callback
arguments, and neither half is the state. A machine in `:red` with a corrupt counter is in
a bad state, and so is one whose counter is fine and whose colour is not a colour. Binding
the pair also keeps §03's `TrafficLight` — which destructures `{name, data} = state` in
the block — exactly as specified, and keeps one meaning of `state` across the behaviours.

**Why the content:** so that `precondition {:withdraw, amount}` is the same declaration
whichever behaviour carries it. The event type is OTP's transport — call, cast, info,
timeout — and a property of a specification is not about how the message arrived. A
pattern that needed to know would have to be rewritten when a call became a cast, which is
a refactoring that changes no state at all.

**Consequences:** a module defining `handle_event/4` is instrumented as a state machine
throughout, including its `init/1` (`{:ok, name, data}`, not `{:ok, state, extra}`); and
`:gen_statem`'s returns need their own extraction, because `{:stop, reason, data}` and a
GenServer's `{:stop, reason, state}` are the same shape carrying different things.
`:state_functions` mode is out of scope — its transitions are functions named after the
states, which `@on_definition` cannot recognise.

See `03-layer1-invariants.md` §What a state machine's `state` is.

**Pinned by:** `test/ex_tla/invariant_behaviours_test.exs` — a state machine's `{state_name, data}` pair.

---

## D-25 — An `Agent`'s checks are runtime-dispatched, and `:disabled` is not free for them

**Decided.** `ExTLA.Invariant.Agent`'s entry points are **functions**, and they ask the
declaring module at runtime whether it carries predicates. Under `mode: :disabled` a
checked `Agent` call costs one export lookup and then does what the plain `Agent` function
does — not nothing.

**Why:** everywhere else in Layer 1 the mode is resolved where the instrumented module
compiles, and `:disabled` emits no code at all. An `Agent` call site is not that place.
The transition is a function the *caller* passes in, the module whose declarations apply
is an argument, and `Application.compile_env/3` — the only way the mode is read — does not
expand inside a function body. These were macros in a first draft for exactly that reason,
and the draft does not compile.

The alternative was to leave `Agent` unsupported, which §03's §Supported OTP Behaviors
does not permit. So the cost is stated instead of hidden: an `Agent` is the one place in
Layer 1 where turning checking off leaves something behind, and it is one `function_exported?/3`
per transition, in code the author wrote explicitly rather than code a hook injected.

**Also settled here:** `callbacks:` has no meaning for an `Agent`. It restricts a
declaration to named OTP callbacks and the caller's function is not one — it runs inside
`Agent`'s own `handle_call/3`. Every declaration in the named module applies to every
checked transition.

See `03-layer1-invariants.md` §An `Agent`'s checks cannot be compiled away.

**Pinned by:** `test/ex_tla/invariant_behaviours_test.exs` — an `Agent`'s checks dispatch at runtime, and
`:disabled` still costs a call there.

---

## D-26 — §6's term check runs at discovery, inside the state graph

**Decided.** `ExTLA.State.validate!/1` is called by `ExTLA.StateGraph.add_state/5`, on the
branch where the state's fingerprint is absent from the table — so once per **distinct**
state. The caller does not validate, and the successor is registered *before* its action
properties are evaluated.

**Replaced:** validation in the private `take_action/6` in `ExTLA.ModelChecker`, on every generated
successor. On `ExTLA.Differential.RaftElection` at the corpus constants that was 255,270
validations where 58,359 would do, and 77.9% of a 23.4 s search.

**Why it is sound, which is the part worth recording.** Validating only new states
necessarily happens *after* the state has been hashed, since newness is knowable only from
the fingerprint — so the ordering §6 appears to demand (validate before you fingerprint)
is not achievable. It is also not the ordering that matters. What matters is that
validation precedes any *use* of the state, and the guarantee survives for a reason
specific to the terms §6 rejects: a pid, reference, port, fun or float is precisely a term
whose encoding does not recur. A state carrying one therefore cannot dedup against an
earlier state, always misses the table, and is always validated on the path that reaches
it first. `:erlang.term_to_binary/2` encodes such terms without complaint, so reaching the
check is guaranteed rather than lucky.

**Why the graph and not the checker.** §6 exists *for* fingerprinting — the terms it
forbids are exactly those whose encoding does not identify a state. Putting the check
where the fingerprint is taken keeps the rule beside its reason, and lets every caller
assume that a state which has entered the graph is one the checker has vetted.

**What this forced.** `add_state/5` now runs before `Safety.check_action_properties/5`
rather than after. Left in the old order, a user's action property would be handed a state
§6 had not yet rejected, and a forbidden term would surface from inside that predicate
instead of from a diagnostic naming the variable — a worse error about a different thing.
The hoist also collapsed two `add_state/5` call sites into one.

**Measured:** 2.65x on `raft` (25.2 s to 9.5 s) and 1.62x on `buffer`, interleaved on one
machine, minima compared. Validation itself fell 4.47x against the 4.37x that the
transition-to-state ratio predicts.

**Revisit if:** a term is ever added to §6's permitted set whose encoding *can* recur
while still being forbidden. The soundness argument above depends on the forbidden terms
being exactly the non-recurring ones, and would have to be rebuilt.

See `02-dsl-semantics.md` §6, `bench/search_profile.baseline.md`.

**Pinned by:** `test/ex_tla/state_validation_test.exs` — a forbidden term is refused at discovery, once
per distinct state.

---

## D-27 — Parallel exploration is level-synchronous, and workers register their own states

**Decided.** `ExTLA.ModelChecker.Parallel` expands one whole BFS level across N workers and
waits for all of them before starting the next. Each worker calls
`ExTLA.StateGraph.add_state/5` on its own successors, against the shared ETS tables, and
returns accumulators that the coordinator merges. `workers:` defaults to **1**.

**Rejected:** a free-running frontier — workers pulling from a shared queue and never
synchronising. It is the faster design and it trades away the project's acceptance
criterion. D-9's differential corpus compares the **length** of the shortest
counterexample against TLC's, and length is not preserved when a violating state can be
reached along a longer path before the shorter one has been expanded. Length, note, and
not route: a parallel run may return a *different* trace of the same length and the corpus
still holds, which is what makes level-synchrony sufficient as well as necessary.

Level-synchrony also buys determinism where it is checked: every state discovered while
expanding level *k* has depth *k+1*, so whichever worker reports a violation first, the
trace is the same length.

**Why workers register rather than report.** The simpler design — workers compute
successors, the coordinator registers them — would parallelise about a quarter of the
work. Since D-26 `add_state/5` performs fingerprinting and the §6 check as well as the ETS
write, and `bench/search_profile.baseline.md` puts the three at 77% of the `raft` search;
Amdahl caps a central registrar near 1.3x however many cores are added. #31 built for
this: `:public` tables, an atomic id, and `insert_new/2` so that of two workers
discovering the same state exactly one claims it.

That atomicity is also what makes the accumulators *summable*. A state is observed by
exactly one worker and a `{state, action}` pair expanded by exactly one worker, so nothing
is counted twice — the merge is exact rather than approximate.

**What the merge revealed.** `ExTLA.Coverage`'s `distinct_generated` credits the action that
reached a state *first*, which is a fact about the search order rather than about the
model: its split across actions moves under `workers:` and its total does not. It is
documented as such and nothing in the report is derived from it. Every other coverage
field is order-independent and must match a single-threaded run exactly — a report naming
an action as never enabled when it was is a false statement about the model, and
`--strict-coverage` fails a build on it.

**With one boundary: a run that halted.** A search that stops at a counterexample stops
mid-expansion, so its counts are a lower bound rather than a census — already recorded as
`bounded_by: :violation`. Under workers the bound is looser and varies between runs,
because the coordinator starts a whole level at once and halts on the first violation it
receives; how much of that level was merged first depends on which worker finished when.
Two runs of the same violating spec at different worker counts agree on the verdict and on
the counterexample's **length** — which is what D-9 compares — and need not agree on the
counts. Asserting that they did would make a flaky test out of correct behaviour.

**Why the default is 1**, against §04's stated `System.schedulers_online()`. A parallel
search is exhaustive exactly as a single-threaded one is, so the cores buy speed and not a
better answer — and how much of a machine to spend on a run is a decision about the
machine, held by whoever runs the checker. `ExTLA.Config.workers/0` derives it for a caller
who asks; nothing derives it for one who did not.

**Liveness is refused alongside it**, exactly as D-22 refuses symmetry with liveness. The
edge table and ENABLED bits are per-struct maps, so a parallel run would answer a temporal
property from a graph missing the edges other workers found, and a cycle spanning two
workers would not exist to be found at all.

**Revisit if:** the corpus stops comparing counterexample length, or the edge table moves
into ETS. The first would remove the reason for the barrier; the second would remove the
reason for the liveness refusal.

See `06-architecture.md` §Concurrency Architecture, `04-layer2-model-checker.md` §Config.

**Pinned by:** `test/differential/parallel_agreement_test.exs` — a parallel run answers what the
single-threaded one answers, at 1, 2, 4 and 8 workers, including the counterexample's
length.

---

## D-28 — A bounded run makes no negative existential claim

**Decided.** A finding of the form "no reachable state has P" — a never-enabled action, a
vacuous property, an invariant never at risk — is reported **only from a complete search**.
A run stopped by `max_states`, by a `state_constraint`, or at a counterexample lists the
same data and does not accuse, and `--strict-coverage` does not fail a build on it.

**Why.** A bounded run cannot tell an action whose guard is never true from one whose
states it never reached. Reporting the first when it has only established the second sends
someone to look for a bug in a spec that may be correct, and — worse for a tool whose whole
argument is that it says what it checked — it does so in the voice of a finding.

The data stays in the report either way, because *what a run saw* is a fact about the run.
What a bounded run may not do is draw a conclusion about the spec from what it did not see.

**Recorded 2026-09-22 (#176); decided at #128**, which applied it to never-enabled actions.
Extending it to the other two negative existentials is #167's remaining work.

**Pinned by:** `test/ex_tla/coverage_test.exs` — a bounded run's never-enabled list is
reported and is not accusable.

See `04-layer2-model-checker.md` §Coverage and Vacuity.

---

## D-29 — A status names what the search did, never what it was configured to do

**Decided.** Every field of `result()` that reports an outcome is derived from
`run.outcome` or from a counter the search kept. A configuration value may explain a
status; it may not *be* one.

**Why.** `:max_states_reached` is set when the budget was hit, not when a budget was given
— and that is the shape every other status has to match. `:constrained` was the exception:
it was set whenever a `state_constraint:` was *configured*, so an exhaustive run whose
constraint never held a state back reported itself unverified, exited 2 and flunked
`assert_spec`. Seven consumers read that status and every one of them states the effect in
its own message ("bounded this run", "the numbers are a lower bound"); only the producer
read the configuration.

The exception that proves it: a refusal is configuration-time by nature — D-22 and D-27
reject a *pairing* before a search exists — and those are refusals, not statuses.

**Recorded 2026-09-22 (#176); the correction to `:constrained` is #167's remaining work**,
and it needs the search to distinguish a state held back by the constraint from one already
seen, which today share one `:hold`.

**Pinned by:** nothing yet — the assertion that a run whose constraint never fired reports
`:ok` is what #167 adds. This decision is written before its fix deliberately: it is the
rule the fix has to satisfy, and writing it afterwards would make it a description of
whatever was built.

See `04-layer2-model-checker.md` §Configuration.

---

## D-30 — Prose about an internal names it without the autolink form

**Decided.** Documentation that names a private function, a `@doc false` module or a
removed one writes it plainly — "the private `merge/2` in `ExTLA.ModelChecker.Parallel`" —
rather than in ExDoc's backticked `Mod.fun/arity` form, which is a *link claim*.

**Why.** The design documents and the decision log describe how the checker works, and
naming the function that does it is the clearest way to say so. ExDoc reads the backticks
as a request to link to a public API and warns when it cannot. Nothing had drifted in those
four cases: the convention and the prose wanted different things from the same syntax, and
the prose was right.

`CHANGELOG.md` is exempt, and that exemption is the point of stating this rule rather than
suppressing the warnings: a changelog that cannot name a removed function cannot record a
removal.

**Recorded 2026-09-22 (#176); the rewording and the CHANGELOG exemption are #156's work.**

**Pinned by:** `mix docs --warnings-as-errors` in the `docs` job (#291). A backticked
`Mod.fun/arity` naming a private, hidden or filtered thing fails the build.

The gate found this decision being broken **two days after it was written**, by the same
hand: #277's moduledoc table named `Liveness.shape/4`, `GenServer.Runtime.verdict/3` and
`Coverage.walk/3` in the autolink form, and nothing said so. That is the argument for the
gate in one example — a decision recorded and not enforced is a decision that lasts until
the next person writes a sentence.

See `02-dsl-semantics.md` §7.

---

## D-31 — The specification carries no `@spec`

**Decided.** `spec/01`–`spec/05` publish `def` heads and `@type`s, and no `@spec`. A
function's return shape is documented in the `@doc` prose beside its head, or in a `@type`
the code also declares.

**Why.** #68 removed all 244 `@spec` annotations from `lib/` with the reasoning that "a
`@spec` that has drifted from its function is worse than none, because it reads as a
checked claim". The specification's own 116 were the same class — hand-maintained, checked
by nothing, and **wrong in seventeen places**, which is what #153 found. Keeping them would
have meant either maintaining two sets of annotations by discipline or reversing #68.

So return types are the one part of the published API surface that is not mechanically
gated. That is a decision, not an oversight, and this entry is where it is recorded: names,
arities and type shapes are gated against `API_SURFACE.md`; return shapes are prose.

**Pinned by:** `test/docs/spec_api_test.exs` "so the class #68 closed in lib/ cannot return
through the document" — a `@spec` reintroduced anywhere in `spec/01`–`05` fails it.

See `02-dsl-semantics.md` §7, `API_SURFACE.md`.

---

## D-32 — An enumeration of what the code declares is a generated golden

**Decided.** A document that lists what the code declares — its functions, its switches,
its diagnostics, its dependencies — is **generated from source and byte-compared in CI**,
never maintained by hand. Seven exist. Five are gated HARD by `surface-drift`:
`TLA_COVERAGE.md`, `API_SURFACE.md`, `CLI_SURFACE.md`, `DIAGNOSTICS.md` and
`PACKAGE_SURFACE.md`. The sixth, `EXERCISE.md` (#370), enumerates what the suite
exercises, and is gated HARD by `test`: it is that job's own coverage run, and checking it
elsewhere would mean carrying the data between jobs or running the suite twice. The
seventh, `RELATIONS.md` (#354), is surfex's: every relation in spec/04's relation log and
its state. surfex writes its header and fixes its gate's name, so it is gated HARD by a job
of that name, `relation-status-drift`, which also checks the log and its evidence. Each
golden's header names its gate, and the gate is the job that runs its check.

**Why.** Every one of them replaced a hand-kept list that was wrong, and in each case the
list's wrongness was invisible: `spec/02` §7 was twenty-eight of fifty diagnostics short;
`spec/06` §Dependencies named one removed a month earlier; the published docs advertised
eleven modules a consumer cannot call; `spec_options_test` walked six tasks and there were
ten. A hand-kept enumeration does not announce that it has stopped being true.

**What this does not cover.** Prose that states a *property* — "zero required runtime
dependencies", "dev/test dependencies are not transitive" — is not an enumeration and does
not drift the way a list does. Those stay written, and the ones that carry weight are
pinned by tests.

**Recorded 2026-09-22 (#176); decided and built at #270.**

**Pinned by:** `test/mix/extla_api_surface_test.exs` "runs every golden's --check from the
job its header names" — a golden whose task can `--write` and `--check`, and whose `--check`
the job named in its header does not run, fails it, so another cannot be added ungated.
"every golden's header names a job that exists and runs its task" covers the goldens
another tool writes, such as `RELATIONS.md`, which the first test never reads.

See `06-architecture.md` §Dependencies, `02-dsl-semantics.md` §7.

---

## D-33 — A description declared is a description shown

**Decided.** A declaration that accepts `desc:` must surface it where the reader meets the
finding: an invariant's and an action property's in the violation that is raised, a
temporal property's in the refutation message its counterexample carries. D-18 says which
declarations accept the option; this says what accepting one obliges.

**Why.** #160 settled that an option nothing reads is the same defect as an unknown key,
and closed the gap by *refusing* `desc:` on the four declarations that had no reader for
it. `temporal` kept the option on the strength of a reader that did not exist: the DSL
stored the description, `compiled_temporals/1` emitted a map without it, and the property
a user was shown when their property was refuted was the bare name `:eventually_done`.
Nothing noticed, because the test written for #160 asserted that a spec carrying `desc:`
compiles — which the code that drops it does too (#225's shape E).

The same hop was missing one level down. Every finding — invariant, action property,
deadlock, liveness — writes a `message` saying what was refuted, `ExTLA.Trace.to_json/1`
carried it out to a file, and `ExTLA.Trace.format/1` printed the banner and dropped it. So
"the description reaches the struct" would have been a green test over a counterexample
that still showed the reader nothing, which is why the pin below is asserted on the
**rendering**.

**Recorded 2026-09-22 (#176); built at #276.**

**Pinned by:** `test/ex_tla/model_checker/liveness_test.exs` "a refuted property's
counterexample carries the description its author wrote", and
`test/ex_tla/model_checker_test.exs` "format/1 prints the message the finding wrote, not just
the property's name" — the hop below it.

See `02-dsl-semantics.md` §5.1, `03-layer1-invariants.md` §Macro Specification.

---

## D-34 — A block the specification shows is compiled, or says why not

**Decided.** Every `elixir` block in `spec/` and `README.md` is either compiled by the
guide harness or carries `<!-- tla:skip reason=… -->`, and the reason names **what the
block is** and, where another gate owns it, **which one**. A bare `tla:skip` is refused.

**Why.** Seventy-six fences were compiled by nothing. Most are API sketches whose
signatures `spec_api_test` already holds to `API_SURFACE.md`, so the gap was smaller than
the count suggests — but "nothing compiles this" and "something else gates this" read
identically in an unannotated block, and only one of them is acceptable. This is #156's
rule about empty spaces, applied to code fences, and `TLA_COVERAGE.md`'s about items:
something nobody verified is recorded as unverified, never omitted.

The pass found three things nobody was looking for: an **empty** `elixir` block standing
in for `ExTLA.Profile`'s API (§Per-declaration cost, since #130), and two conformance
examples — the ones a reader copies — that cannot compile, because `ExTLA.Refinement`'s
validator probes `concrete_message/2` with an empty binding and a mapping for an action
with params cannot answer it (#284).

**What the skips record, and what they are not.** Four kinds:

- an API sketch, gated by `spec_api_test` — the largest group, and not a gap at all;
- a fragment: an `action` or `invariant` declaration shown on its own, which is not a
  compilable module and is not meant to be;
- a deferred design — `ExTLA.Supervisor.Spec`, `Mix.Tasks.Extla.Gen.Test` — skipped with the
  phase that owns it, so the block reads as unbuilt rather than as broken;
- a block blocked by a defect, naming the issue. Those are the only skips that should
  disappear: when #284 lands, two of them go.

**Recorded 2026-09-23 (#178); built at #281.**

**Pinned by:** `test/guides/guide_check_test.exs` "every block in spec/ and README.md is
compiled or skipped with a reason" and "a skip with no reason is rejected".

See `spec/README.md` §How this specification stays true.

---

## D-35 — A compile-time probe draws every binding it can construct, and says it is a probe

**Decided.** `ExTLA.Refinement.validate!/3` probes the round-trip rule with **every** binding
each `init` block yields — every binding a compile can construct — and describes itself as a
probe rather than as the exhaustive check `05-layer3-conformance.md` used to promise.

**Why not fewer.** It took three bindings from the first `init` block. #169 asked whether
widening was worth its cost and refused to assume; measured across the differential corpus,
the cost is nothing:

| Spec | Bindings per action, at an initial state |
|---|---|
| `distributed_lock` | 4, 4, 4, 2 |
| `raft_election` | 3, 0, 0, 0 |
| `paxos` | 2, 0, 4, 0 |
| `two_phase_commit` | 3, 1, 1, 3, 3, 3, 3 |

Every action has between **0 and 4**, because the sets a param draws from are mostly empty
at an initial state — no messages in flight, no locks held. So the cap of three was
excluding at most one binding per action, and every spec in the corpus has exactly one
`init` block. Two restrictions, buying nothing between them.

**Why not more.** Bindings reachable later in the search cannot be drawn without running the
search, and running it at compile time is not a probe, it is the check the model checker
already performs. So this stays a probe and the specification says so — with what it draws
from, so a reader can tell what was established from what was assumed.

**Recorded 2026-09-24 (#169); built at #298.**

**Pinned by:** `test/conformance/param_mapping_test.exs` — a mapping wrong for a binding
that an `init` block yields is caught, and one whose action has no binding at all is named
in the deferred list rather than reported as checked.

See `05-layer3-conformance.md` §`ExTLA.Refinement`.

---

## D-36 — The mapping says how a message is delivered, and a cast completes at a `:sys.get_state`

**Decided.** `concrete_message/2` may return `{:call, msg}`, `{:cast, msg}` or
`{:info, msg}`; a bare term is a call. A cast's completion is observed by a **monitored
`:sys.get_state/2`**, the call both drivers already make.

**Why it had to be decided at all.** `ExTLA.GenServer.Driver.call/3` sends `{:"$gen_call", …}`
unconditionally, and it is the sole delivery path for the private `drive/5` in `ExTLA.Replay`
and `step/4` in `ExTLA.Simulation` (D-30). **`05-layer3-conformance.md`'s own canonical refinement maps
`:complete_transfer` and `:reset` to `handle_cast/2` clauses.** Delivered as a `$gen_call`
those reach `handle_call/3`, which has no matching clause; the server dies and replay reports
`:not_followed` — "the spec permits a behaviour the implementation does not take", about a
server that is fine. Nothing restricts the callback to calls, and the runtime wrapper *does*
instrument casts and infos, so the gap is exactly **checked but not drivable**.

**Why the mapping and not an inference.** A term is a message and a message does not carry
how it arrives, so a bare return cannot distinguish a call from a cast. Inferring it from
which callback has a matching clause guesses, and a message two callbacks both match is not
decidable that way. Declaring it on the spec side is the wrong layer: delivery is an
implementation detail and the specification is meant not to know one.

A bare term keeps today's meaning, so no existing mapping changes. The one ambiguity it
introduces — a mapping whose literal message *is* `{:cast, 5}` — has a total escape:
`{:call, {:cast, 5}}`.

**The hard half: when is a cast done.** A call hands the driver "answered, refused, or died"
as a value; a cast has no reply, and a driver that moved on before the cast was handled
would compare the next action against a stale state. That is #168's defect class, and it
must not be reintroduced by the fix for a different one.

`:sys.get_state/2` is a system message through the same mailbox, so it is ordered **behind**
the cast just sent: when its reply arrives, the cast has been handled. Its cost is **no
additional round-trip** — the private per-step functions of `ExTLA.Replay` and
`ExTLA.Simulation` each already call
`:sys.get_state/1` after every step to map the post-state through `abstract/1`, so for a
cast that same call does double duty. The monitor still carries the other outcomes: a
violation raised in `handle_cast/2` kills the server and arrives as the same `:DOWN`, and a
cast that never completes is a `{:timeout, ms}` — a named finding, never a silent "followed".

**Considered and rejected:** a bounded wait with no state read (it decides completion by a
clock, which makes a run's verdict depend on load); a completion signal emitted by the
runtime wrapper (more machinery for a synchronisation the mailbox already provides, and it
would only work for instrumented servers).

**Recorded 2026-09-24 (#305); built at #306**, which also added the first
conformance-corpus entry handling an action by cast — the corpus was `handle_call`-only
until then, which is why this went unseen.

**Pinned by:** `test/conformance/cast_delivery_test.exs` — an action the server takes in
`handle_cast/2` drives under both `ExTLA.Replay` and `ExTLA.Simulation`, a bare term is still a
call, a cast is handled before the driver returns, and a cast that never completes is a
`{:timeout, ms}`. `test/docs/delivery_contract_test.exs` holds the three documents to the
same forms.

See `05-layer3-conformance.md` §`ExTLA.Refinement` and `usage-rules.md`.

---

## D-37 — `mix extla.stamp --check` fails on an unverified stamp, and there is no CI job for it

**Decided.** `--check` exits 1 where a stamp is **stale**, or where its spec's source is not
on disk so **nothing verifies it**. It is a flag rather than the default, and **no CI job
runs this task**.

**The question it asks, once, of each mapping:** *is this stamp verified by something?*

| status | verified by | `--check` |
|---|---|---|
| `:fresh` | this task | 0 |
| `:stale` | this task — and it is **wrong** | **1** |
| `:unstamped` | nothing to verify; the mechanism is opt-in | 0 |
| `:unverifiable`, spec source not on disk | nothing | **1** |
| `:unverifiable`, `spec:` not a literal alias | **the compiler** | 0 |

**The last row is the finding.** A `spec:` given as `@an_attribute` cannot be resolved by a
task that reads source without compiling — that is what `:unverifiable` means here. But
`use ExTLA.GenServer` has the attribute's *value* at expansion, so the compile-time check
verifies that stamp completely. Measured rather than assumed:

    attribute spec, correct stamp:  :compiled
    attribute spec, stale stamp:    {:raised, ExTLA.Spec.CompileError}

Failing a build on it would be a **false finding about a mapping that is fully checked** —
and a false finding is how a check gets turned off.

**Why no CI job, which is what #173 asked and expected a yes to.** A stale stamp is
*already* a compile error, and a spec whose source is not on disk *already* emits a compile
warning. On any project whose CI compiles with `--warnings-as-errors` — this one does — both
failures arrive from the `compile` job, earlier and with a better message. A job running
this task would add a second way to learn the same thing, and a second place to keep in
step with the first.

So the flag's purpose is the workflow the compiler **cannot** serve: the project does not
compile, and a script wants the list of mappings to re-read rather than one error at a
time. That is the situation the task was built for — it reads source and loads nothing for
exactly this reason — and an exit code is what lets a script act on it.

**Why a flag and not the default.** The task is a *report*, and a report that exits non-zero
by default breaks every script that runs it to see the numbers. `05-layer3-conformance.md`'s
reasoning about `--restamp` does not apply here and was checked against: it says an
automatic *repair* must not be easy, because "a stamp applied without reading is worse than
no stamp". It says nothing against a build that fails on a stale stamp — arguably the
opposite, since a failing build is what makes someone read the spec diff. The default is
about not surprising a caller, not about the judgement.

**Recorded and built 2026-09-24 (#311).**

**Pinned by:** `test/mix/extla_stamp_test.exs` — `--check` exits 1 for a stale stamp and for a
spec with no source, exits 0 for an unstamped mapping and for one whose `spec:` is an
attribute, and the compile-time behaviour that makes the last row right is asserted rather
than described.

See `05-layer3-conformance.md` §`mix extla.stamp`.

---

## D-38 — One implementation of each operator, behind one façade a spec body imports

**Decided.** `ExTLA.Set` and `ExTLA.Function` hold the **only** implementation of every
set-theoretic and function operator. `ExTLA.Spec.Helpers`, which `use ExTLA.Spec`
imports into every spec body, delegates each one to them and implements none of them. It
keeps its own thin covers over `MapSet` and `Enum` — `set/1`, `put/2`, `union/2`, `len/1`,
`sum/1` and the rest — because those have no counterpart in the foundation.

The consequence a user sees: **`01-foundation.md`'s vocabulary is callable unqualified from
a spec body.** Before this, `powerset`, `cross`, `for_all?`, `exists?`, `range`,
`function_set`, `record_set` and the rest needed a fully-qualified call, and exactly one
spec in the repository made one.

**Replaced:** two implementations of four operators, side by side, with nothing comparing
them.

**Why.** They had already drifted, and in the direction the project refuses everywhere
else (#318):

- `for_each/2` refused a list **by name**, because building a function over a *sequence*
  deduplicated it silently — that is #211, fixed in one copy. `ExTLA.Function.construct/2`
  still did exactly that: a three-element sequence became a two-element function.
- `Helpers.domain/1` read a sequence as the function on `1..Len(s)` that `at/2` applies it
  as. `ExTLA.Function.domain/1` was `Map.keys |> MapSet.new`, so a list raised `BadMapError`
  — and a `MapSet`, which **is** a struct and therefore a map, was answered with the
  struct's own field names. A wrong answer that looks like an answer is the failure D-20
  exists to refuse, and it was sitting in the module `01-foundation.md` calls the
  foundation.

A test proving two implementations agree would have been the smaller change, and #318 wrote
one. It is not enough on its own: it holds them in step without saying which is right, and
the pair above disagreed about the case that matters most precisely because each had been
edited alone.

**Why a façade and not a second `import`.** #183 preferred importing `ExTLA.Set` and
`ExTLA.Function` into the spec body directly. That is not available: `domain/1`, `choose/1`
and `choose/2` exist on both sides, so a second import makes every shared name **ambiguous
at its call site**, in every spec. The collision the proposal asked us to check is real —
it is between the two modules, not with `Kernel`. Delegating through the module already
imported gives the same reachability with no collision, and one place to document the
vocabulary.

**Four operators arrive under another name, and only four.** `for_each/2` and `update/3`
are the DSL's own long-standing spellings of `construct/2` and `except_with/3`; renaming
them would break every spec written so far to buy nothing. `set_map/2` and `set_filter/2`
are `ExTLA.Set.map/2` and `filter/2`, because an unqualified `map/2` in a spec body reads as
`Enum.map/2` to every Elixir programmer who opens the file, and a set operation that
silently returns a different cardinality than its argument is the same defect class as
#211.

**Cost.** A delegation is a second name for one function, so a reader who greps for
`powerset` finds two hits. Paid for by `defdelegate` being a compile-time check that the
target exists — a renamed operator fails when ExTLA compiles rather than at a user's first
call — and by the gate below, which reads the façade's own AST and fails if any operator is
implemented there rather than delegated.

**Revisit if:** the DSL gains a way to import a vocabulary without the flat-namespace
collision, in which case the façade becomes a re-export list rather than a module of
delegations. The decision that the foundation holds the implementation does not change.

**Recorded and built 2026-09-25 (#319, for #183).**

**Pinned by:** `test/ex_tla/spec/operator_agreement_test.exs` — what a spec body can reach is
derived from `lib/ex_tla/spec.ex`'s own `__using__` imports; every operator the foundation
exports must be reachable under its own name or a written-down alias; and
`lib/ex_tla/spec/helpers.ex`'s AST is read so that a name defined there with `def` rather than
`defdelegate`, where the foundation defines one too, fails the build.
`test/differential/set_vocabulary/` checks the vocabulary against TLC, used the way an
author would use it.

See `01-foundation.md` §The vocabulary a spec body reaches and
`04-layer2-model-checker.md` §Helper Functions Available in DSL Blocks.

---

## D-39 — Totality over a bounded domain is a list comparison, not a probe

**Decided.** Whether `concrete_message/2` covers every action the spec declares is answered
by **comparing two lists**: the spec's actions, against the first argument of every clause,
recorded as the mapping compiles by an `@on_definition` hook that `use ExTLA.Refinement`
installs. `ExTLA.Refinement.validate!/3` never calls the callback to find out.

**Replaced:** calling `concrete_message(action, params)` for each action and reading what
came back. A mapping with **no clause** for one of them therefore raised
`FunctionClauseError` from inside the validator, where the contract is a
`ExTLA.Refinement.Error` with a sentence naming the action — which is exactly what that rule
exists to report (#299).

**Why not the precedent one function up.** `abstract_action/1`'s totality *is* established
by a probe, and the obvious move was to make the two symmetric. It is the wrong analogy,
for a reason that decides the general case:

| | `abstract_action/1` | `concrete_message/2` |
|---|---|---|
| domain | any message a server might receive | the spec's actions |
| size | unbounded | known, and in `validate!/3`'s hand |
| how to ask | a probe term no clause can have anticipated | read the clauses, compare the lists |

A probe over an unbounded domain is the only instrument available, and its limits are why
that one is documented as "a probe, not a proof". Over an **enumerable** domain a probe is
strictly worse than the comparison: it decides nothing the comparison does not, it needs a
binding the comparison does not, and it gets its answer by running user code that may raise
for reasons of its own.

The binding is not a detail. The private `sample_params/3` yields nothing for an action with params
where the constants have no value — the ordinary shape of a published example (D-35) — so
the probe **skipped** those actions, and a missing clause for one of them validated clean.
The comparison decides them all.

**And not `try/rescue` at the call site**, which was the other option on the table.
CLAUDE.md forbids it, and here it is also undecidable: a `FunctionClauseError` raised
*because the mapping has no clause* is indistinguishable at the call site from one raised
*inside a clause that does exist* — which is #315's defect verbatim, one function over, and
the reason the private `total!/1`'s rescue had to be narrowed to a single stack frame.

**A variable first argument reads as total.** `def concrete_message(action, params)` covers
every action, and the hook can see that its first argument is not a literal atom. Anything
that is not a literal atom — a variable, a match, a guarded variable — is recorded as
covering everything. A hook that read a variable as covering nothing would report a
**complete** mapping as incomplete, and a false finding about correct code is worse than
the crash this replaced. The cost is the other direction: `def concrete_message(action, _)
when action in [:a, :b]` reads as total and its gap is left to the round-trip probe. That
is the right way round for a rule whose failure mode is an author being told their correct
mapping is wrong.

**Three shapes stay distinct**, which the crash had collapsed into two. Defining **none** is
legal — `@optional_callbacks [concrete_message: 2]`, the shape `Counter.Impl.Undrivable`
rests on — and is reported as an undecided rule rather than a fault. Defining **all**
passes. Defining **some** is the finding, and it names the actions it does not cover.

**Cost.** The record only exists where the mapping `use`d the module. One that writes
`@behaviour ExTLA.Refinement` by hand has nothing to compare against, and rule 5 is named in
the deferred list for it rather than claimed — the same answer the two runtime rules get,
for the same reason.

**Recorded and built 2026-09-26 (#321, for #299).**

**Pinned by:** `test/conformance/param_mapping_test.exs` — a mapping missing a clause is an
error naming the action, including for an action with no binding to probe with; one whose
only clause has a variable first argument validates as total; one defining none still
validates and says the rule went unchecked; and a hand-declared behaviour is named as
unrecorded. `test/conformance/conformance_test.exs` holds the corpus mutant
`Counter.Mutants.NoClauseForAction`, one door over from `ActionNeverNamed`, which names an
action wrongly rather than not at all.

See `05-layer3-conformance.md` §`ExTLA.Refinement`.

---

## D-40 — Every module lives under `ExTLA`, the library's own name

**Decided.** ExTLA defines its modules under `ExTLA`: the library itself is `ExTLA`, and
everything else is `ExTLA.<Something>`. The application, package and repository stay
`:extla`. The one exception is Mix tasks, which live under `Mix.Tasks`, where Mix finds them.

**Replaced:** the `TLA` namespace (`TLA`, `TLA.ModelChecker`, `TLA.Spec`, …), which nothing
had chosen. No decision here named it; it was where the first module happened to be put.

**Why.** Elixir's code anti-patterns name this one *namespace trespassing*: a library should
use its name as the prefix of every module, because the VM loads only one module per name,
so two libraries that define the same module cannot both be used. `TLA` is the most generic
name a TLA+ library could take: a TLC wrapper, a parser or another checker would reach for
it first, and whichever loaded second would silently replace the other's modules.

**Why `ExTLA` and not `Extla`.** `:extla` camelizes to `Extla`, but the project's name is
ExTLA, and Elixir keeps acronyms capitalised in aliases (`Mix.SCM`, `ExUnit.CaptureIO`).
Files follow the module: `lib/ex_tla.ex`, `lib/ex_tla/…`, as `Macro.underscore/1` gives.

**No compatibility shims.** Keeping `TLA.*` modules that delegate to `ExTLA.*` for a release
would be the trespass itself, and the DSL's macros (`use TLA.Spec`) do not delegate cleanly.
ExTLA is pre-1.0, so the move is a minor version (0.4.0), and `CHANGELOG.md` carries the
migration.

**Unchanged:** telemetry events, already `[:extla, …]`; the application environment
(`:extla`); the TLA+ language's names in prose ("TLA+", "TLC", "a TLA formula");
`TLA_COVERAGE.md`, whose name is about TLA+ verification, not the module.

**Recorded and built 2026-10-03 (#338, for #337).**

**Pinned by:** `test/ex_tla/namespace_test.exs` — every module the compiled application defines
from `lib/` or `ledger/` is `ExTLA`, `ExTLA.*` or `Mix.Tasks.*`, with an anti-vacuity test
that the walk finds the library, the ledger tooling and the Mix tasks.

See `CHANGELOG.md` for the migration a consumer applies.