# Reference The facts a user of ExTLA looks up rather than learns: how `mix extla.check` differs from calling the checker yourself, the levers that make a large state space tractable and what each one costs, how to read a coverage report and a JSON result, what conformance checks, how Layer 1 behaves in tests and in production, and what ExTLA deliberately does not do. The [tutorial](tutorial/00-introduction.md) teaches the same ground in order. The DSL itself is in the [DSL reference](../spec/02-dsl-semantics.md), and every module's options are on its own page — start at `ExTLA`. ## The CLI and the API `mix extla.check` and `ExTLA.ModelChecker.run/2` run the same checker. One default differs. **The CLI infers `check_liveness`; the API does not.** `ExTLA.ModelChecker.run/2` defaults it to `false`. `mix extla.check` sets it to `true` when the spec declares a `temporal` and none of `--safety-only`, a `symmetry:` declaration or `--workers` above one applies. The task has the spec in hand and can tell that liveness is what the author meant; a library caller gets exactly what they wrote. So a temporal property `mix extla.check` checks is **not** checked by `ExTLA.Spec.Test.assert_spec/2` unless its config says `check_liveness: true`. A suite can be green over a temporal property nothing evaluated. **A liveness pass that was asked for and did not run is named.** Liveness runs over a finished graph, so four things skip it: a deadlock, a `state_constraint:` that held states back, the state budget stopping the search, and a safety counterexample halting it. Each adds one warning to the result — "N temporal properties were not checked", with the reason and what to do — and the status is whatever the search produced. That matters most under `--allow-incomplete`, which turns a bounded run into exit 0. ## Making a large state space tractable [When the state space explodes](tutorial/09-when-it-explodes.md) is the order to reach for these in. This is what each one does and what it asks of you. ### State constraints `state_constraint:` is a predicate on states; a state that fails it is not expanded. It bounds an otherwise unbounded variable — a growing log, an unbounded counter — without changing the spec: ```elixir state_constraint: fn s -> length(s.log) <= 5 end ``` A constrained run is **not** exhaustive, and the result says so: the status is `:constrained`, the coverage report names the bound, and a temporal property is not checked under it. ### Symmetry `symmetry:` names constants whose elements are interchangeable — process IDs, account names, replica IDs. States that differ only by a permutation of those elements are treated as one, so a symmetric set of size *n* shrinks the reachable space by up to *n*!. **What it costs.** Each state is put in a canonical form by trying every permutation: *n*! encodings per state for one symmetric set, and the product for several. At three elements that is roughly a wash in wall-clock time; at four or five it is a clear win. Measure it on your spec rather than assuming it. **Soundness is your obligation.** The reduction is sound only if no property and no action can tell the elements apart: no `Enum.at(^accounts, 0)`, no `Enum.sort`, no `<` between process names, nothing that depends on list position. Nothing can check this statically — a constant flows into arbitrary Elixir, and any conservative check would reject the `Enum.all?(^processes, …)` almost every symmetric spec is built from. It is the author's obligation, exactly as it is in TLC. What ExTLA does is make a wrong declaration **detectable**. `mix extla.check --verify-symmetry` (`verify_symmetry: true`) runs the model with and without the reduction and fails if any verdict differs: the status, what was refuted, whether it deadlocked, which actions were never enabled. The state counts are not compared, because a sound reduction changes them on purpose. Run it once per spec on a small constant assignment before trusting the reduction on a large one. It refuses to compare a run that hit the state budget or a constraint, because a truncation is not a verdict. **Not together with liveness.** The reduced graph identifies states, so a path that leaves an orbit and one that returns to it look alike, and the quotient can hold cycles the real system does not — which is exactly what a liveness verdict is read off. Asking for both raises. Check safety under the reduction, and the temporal properties in a run without it. ### Parallel exploration `--workers N` (`workers: N`) expands each breadth-first level across N processes and waits for all of them before starting the next. That barrier is what keeps the counterexample the **shortest** one: a parallel run may return a different trace than a single-threaded run, but never a longer one. Every coverage field except `distinct_generated`'s split across actions comes out exactly as a single-threaded run's. The default is 1. A parallel search explores the same space and gives the same answer, so the cores buy speed and not a better result, and how much of a machine to spend is the caller's decision. `ExTLA.Config.workers/0` returns the machine's answer if you want it. Liveness is refused under workers, for the same kind of reason it is refused under symmetry: a cycle spanning two workers' states would not be found. A run that halts at a counterexample under workers agrees with a single-threaded run on the verdict and the counterexample's length, not on the counts. ### What is not provided View abstraction (TLC's `VIEW`) is deferred: it is easy to make unsound, and symmetry covers the common case. Partial-order reduction is a non-goal — Concuerror already does it at the level where it pays off. ## Reading the coverage report A run can report success while having verified almost nothing, and the coverage report is how you tell. It names three things: - **An action that was never enabled.** A typo in a guard turns an action off entirely, and the spec still verifies — a weaker spec passes more easily. This is the most common finding. - **A vacuous property.** `P ~> Q` where `P` never holds in any reachable state is trivially true and says nothing about `Q`. Under a quantifier, each instance is reported on its own. - **An invariant that was never at risk.** One whose near-miss count is 0: no reachable state came close to falsifying it. Such an invariant is indistinguishable from `true`. A near-miss count is measured only for an invariant whose top level is an `or`; anything else reports `nil`, meaning "not measured", which is not the same as 0. `--strict-coverage` fails the build on a never-enabled action or a vacuous property. It does so only where the run can support the claim: "no reached state did X" says nothing about the states a bounded run never reached, so on a bounded run these stay in the report, qualified, and do not fail anything. Reading a counterexample is covered in the tutorial; `mix extla.explore` evaluates your own expressions over a saved one. ## The JSON result schema `mix extla.check --format json` emits a versioned envelope, so a reader can refuse a shape it does not know rather than misread it: ```json { "schema_version": 3, "specs": [ { "spec": "Specs.TransferProtocol", "status": "ok", "message": null, "distinct_states": 3612, "states_found": 9004, "transitions": 12871, "diameter": 14, "deadlock": false, "duration_ms": 812, "fingerprint_bits": 64, "collision_estimate": 1.0e-9, "warnings": [], "coverage": { "actions": {"begin_transfer": {"enabled_in": 44, "states_generated": 88, "distinct_generated": 61}}, "never_enabled": ["cancel_transfer"], "invariants": {"type_ok": {"evaluated_in": 3612, "near_misses": null}}, "vacuous": [], "terminal_but_live": [], "terminals": {"all_done": {"admitted": 6}}, "bounded_by": "none" }, "profile": null, "violation": null } ] } ``` Four rules the schema keeps: 1. **`schema_version` leads the envelope.** Refuse a version you do not recognise. 2. **`specs` is a list of self-describing entries**, sorted, so two runs diff cleanly. 3. **Every entry carries every key, and absent is `null`, never `0`.** A zero near-miss count is a finding; not having measured near-misses is not. 4. **A bounded run is marked.** `coverage.bounded_by` is `none`, `state_constraint`, `max_states` or `violation`; anything but `none` means the counts are lower bounds. `duration_ms` is wall time and varies between runs, so nothing should gate on it. `profile` is `null` unless the run was asked for one with `--profile`. When present it carries `run_reductions`, `otp_version`, `calibration` and `declarations`, a sorted list of entries: ```json "profile": { "run_reductions": 84117, "otp_version": "29", "calibration": {"2": 1, "3": 1}, "declarations": [ {"kind": "invariant", "name": "conservation_of_money", "evaluations": 3612, "reductions": 505680, "per_eval": 140, "observed": 511204} ] } ``` `reductions` is `per_eval * evaluations`, where `per_eval` is the cheapest evaluation observed rather than the mean — that is what makes it reproducible under machine load. `observed` is what the counter actually accumulated; a large gap between the two marks a predicate whose cost varies with the state. Unlike `duration_ms`, the declaration costs are a function of the code, the data and the OTP release, so two runs of an unchanged spec on one build agree to within two reductions per evaluation. A reduction count is comparable only within one OTP release, which is why `otp_version` is carried. `ExTLA.Profile` explains the measurement. ## What conformance checks Layer 3 maps a running GenServer's state onto the spec's, and checks every step the implementation takes: | Check | Question | |---|---| | **Step legality** | Is the abstract post-state what the named spec action produces from the abstract pre-state? | | **Stuttering** | If the message maps to no action, did the abstract state stay put? | | Invariants | Does the abstract post-state satisfy the spec's invariants? | | Action properties | Does the abstract step satisfy the spec's action properties? | | Temporal | Does the accumulated abstract behaviour satisfy the temporal properties? | Step legality is what makes this refinement checking rather than a projection with some predicates on it. Without it, an implementation could take a transition no spec action permits, and as long as the resulting state satisfied the invariants nothing would notice — and the transition the design never sanctioned is where the interesting bugs are. It is also cheap: an action body is a pure function of the pre-state and its parameters, so checking it is one function application and one comparison per callback. **A temporal property over a finite trace has three verdicts.** A trace is a prefix of an infinite behaviour. A prefix can refute `always P` or satisfy `eventually P`, but not the other way round, so `ExTLA.Temporal`'s operators return `:holds`, `:violated` or `:inconclusive` rather than a boolean. A lasso — a prefix plus a cycle that repeats — describes an infinite behaviour, and over one every operator answers definitely. Without one, `<>[]P`, `[]<>P` and `P ~> Q` are `:inconclusive` for every trace. ExTLA checks refinement on the behaviours it observes. It does not prove it. ### The verification pipeline | Mode | When | What it does | |------|------|--------------| | Exhaustive | `mix extla.check` | model checks the spec itself | | Runtime | every transition, in dev and test | step legality, stuttering, invariants and action properties | | Simulation | `mix extla.simulate`, or `ExTLA.Simulation` in tests | random walks over the real implementation, all property kinds | | Replay | `mix extla.replay`, or `ExTLA.Replay` in tests | drives the implementation through a counterexample or a captured trace | Together: ```sh # 1. Model check the spec: design bugs, before the code exists mix extla.check Specs.TransferProtocol # 2. Check the implementation conforms, over random traces mix extla.simulate MyApp.TransferServer --traces 10000 # 3. Replay the counterexample from step 1 against the real code mix extla.replay MyApp.TransferServer --trace counterexample.json # 4. Check a captured production trace against the spec mix extla.replay MyApp.TransferServer --captured incident.json ``` Step 3 turns a design-level counterexample into an executable reproduction, and step 4 lets a specification say something about the system that is actually running. `ExTLA.PropertyTest` derives StreamData generators from the spec for your own property tests beside these. [Putting a specification in your project](tutorial/10-in-your-project.md) covers running all of it from your suite. ## Layer 1 in tests and in production ### Testing helpers `use ExTLA.Invariant.Test` brings in: - `assert_invariants(module, state)` — every invariant of `module` holds for `state`. On failure it names every invariant that failed, not just the first. - `assert_action_properties(module, old, new)` — every action property holds for the step. - `refute_invariant(module, name, state)` — the named invariant **fails** for `state`. This is the test that proves an invariant can fail at all; one no test has seen return false is indistinguishable from `true`. - `valid_states(module, type_invariant, base_generator)` — a StreamData generator of states the named invariant accepts. It filters `base_generator` rather than constructing states, so the base generator should already have the type's shape and be accepted at least about half the time; at much lower acceptance rates a property fails on some seeds with `StreamData.FilterTooNarrowError`. Each helper raises, rather than failing, when the module carries no predicates — it does not `use ExTLA.Invariant`, or was compiled under `mode: :disabled` — and `refute_invariant/3` raises for a name the module does not declare. Otherwise a renamed declaration would turn a test green by making it check nothing. ```elixir defmodule BankAccountTest do use ExUnit.Case use ExTLA.Invariant.Test test "a withdrawal keeps the invariants" do state = %{balance: 100, status: :active, transactions: []} new_state = %{state | balance: 50, transactions: [{:withdraw, 50}]} assert_invariants(BankAccount, new_state) assert_action_properties(BankAccount, state, new_state) end end ``` ### Telemetry If `:telemetry` is loaded, Layer 1 emits: ```elixir # Always: [:extla, :invariant, :violated] # metadata: %{module: m, name: n, violation: v} [:extla, :action_property, :violated] [:extla, :precondition, :violated] [:extla, :postcondition, :violated] # Only under `config :extla, telemetry: :verbose`: [:extla, :invariant, :checked] # metadata: %{module: m, name: n, duration: d} [:extla, :action_property, :checked] [:extla, :precondition, :checked] [:extla, :postcondition, :checked] ``` Success events are off by default because they are the hot path: `:telemetry.execute/3` costs around a microsecond even with no handler attached, and one transition can fire four. The setting is read at compile time, so without `:verbose` the success events are not emitted at all, rather than emitted and ignored. ### Performance | Mode | Overhead | Notes | |------|----------|-------| | `:disabled` | none | no wrapper is emitted; the module compiles as written | | `:enabled` | about 1–5 µs per transition | dominated by the predicates themselves | | `:log_only` | about 1–5 µs per transition | the same, without the raise | That is a target for ExTLA's own overhead, not a guarantee: a predicate that walks a 10,000-element list costs what it costs. Three levers when checking is too expensive: ```elixir # 1. Compile one check out, per invariant invariant :expensive_check, enabled: Mix.env() == :test do deep_structural_audit(state) end # 2. Restrict it to some callbacks invariant :queue_bounded, callbacks: [:handle_cast] do length(state.queue) <= 1000 end # 3. Turn the layer off for an environment config :extla, mode: :disabled ``` An `Agent`'s checks are the exception: an `Agent` has no callback module to instrument, so `ExTLA.Invariant.Agent` dispatches at runtime and `:disabled` cannot compile them away. ## What ExTLA is not Each of these has a better tool already. - **Not a theorem prover.** ExTLA checks bounded models exhaustively and observed behaviours concretely. It does not prove a spec correct for all parameters, and it does not prove that an implementation refines a spec — it checks that the behaviours it saw did. TLAPS proves; ExTLA checks. - **It does not explore process interleavings in running code.** It finds design bugs in a state machine, not scheduling bugs in an implementation. Concuerror does that, on unmodified tests; the two are complementary. - **It does not extract models from source.** Specs are written, not inferred. - **It does not generate implementations from specs.** That is Erla+. - **No real-time or probabilistic extensions.** No clocks and no distributions. Supervision trees are not modelled yet: `ExTLA.Supervisor.Spec` is deferred, because faithful OTP restart semantics is a research-scale problem. ## Further reading These are the project's own records, on GitHub: - [The specification](https://github.com/dcoai/extla/blob/main/spec/README.md): the full design, the normative account behind every page here. - [Design decisions](https://github.com/dcoai/extla/blob/main/spec/08-decisions.md): why ExTLA is shaped the way it is, decision by decision. - [Prior art](https://github.com/dcoai/extla/blob/main/spec/00-prior-art.md): the other verification tools for Elixir and Erlang, and where ExTLA fits among them.