TLX

A Spark DSL for writing TLA+/PlusCal specifications in Elixir, with TLC model checking and an optional Elixir simulation mode.

What TLX provides

The TLX library — an Elixir DSL for defining state machines, invariants, temporal properties, and refinement mappings. Emits TLA+, PlusCal (C and P syntax), and Elixir (for round-trip). Includes NimbleParsec importers, an Elixir simulator, and TLC integration.

The formal-spec agent skill — a structured workflow for AI-assisted formal specification, distributed as an agentskills.io-compliant skill via usage_rules. Teaches the full lifecycle from ADR to refinement-checked specs.

About TLA+

TLA+ is a formal specification language designed by Leslie Lamport for modelling concurrent and distributed systems. It is used at Amazon, Microsoft, MongoDB, CockroachDB, and others to verify correctness of critical infrastructure. TLX makes TLA+ accessible to Elixir developers without requiring them to learn TLA+ syntax directly.

TLA+ Home Page — Leslie Lamport’s reference
TLA+ Foundation — independent non-profit advancing TLA+ adoption
Learn TLA+ — community learning resource by Hillel Wayne

Workflows

1. Manual specification

Write specs directly in the TLX DSL, emit TLA+, verify with TLC:

import TLX

defspec MySpec do
  variable :x, type: :integer, default: 0

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

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

mix tlx.emit MySpec --format tla    # emit TLA+
mix tlx.check MySpec                # run TLC
mix tlx.simulate MySpec --runs 100  # Elixir random walk

2. AI-assisted specification

Use the formal-spec skill to guide the process:

Read the ADR, extract states/transitions/invariants
Write the abstract spec (design intent)
Generate a concrete spec skeleton from code (mix tlx.gen.from_state_machine)
Enrich the skeleton with guards, branches, invariants
Add a refines block to verify the concrete spec satisfies the abstract
Run TLC refinement checking

The skill provides the workflow checklist, common TLX patterns, and working examples. Any coding assistant that supports agent skills can use it.

The ideal workflow

Design — write an abstract TLX spec from your ADR, verify with TLC (catches design bugs before code exists)
Implement — write the code, guided by the verified spec
Verify — write a concrete TLX spec from the code, refinement-check against the abstract spec (proves the code matches the design)

Shared tooling

Both workflows use the same mix tasks:

mix tlx.emit — emit to TLA+, PlusCal, or Elixir
mix tlx.check — full pipeline: emit, translate, run TLC
mix tlx.simulate — Elixir random walk simulation
mix tlx.watch — auto-simulate on file changes
mix tlx.list — discover spec modules in the project
mix tlx.import — import TLA+ or PlusCal back to TLX DSL
mix tlx.gen.from_state_machine — generate spec skeleton from GenStateMachine

Installation

def deps do
  [{:tlx, "~> 0.3.0", only: [:dev, :test]}]
end

To install the agent skill in your project:

# In your mix.exs usage_rules config
usage_rules: [
  file: "AGENTS.md",
  skills: [
    location: ".claude/skills",
    package_skills: [:tlx]
  ]
]

Then run mix usage_rules.sync.

Status

Active development. Not yet published on Hex.

Documentation

License

MIT