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