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 teaches the same ground in order. The DSL itself is in the DSL reference, 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 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:

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:

{
  "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:

"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:

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

Together:

# 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 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.

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:

# 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

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:

# 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: the full design, the normative account behind every page here.
• Design decisions: why ExTLA is shaped the way it is, decision by decision.
• Prior art: the other verification tools for Elixir and Erlang, and where ExTLA fits among them.