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

[Andrew Helwer]

Hi Georges,

Is the input DSL itself a subset of valid Elixir code? Thanks,

Andrew Helwer

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/19402c53-e0d8-4aac-9115-c006c23f2da3n%40googlegroups.com.

[Georges Martin]

Hello, Andrew.

Is the input DSL itself a subset of valid Elixir code? Thanks,

Yes. But… 🙂

Elixir compiles to the BEAM virtual machine, and provides a macro system to generate or transform code at compile-time [1].

Elixir libraries usually take advantage of this to provide high-level, declarative, and often pipeline-oriented, DSL. [2] [3]

In TLX, I'm using the Spark[4] library to provide a specification DSL, based on TLA+ constructs like defspec, variables/constants, actions, awaits/guards, next, branches, invariants, refines, etc.

Under the hood, the spec is transformed to an IR (based on Elixir structs) that is used by TLX Emitters to output TLA+, PlusCal, DOT, mermaid, D2,... or by tools like the TLX Simulator. TLX Extractors and Importers can also generate IR from TLA+ specs or State Machines from Elixir code.

HTH,

Georges

---

[1] see the meta-programming section in the Elixir docs: https://hexdocs.pm/elixir/main/quote-and-unquote.html

[2] Plug, a specification for composing web applications with functions: https://hexdocs.pm/plug/readme.html#hello-world-websockets

[3] Ash, a declarative application framework: https://hexdocs.pm/ash/what-is-ash.html

[4] "Spark is a framework for creating declarative domain-specific languages in Elixir. It transforms simple struct definitions into rich, extensible DSLs that come with autocomplete, documentation generation, and sophisticated tooling built right in." (https://github.com/ash-project/spark?tab=readme-ov-file)

[Irwansyah Irwansyah]

Unfortunately, the whole point of using TLA+ is we can go straight forward attacking the problem without having to deal with setting up developnent environment that came with progrramming languages

--

You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/351DFFB1-ADFB-4DAA-B37C-9784B71E5B65%40gmail.com.

[Georges Martin]

Hello,

> Le 12 avr. 2026 à 09:57, Irwansyah Irwansyah <irwa...@gmail.com> a écrit :
>
> Unfortunately, the whole point of using TLA+ is we can go straight forward attacking the problem without having to deal with setting up developnent environment that came with progrramming languages

I understand, and don't question that.

TLX reads and emits TLA+ and PlusCal, and calls TLC. Its DSL is based on TLA+. I'm not reinventing the wheel, and don't intend to: I am neither a formal specs expert nor a mathematician.

That said, even though I have a long experience with Perl, LaTeX, XSLT, and a bit of Erlang, I found the syntax (not the concepts) of TLA+ and PlusCal, well... much more intimidating 😅 I also have experience with Smalltalk, Python and Elixir, so I understand the importance of Developer Experience -- DX.

Thus, with TLX, I just tried to improve the TLA+ DX (it worked for me), make formal specs usage frictionless in Elixir projects (it worked in my project), prove a large, distributed, Elixir project design and implementation were correct (TLC found one bug and one design ambiguity, so it worked for me), and integrate formal specs verifications into CI (it worked ! 🥳).

So, I tried to make TLX a good citizen in the TLA+ ecosystem. And simply decided to open source it. That's all.

Thanks for your feedback 🙂

Georges

[Andrew Helwer]

Thanks Georges, very interesting. I do not know Elixir but have long wanted to learn a BEAM VM language. If you write a TLX spec, do you think it is possible for the code to function as both a spec and some base for an implementation of the full system in Elixir?

Andrew

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/tlaplus/BB88B7B6-F487-4701-BC89-1AAE241B3E5A%40gmail.com.