ExTLA

The problem

Concurrency bugs live in message orderings. A GenServer written by an LLM can pass every test, because the tests try the orderings its author thought of, and those are the ones the code already handles. A fix for one race can leave the same race one call over, and nothing notices.

ExTLA checks every ordering instead. You state what the system may do, and what must never happen, in a few dozen lines of Elixir that a person can read and agree with. In LLM-assisted development this changes the division of labour: a model can draft the specification, the checker validates it exhaustively within the bounds you set, and code is then held to the checked model. A green run means what it says, whether a person or an agent is reading it.

How it works

The design has layers, each useful on its own:

• Foundation. Core types and operators: states, sets, functions, temporal operators, and state fingerprints.
• Runtime invariants. Design-by-contract checks for GenServers and other OTP behaviours. When turned off they compile to no code at all.
• Specification DSL and model checker. A specification declares variables, an initial state, actions, and invariants and temporal properties. The checker explores the reachable state space and reports the shortest counterexample to any broken rule.
• Conformance. ExTLA.GenServer links an implementation to its specification and checks that every step the code takes is a step the specification allows, through a refinement mapping. Random simulation, counterexample replay and captured-trace replay drive the real process against the model.

One principle runs through all of it: never claim more than was checked. An incomplete run fails. A bounded run says it was bounded. A run also reports which actions it never enabled, so a pass that exercised nothing does not look like a pass that exercised everything.

The project is clear about what it is not. It is not a theorem prover, it does not extract models from source code, and it does not generate implementations from specifications.

Getting started

Add the dependency to mix.exs:

def deps do
  [
    {:extla, "~> 0.6.0"}
  ]
end

A specification is an Elixir module:

defmodule Specs.Counter do
  use ExTLA.Spec

  variable :count, type: 0..3
  variable :status, type: [:ready, :busy]

  init do
    count = 0
    status = :ready
  end

  action :start do
    require status == :ready and count < 3
    status = :busy
  end

  action :finish do
    require status == :busy
    count = count + 1
    status = :ready
  end

  invariant :in_bounds do
    count <= 3
  end
end

Check it:

mix extla.check Specs.Counter

Other tasks run random traces of an ExTLA.GenServer against its specification (mix extla.simulate), drive the code through a counterexample or a captured trace (mix extla.replay), evaluate expressions over a saved counterexample (mix extla.explore), and render the state graph as DOT (mix extla.visualize). ExTLA has no required runtime dependencies. Jason is optional and enables JSON output.

The documentation includes a half-hour getting-started guide, an eleven-page tutorial built around a single lock example, a TLA+ primer for newcomers, and the full design specification with its recorded design decisions.

Status

Experimental. The checker agrees with TLC, the reference TLA+ model checker, on every specification in its differential test corpus. The interface can still change between minor versions before 1.0, as it did in v0.4.0. Each changelog entry explains how to upgrade. The current release line is 0.6. ExTLA is MIT licensed.