Skip to content

paralin/tla

v0.1.0MIT

Model your whole program in TLA+, with each spec beside the code it describes, checked by tla-ts. Then simplify the spec and the code together.

GitHubOpen Website

tla-skill

An agent skill for writing software whose state you can trust. It teaches a coding agent to model the whole program in TLA+, keep each spec in a .tla file beside the code it describes, check every spec with tla-ts on every build, and use the model and the code together to make both simpler.

Agents make state mistakes: a flag set in one lock section and read in another, a Stop that returns before the queue drains, a button shown to someone who cannot press it. Tests walk one schedule and rarely find these. A model checker walks every interleaving, crash point and restart inside its bounds, and returns the shortest path to each broken rule. This skill makes that check part of normal work rather than a special occasion.

It needs Node 20 or later, or Bun. It does not need Java or TLC.

What the skill does

  • Models the entire program. Each component that holds state gets a spec of its real steps, plus a smaller interface spec of what its callers see. The implementation is checked to refine its interface, each spec builds on the interfaces below it, and a program spec at the root checks the promises a person relies on end to end. A coverage list gives every stateful component a spec or a written reason it needs none.
  • Keeps each spec next to its code. worker.go and Worker.tla share a directory and change in the same commit. The build checks the spec, so a spec that drifts from its code fails the change that made it drift.
  • Simplifies the spec and the code together. The agent models the code as it is, finds a design with fewer states in the model, checks it against the same promises, confirms that real primitives can enforce each step, builds it, and deletes what it displaces. Then it runs the next pass.
  • Proves each guard is needed. Each check, recheck, signal or lock the code relies on gets a mutant: the spec with that guard removed, which must break a rule. A mutant that survives means either the spec misses something or the guard is dead code.
  • Reads every counterexample against the source. A trace is a claim about the code. When the code can take every step, the trace is the reproduction and becomes the regression test. When it cannot, the spec is wrong.

What's inside

skills/tla/
  SKILL.md                         the workflow the agent follows
  references/
    whole-program.md               the tree of specs, refinement, coverage, screens
    modeling-code.md               modeling the code faithfully: callers, steps, platform semantics
    simplification.md              the joint spec and code simplification pass
    defects-and-mutants.md         working a bug through the spec; the mutants file
  tools/
    tla                            entry point; installs the pinned tla-ts on first run
    check.mjs                      finds and checks every model and mutant
    package.json, package-lock.json
    update-tla-ts.sh               moves the pin to the latest tla-ts
    modules/Surface.tla            shared rules for screen specs
  example/worker/
    worker.go                      a Go job queue
    Worker.tla, Worker.cfg         its spec and default model, beside it
    WorkerApi.tla                  the interface the Worker refines
    Worker.mutants.json            four guards, each shown necessary

Install

Claude Code

/plugin marketplace add paralin/tla-skill
/plugin install tla@tla-skill

Claude Code prefixes plugin skills, so the skill is /tla:tla. The agent also loads it on its own when a task matches the skill's description.

Cursor

The repository is a Cursor plugin too: .cursor-plugin/plugin.json points at skills/. Or copy skills/tla into your project's .cursor/skills/.

Any other agent

Copy the folder into the directory where your agent reads skills:

git clone https://github.com/paralin/tla-skill
cp -r tla-skill/skills/tla ~/.claude/skills/tla   # or your agent's skills directory

The skill is one self-contained folder. Nothing outside it is needed.

Try it

Run the checker on the worked example:

skills/tla/tools/tla skills/tla/example

The first run installs the pinned tla-ts with npm ci. Then:

pass      580 states  16 deep    103 ms  example/worker/Worker.cfg
kill      189 states   6 deep     37 ms  example/worker/Worker.tla mutant "take checks the queue and stops in two lock sections"  [][Next]_vars (WorkerApi line 52)
kill       13 states   3 deep     21 ms  example/worker/Worker.tla mutant "Submit accepts after Stop"  [][Next]_vars (WorkerApi line 52)
kill      478 states  16 deep     55 ms  example/worker/Worker.tla mutant "Submit does not signal"  AcceptedRuns
kill      266 states   7 deep     20 ms  example/worker/Worker.tla mutant "Stop does not signal"  deadlock
1 model(s), 0 failure(s)

The Worker's spec passes its safety, liveness and refinement checks, and each mutant breaks the rule it should. Run with TLA_MUTANT_TRACES=1 to see each counterexample. The first one is the bug the single lock section in worker.go prevents:

1. Init: lpc = "take", phase = "running", queue = <<>>, ...
2. Take: lpc = "check"
3. Submit(j1): sub = (j1 :> "signal" @@ j2 :> "idle"), queue = <<j1>>
4. StopMark: spc = "signal", phase = "draining"
5. CheckStop: lpc = "close", phase = "stopped"
6. CloseDone: lpc = "exited", done = TRUE

The loop saw an empty queue, a job was accepted, Stop was called, and the loop exited with the accepted job still queued.

Then ask your agent for real work, for example:

model our connection pool in TLA+ beside pool.go, then find a simpler design

this upload sometimes finishes twice after a reconnect. work it through a spec

add TLA+ coverage for every package under internal/ that holds state

The checker

tools/tla takes directories, .tla files or .cfg files, and checks the working directory when given none.

  • Foo.tla is checked once for each config beside it: Foo.cfg, and each Foo-<variant>.cfg. A .tla with no config is a helper module.
  • Modules resolve from the spec's own directory, then from tools/modules/.
  • Each result shows distinct states, depth and time, which is what you compare between a baseline and a simpler design. -json prints one JSON object per result.
  • A failure prints the broken rule and its shortest trace, one state per line, showing only the variables that changed. A missing EXTENDS is named.
  • Foo.mutants.json lists mutants as exact text replacements applied in memory. Each must break its expected rule; a mutant that passes, breaks a different rule, or no longer matches the spec fails the run.
  • -workers N searches in parallel on a large model.
  • The exit code is 0 when everything passes, 1 when a model fails or a mutant survives, and 2 when the arguments are wrong, such as a missing path or a spec file with no config beside it. A directory with no models passes, so check:tla can be set up before the first spec.

To run it in your own repository, copy skills/tla/tools/ to a path such as tools/tla/, ignore its node_modules/, and add a check:

{ "scripts": { "check:tla": "tools/tla/tla src" } }

Run that check in CI and in the same local loop as your build.

Updating tla-ts

tools/package.json pins tla-ts so every machine checks with the same version. tools/update-tla-ts.sh moves the pin to the latest release and refreshes the lockfile; rerun your models afterwards.

Credits

tla-ts by Aiden Bai is the model checker, a TypeScript implementation of TLA+ checking compatible with TLC, and is MIT licensed. TLA+ is Leslie Lamport's.

License

MIT