TLX — TLA+ specifications in Elixir syntax, with TLC integration

[Georges Martin]

Hi all,

I've published TLX, an open-source Elixir library that provides a DSL for writing TLA+/PlusCal specifications. It emits valid TLA+ and PlusCal (both C and P syntax)  for TLC model checking.

I want to be upfront: I'm not a TLA+ expert. I'm an Elixir developer working on infrastructure with complex state machines (concurrent provisioning, reconciliation  loops, approval workflows). I've been aware of TLA+ for years and knew it was the right tool, but the syntax barrier kept me from adopting it. TLX is my attempt to bridge that gap for the Elixir/Erlang ecosystem.

What it does:

Elixir developers write specifications using a declarative DSL:

  defspec BoundedCounter do
    variable :x, 0

    action :increment do
      guard(e(x < 5))
      next :x, e(x + 1)
    end

    invariant :bounded, e(x >= 0 and x <= 5)
  end

TLX emits standard TLA+:

  ---- MODULE BoundedCounter ----
  EXTENDS Integers, FiniteSets
  VARIABLES x
  vars == << x >>

  Init == x = 0
  increment == /\ x < 5 /\ x' = x + 1
  Next == \/ increment
  Spec == Init /\ [][Next]_vars
  bounded == (x >= 0 /\ x <= 5)
  ====

Then mix tlx.check invokes TLC via tla2tools.jar, parses the -tool mode output, and reports violations with formatted counterexample traces.

TLA+ coverage:

Variables, constants, actions (guards, transitions, UNCHANGED), processes, non-deterministic choice (either/or, pick from set), invariants, temporal properties  (always, eventually, leads_to), fairness (WF/SF), quantifiers, IF/THEN/ELSE, LET/IN, CHOOSE, CASE, set operations (union, intersect, subset, cardinality,  comprehension), function application and EXCEPT, records, sequences (Len, Append, Head, Tail, SubSeq), DOMAIN, implication/equivalence, range sets, configurable  EXTENDS, and refinement checking via INSTANCE/WITH.

Not supported: RECURSIVE operators, LAMBDA, multi-module composition beyond refinement, TLAPS proofs.

Emitted output is validated against SANY and pcal.trans in the test suite (87 integration tests). The emitters are not just string concatenation — they use a shared  AST formatter parameterized by symbol tables.

Also includes:

• An Elixir simulator (mix tlx.simulate) for fast feedback without Java
  
• NimbleParsec-based importers for TLA+ and PlusCal (converts back to the DSL)
  
• Refinement checking (concrete spec refines abstract spec)
  
• A formal-spec agent skill for AI-assisted specification workflows

I'd value feedback from this community. If the TLA+ emission has issues I haven't caught, or if there are better ways to map certain constructs, I'd like to hear about it.

GitHub: https://github.com/jrjsmrtn/tlx
Package: https://hex.pm/packages/tlx
Docs: https://hexdocs.pm/tlx