TLX - TLA+ formal verification for Elixir via a Spark DSL

Your Libraries & OS Mentoring Libraries
1

TLX lets you write TLA+/PlusCal formal specifications in Elixir syntax and verify them with TLC, the TLA+ model checker. It’s built on Spark and targets Elixir developers who want to verify their state machine designs without learning TLA+ syntax.

What it does

You define specifications using an Elixir DSL — variables, actions with guards and transitions, invariants, temporal properties, concurrent processes — and TLX emits valid TLA+ or PlusCal that TLC can model-check. TLC exhaustively explores every reachable state, finding bugs that testing and code review miss: race conditions, deadlocks, invariant violations, liveness failures.

import TLX

defspec TrafficLight do

  action :to_green do
    guard(e(color == :red))
    next :color, :green
  end

  action :to_yellow do
    guard(e(color == :green))
    next :color, :yellow
  end

  action :to_red do
    guard(e(color == :yellow))
    next :color, :red
  end

  invariant :valid_color, e(color == :red or color == :green or color == :yellow)
end

mix tlx.emit TrafficLight          # emit TLA+
mix tlx.check TrafficLight         # run TLC model checker
mix tlx.simulate TrafficLight      # Elixir random walk (no Java needed)
mix tlx.watch TrafficLight         # auto-simulate on file changes

Features

  • Elixir DSL — variables, constants, actions, guards, branches, processes, invariants, temporal properties, refinement checking
  • Multiple outputs — TLA+, PlusCal (C and P syntax), Elixir round-trip
  • Expression system — e() macro captures Elixir expressions as TLA+ AST. Supports if/else, quantifiers (forall, exists), set operations, function application (at, except), CHOOSE, CASE, LET/IN, sequences, records, implication, and more
  • Elixir simulator — mix tlx.simulate gives fast feedback without Java. Good for rapid iteration during design
  • TLC integration — mix tlx.check runs the real model checker. Parses results, formats counterexample traces
  • Refinement checking — verify that a concrete spec (from code) satisfies an abstract spec (from design) via refines blocks
  • Spec discovery — mix tlx.list finds all spec modules in your project
  • File watcher — mix tlx.watch auto-recompiles and re-simulates on changes
  • Import — mix tlx.import parses TLA+ or PlusCal back into TLX DSL
  • Skeleton generator — mix tlx.gen.from_state_machine generates a spec from a GenStateMachine module
  • Agent skill — a formal-spec workflow skill for AI-assisted specification, shipped via usage_rules

Background

I’m not a TLA+ expert. I’m an Elixir developer who wanted to prove a large project’s design was correct. I’ve known about TLA+ for years — used at Amazon, Microsoft, MongoDB to find bugs in distributed systems — but the syntax was a barrier. TLX is the tool I wished existed: write specs in Elixir, let the DSL handle the TLA+ translation.

The project was built using AI-Assisted Project Orchestration patterns. 192 unit tests + 87 integration tests (SANY and pcal.trans validated). Full Diátaxis documentation.

If you’re a TLA+, formal methods, or Spark/Ash expert and find this useful, I’d welcome collaborators.

Links

3 Likes