TLA+ for TypeScript developers

TLA+ is a language for describing a system as state and the steps that change it. AWS, Microsoft and MongoDB use it on their distributed systems. TLA+ is the language. The checking is done by separate tools, and there are two main ones:

• TLC, the original model checker. It visits every reachable state of the spec. It also checks liveness: “this always ends”, not only “this never breaks”.
• Apalache, a symbolic checker built on the Z3 solver. It checks every run up to a set number of steps, and handles large ranges of values without listing each state. It needs type annotations.

One .tla file works with both, which is why this is one page and not three. Quint is a friendlier language that compiles to TLA+ and runs these same two checkers underneath. This page uses TLA+ directly.

TLA+ describes a system as state, steps and “must never happen” rules, checked in every order. It has its own language and checks the spec, not the real code. The spec is a separate, much smaller file with only the state and steps that matter, so bugs are easier to see. The cost is a second file to keep in sync with the code; the replay test in Step 6 does that.

Write the spec as plain text, let an agent turn it into TLA+, let TLC find the double connect, then replay every behavior of the spec against the real TS code.

Why you would want this

The test passes, but two requests at startup both connect.

Connect to the database on first use, then reuse the connection. Almost every Node service has this somewhere:

src/lazy-connect.ts

// Connect on first use, then reuse the connection.
export function lazyConnect<T>(connect: () => Promise<T>) {
  let db: T | undefined;
  return async () => {
    if (!db) db = await connect();
    return db;
  };
}

src/lazy-connect.test.ts

test('the second call reuses the connection', async () => {
  let connects = 0;
  const getDb = lazyConnect(async () => {
    connects++;
    return { pool: 1 };
  });
  await getDb();
  await getDb();
  expect(connects).toBe(1);
});

The test passes. It lets the first call finish before the second one starts. In production, two requests arrive while the service starts. Both see no connection, because the first connect() has not returned yet, and both connect: two pools, and the first one is never closed. TLC tries every order.

When TLA+ fits

• Several actors change shared state: requests, handlers, timers, retries, queues, locks, leader election, sagas.
• The bug you fear is about order: “what if a second request arrives while the first one is still connecting?”
• The rule can be said as “this must never happen” (two connects at once) or “this must always happen in the end” (every request gets the connection). TLC checks both kinds.

TLA+ is not the tool for proving one function’s math right for every input. See the Dafny and Lean pages for that.

Install

One jar and Java 11 or newer. Apalache is a separate download.

curl -LO https://github.com/tlaplus/tlaplus/releases/download/v1.7.4/tla2tools.jar
java -jar tla2tools.jar Spec.tla      # runs TLC on Spec.tla with the settings in Spec.cfg

TLC needs Java 11+. Apalache is a separate download and needs Java 17+.

Step 1: write the spec as plain text (you and AI)

A markdown file next to the code: variables, actions with a guard and an effect, and the rules. You and the agent write it together.

Before any TLA+, write down what the code does in a plain text file in the repo. There are concepts to learn, but no new syntax: variables and the values they can take, actions with a guard (when the step can happen) and an effect (what changes), and the rules that must hold. Write it together with a coding agent: it drafts from the TS code and asks what is unclear, you decide what the steps and rules are and correct every line. It is the file reviewers read.

Concepts: state, variables, actions, guards, effects, invariants, liveness, fairness.

spec/lazy-connect.md

# Lazy connect - spec

Connect on first use, then reuse the connection.
The checkable version is LazyConnect.tla, next to this file.

## Constants

- callers = a, b (two are enough to race)

## Variables

- db: none | ready = none (the connection that is kept)
- connecting: 0..2 = 0 (connect() calls in flight)
- callers: { a: idle | connecting | done | failed = idle, b: same as a }

## Actions

- call c (per caller)
  - Guard: c is idle
  - Effect:
    - db ready: c is done
    - otherwise: connect() starts, connecting + 1, c is connecting

- connect resolves for c
  - Guard: c is connecting
  - Effect: db = ready, connecting - 1, c is done

- connect rejects for c
  - Guard: c is connecting
  - Effect: connecting - 1, c is failed

- retry c (per caller)
  - Guard: c is failed
  - Effect: c is idle

## Properties

### Invariants

- at most one connect() at a time: connecting <= 1

### Temporal properties

- every caller gets the connection in the end, granted: callers call and retry, and
  connect may reject, but not every time

## Considerations

- The connection itself is not modeled, only whether there is one.
- Retry stands for the same caller, or the next request, asking again.

How it maps to the code:

• db is the db variable in lazyConnect. connecting counts the connect() calls that have not returned yet.
• Each action is one step of the code between two awaits. call c is getDb() up to await connect().

Writing it is where most of the thinking happens. The call c line has to say what a second caller sees while the first one is still connecting, and the answer, “otherwise: connect() starts”, is the bug.

Step 2: turn the text into TLA+ (use AI)

The agent writes the TLA+. You do not read it: the agent maps it back to the text, and the checks do the rest.

Ask AI to write spec/LazyConnect.tla and spec/LazyConnect.cfg from spec/lazy-connect.md. One variable per variable, one action per action, guards as conditions, the invariant and the temporal property as operators, fairness as the text states it. Above each part, put the line of the text it comes from as a comment. List anything you had to guess.

You do not need to read TLA+. To check the result:

• TLC parses it: java -jar tla2tools.jar spec/LazyConnect.tla starts checking instead of stopping at a parse error.
• Every action and rule in the text has its part in the spec, with the text line above it.
• The agent’s guesses are answered in the text, not in the spec. Then regenerate.

TLC then checks the spec (Step 3), and the replay checks that the real code does what the spec says (Step 6).

The generated spec, and how to read it

A TLA+ spec has variables (the state) and actions (the steps that change it). An action is a list of conditions joined by /\ (and). A line without ' is a condition: if it is false, the action cannot happen now. x' means “the value of x after this step”. Every action must say what every variable becomes, which is what UNCHANGED is for.

---- MODULE LazyConnect ----
\* Two callers ask for the connection at once. The first call connects,
\* later calls reuse the connection.
EXTENDS Naturals

Callers == {"a", "b"}

VARIABLES db, connecting, pc

vars == <<db, connecting, pc>>

Init ==
    /\ db = "none"
    /\ connecting = 0
    /\ pc = [c \in Callers |-> "idle"]

\* A caller asks: it gets the connection, or awaits connect() if there is none yet.
Call(c) ==
    /\ pc[c] = "idle"
    /\ IF db = "ready"
         THEN /\ pc' = [pc EXCEPT ![c] = "done"]
              /\ UNCHANGED connecting
         ELSE /\ pc' = [pc EXCEPT ![c] = "connecting"]
              /\ connecting' = connecting + 1
    /\ UNCHANGED db

\* connect() resolves: the connection is kept.
ConnectOk(c) ==
    /\ pc[c] = "connecting"
    /\ db' = "ready"
    /\ connecting' = connecting - 1
    /\ pc' = [pc EXCEPT ![c] = "done"]

\* connect() rejects: the caller gets the error.
ConnectFails(c) ==
    /\ pc[c] = "connecting"
    /\ connecting' = connecting - 1
    /\ pc' = [pc EXCEPT ![c] = "failed"]
    /\ UNCHANGED db

\* A caller got an error and tries again.
Retry(c) ==
    /\ pc[c] = "failed"
    /\ pc' = [pc EXCEPT ![c] = "idle"]
    /\ UNCHANGED <<db, connecting>>

Next == \E c \in Callers : Call(c) \/ ConnectOk(c) \/ ConnectFails(c) \/ Retry(c)

\* Callers call and retry. connect() may reject, but not every time.
Spec ==
    /\ Init /\ [][Next]_vars
    /\ \A c \in Callers : WF_vars(Call(c)) /\ WF_vars(Retry(c)) /\ SF_vars(ConnectOk(c))

\* At most one connect() at a time.
OneConnect == connecting <= 1

\* Every caller gets the connection in the end.
EveryoneGetsIt == \A c \in Callers : <>(pc[c] = "done")
====

And the config file TLC reads next to it:

\* spec/LazyConnect.cfg
SPECIFICATION Spec
INVARIANT OneConnect
PROPERTY EveryoneGetsIt

How to read it:

• [c \in Callers |-> "idle"] is a map, like Record<string, string>. pc[c] reads it, and [pc EXCEPT ![c] = "done"] returns an updated copy. pc is where each caller is, like a program counter.
• Call(c) has a parameter: there is one for each caller. So do ConnectOk(c) and ConnectFails(c), since each caller has its own connect() in flight.
• Next says what can happen next: any step whose conditions hold. TLC tries each one.
• Spec is the whole system: start in Init, then take Next steps. WF and SF are fairness: callers do call and retry, and connect() may reject, but not every time. SF (strong fairness) is what says “not every time”.
• OneConnect is an invariant: true in every state. EveryoneGetsIt is a liveness property: <> means “at some point”.

Step 3: let TLC find the bad order

TLC finds the double connect in under a second, in 3 states.

-deadlock turns off TLC’s deadlock check, since a run where both callers have the connection is supposed to stop. TLC stops at the first state that breaks OneConnect:

TLC’s counterexample (19 lines)

$ java -jar tla2tools.jar -deadlock spec/LazyConnect.tla
Error: Invariant OneConnect is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ connecting = 0
/\ pc = [a |-> "idle", b |-> "idle"]
/\ db = "none"

State 2: <Call line 19, col 5 to line 25, col 19 of module LazyConnect>
/\ connecting = 1
/\ pc = [a |-> "connecting", b |-> "idle"]
/\ db = "none"

State 3: <Call line 19, col 5 to line 25, col 19 of module LazyConnect>
/\ connecting = 2
/\ pc = [a |-> "connecting", b |-> "connecting"]
/\ db = "none"

6 states generated, 6 distinct states found, 3 states left on queue.

Read it as a timeline:

1. Caller a sees no connection and calls connect().
2. Caller b arrives before that call returns. It sees no connection either, and calls connect() again.

Two connects, two pools. TLC checks states in breadth-first order, so the trace it prints is a shortest one. Most races need only two or three actors to show up.

Step 4: fix it

Keep the promise, not the connection, and drop it if it rejects. Both properties hold.

Keep the promise instead of the connection, so a second caller awaits the same connect(). If the promise rejects, drop it, so the next call connects again. A rejected promise that stays would fail every later call, and TLC’s EveryoneGetsIt check catches that too. Change the text first:

Before the fix Diff With the fix

# Lazy connect - spec
Connect on first use, then reuse the connection.
The checkable version is LazyConnect.tla, next to this file.
## Constants
- callers = a, b (two are enough to race)
## Variables
- db: none | pending | ready = none (the connectionpromise that is kept)
- connecting: 0..2 = 0 (connect() calls in flight)
- callers: { a: idle | connectingwaiting | done | failed = idle, b: same as a }
## Actions
- call c (per caller)
  - Guard: c is idle
  - Effect:
    - db none: connect() starts, db = pending, connecting + 1, c is waiting
    - db pending: c is waiting on the same promise
    - db ready: c is done
    - otherwise: connect() starts, connecting + 1, c is connecting
- connect resolves for c
  - Guard: c is connecting
  - Guard: db is pending
  - Effect: db = ready, connecting - 1, cevery waiting caller is done
- connect rejects for c
  - Guard: c is connecting
  - Guard: db is pending
  - Effect: connecting - 1, c is failed
  - Effect: db = none (the rejected promise is dropped), connecting - 1, every waiting caller is failed
- retry c (per caller)
  - Guard: c is failed
  - Effect: c is idle
## Properties
### Invariants
- at most one connect() at a time: connecting <= 1
### Temporal properties
- every caller gets the connection in the end, granted: callers call and retry, and
  connect may reject, but not every time
## Considerations
- The connection itself is not modeled, only whether there is one.
- Retry stands for the same caller, or the next request, asking again.

The agent updates the spec to match.

The spec change: spec/LazyConnect.tla

db now holds the promise: none yet, pending or resolved. The two connect actions no longer belong to one caller: every caller waiting on the promise gets the same result.

Before the fix Diff With the fix

---- MODULE LazyConnect ----
\* Two callers ask for the connection at once. The first call connects,
\* later calls reuse the connection.
EXTENDS Naturals
Callers == {"a", "b"}
VARIABLES db, connecting, pc
vars == <<db, connecting, pc>>
Init ==
    /\ db = "none"
    /\ connecting = 0
    /\ pc = [c \in Callers |-> "idle"]
\* A caller asks: it gets the connection, or awaits connect() if there is none yet.
\* A caller asks: it gets the promise that is kept, or starts connect() and keeps its promise.
Call(c) ==
    /\ pc[c] = "idle"
    /\ IF db = "ready"
    /\ CASE db = "none" ->
         THEN               /\ pc' = [pc EXCEPT ![c] = "donewaiting"]
              /\ UNCHANGED connecting
              /\ db' = "pending"
         ELSE /\ pc' = [pc EXCEPT ![c] = "connecting"]
              /\ connecting' = connecting + 1
    /\ UNCHANGED db
         [] db = "pending" ->
              /\ pc' = [pc EXCEPT ![c] = "waiting"]
              /\ UNCHANGED <<db, connecting>>
         [] db = "ready" ->
              /\ pc' = [pc EXCEPT ![c] = "done"]
              /\ UNCHANGED <<db, connecting>>
\* connect() resolves: the connection is kept.
\* connect() resolves: every waiting caller gets the connection.
ConnectOk(c) ==
    /\ pc[c] = "connecting"
    /\ db = "pending"
    /\ db' = "ready"
    /\ connecting' = connecting - 1
    /\ pc' = [pc EXCEPT ![c] = "done"]
    /\ pc' = [c \in Callers |-> IF pc[c] = "waiting" THEN "done" ELSE pc[c]]
\* connect() rejects: the caller gets the error.
\* connect() rejects: every waiting caller gets the error, and the rejected promise is dropped.
ConnectFails(c) ==
    /\ pc[c] = "connecting"
    /\ db = "pending"
    /\ db' = "none"
    /\ connecting' = connecting - 1
    /\ pc' = [pc EXCEPT ![c] = "failed"]
    /\ pc' = [c \in Callers |-> IF pc[c] = "waiting" THEN "failed" ELSE pc[c]]
    /\ UNCHANGED db
\* A caller got an error and tries again.
Retry(c) ==
    /\ pc[c] = "failed"
    /\ pc' = [pc EXCEPT ![c] = "idle"]
    /\ UNCHANGED <<db, connecting>>
Next == ConnectOk \/ ConnectFails \/ \E c \in Callers : Call(c) \/ ConnectOk(c) \/ ConnectFails(c) \/ Retry(c)
\* Callers call and retry. connect() may reject, but not every time.
Spec ==
    /\ Init /\ [][Next]_vars
    /\ \A c \in Callers : WF_vars(Call(c)) /\ WF_vars(Retry(c)) /\ SF_vars(ConnectOk(c))
    /\ SF_vars(ConnectOk)
    /\ \A c \in Callers : WF_vars(Call(c)) /\ WF_vars(Retry(c))
\* At most one connect() at a time.
OneConnect == connecting <= 1
\* Every caller gets the connection in the end.
EveryoneGetsIt == \A c \in Callers : <>(pc[c] = "done")
====

In the TS code:

Before the fix Diff With the fix

export function lazyConnect<T>(connect: () => Promise<T>) {
  let db: Promise<T> | undefined;
  return async () => {
    if (!db) db = await connect();
    if (!db) {
      db = connect().catch((e) => {
        db = undefined;
        throw e;
      });
    }
    return db;
  };
}

$ java -jar tla2tools.jar -deadlock spec/LazyConnect.tla
Checking 2 branches of temporal properties for the complete state space with 28 total distinct states
Finished checking temporal properties in 00s
Model checking completed. No error has been found.
27 states generated, 14 distinct states found, 0 states left on queue.

Never two connects at once, and every caller gets the connection in the end, in every run.

Step 5: the same spec in Apalache

Add a type comment to each variable; Apalache finds the same double connect with Z3.

Apalache reads the same file. It needs one type comment per variable, which the agent adds. TLC ignores them.

The type comments

VARIABLES
    \* @type: Str;
    db,
    \* @type: Int;
    connecting,
    \* @type: Str -> Str;
    pc

Apalache checks “must never happen” rules; it has no fairness, so it cannot check EveryoneGetsIt. On the Step 2 spec it finds the double connect:

$ apalache-mc check --no-deadlock --inv=OneConnect --length=10 spec/LazyConnect.tla
State 2: state invariant 0 violated.
Found 1 error(s)
The outcome is: Error
Total time: 1.691 sec

On the fixed spec:

$ apalache-mc check --no-deadlock --inv=OneConnect --length=10 spec/LazyConnect.tla
The outcome is: NoError
Checker reports no error up to computation length 10
Total time: 1.805 sec

Callers can retry forever, so runs of this spec never stop. Apalache checked every run up to 10 steps; TLC checked every state, which covers runs of any length. Apalache also writes a counterexample as violation1.itf.json in _apalache-out/, the same trace format Quint uses.

Which checker to use:

	TLC	Apalache
How	Lists every reachable state	Turns runs into Z3 formulas
Covers	Every state, however many steps	Every run up to --length steps
Liveness (<>, fairness)	Yes	Limited
Big value ranges (amounts, counters)	Slow: each value is a state	Fast: a range is one formula
Needs	Java 11+, one jar	Java 17+, type comments

Start with TLC. Use Apalache when a variable holds amounts or large numbers and TLC’s state count grows too large.

Step 6: replay every behavior against the real TS code (use AI)

TLC writes its whole state graph; vitest walks every path in it against the real function.

The spec is right. Nothing yet says the TS code behaves like the spec. TLC can write the whole state graph it explored, with each edge labeled by its action:

java -jar tla2tools.jar -deadlock -dump dot,actionlabels spec/out/graph spec/LazyConnect.tla

That writes spec/out/graph.dot: one node per state, one edge per step. The spec is small, so the test can walk every path from the first state until it stops or comes back to a state it has already been in. That is every behavior of the spec up to its first loop, not a sample. For each path, it drives the real lazyConnect with a connect whose calls wait until the path says how they end:

The replay test: src/lazy-connect.tla.test.ts (119 lines)

src/lazy-connect.tla.test.ts

import { readFileSync } from 'node:fs';
import { expect, test } from 'vitest';
import { lazyConnect } from './lazy-connect';

// TLC's state graph (-dump dot,actionlabels): one node per state, one edge per step.
type Status = 'idle' | 'connecting' | 'waiting' | 'done' | 'failed';
interface State {
  connecting: number;
  pc: Record<string, Status>;
}
interface Edge {
  to: string;
  action: string;
}

function readGraph(file: URL) {
  const states = new Map<string, State>();
  const edges = new Map<string, Edge[]>();
  let init = '';
  for (const line of readFileSync(file, 'utf8').split('\n')) {
    const node = line.match(/^(-?\d+) \[label="(.*)"(,style = filled)?\]/);
    if (node) {
      const pc = Object.fromEntries(
        [...node[2].matchAll(/(\w+) \|-> \\"(\w+)\\"/g)].map((m) => [m[1], m[2] as Status]),
      );
      states.set(node[1], { connecting: Number(node[2].match(/connecting = (\d+)/)![1]), pc });
      if (node[3]) init = node[1];
    }
    const edge = line.match(/^(-?\d+) -> (-?\d+) \[label="(\w+)"/);
    if (edge && edge[1] !== edge[2]) {
      edges.set(edge[1], [...(edges.get(edge[1]) ?? []), { to: edge[2], action: edge[3] }]);
    }
  }
  return { states, edges, init };
}

// Every behavior of the model: each path from the initial state until it stops,
// or until it comes back to a state it has already been in.
function allPaths(graph: ReturnType<typeof readGraph>): Edge[][] {
  const walk = (from: string, seen: Set<string>): Edge[][] => {
    const next = graph.edges.get(from) ?? [];
    if (next.length === 0) return [[]];
    return next.flatMap((e) =>
      seen.has(e.to) ? [[e]] : walk(e.to, new Set([...seen, e.to])).map((rest) => [e, ...rest]),
    );
  };
  return walk(graph.init, new Set([graph.init]));
}

// Each connect() call waits until the replay says how it ends.
function world() {
  const connects: { caller: string; ok: () => void; fail: () => void }[] = [];
  let caller = '';
  const getDb = lazyConnect(
    () =>
      new Promise<string>((resolve, reject) => {
        connects.push({ caller, ok: () => resolve('pool'), fail: () => reject(new Error('refused')) });
      }),
  );
  const status: Record<string, Status> = { a: 'idle', b: 'idle' };
  const call = (c: string) => {
    caller = c;
    status[c] = 'waiting';
    getDb().then(
      () => (status[c] = 'done'),
      () => (status[c] = 'failed'),
    );
  };
  // End the connect() this caller started, or the one shared by everyone.
  const finish = (how: 'ok' | 'fail', c: string) => {
    expect(connects.length, 'the model says connect() ends here, but none is running').toBeGreaterThan(0);
    const i = Math.max(0, connects.findIndex((x) => x.caller === c));
    connects.splice(i, 1)[0][how]();
  };
  return { connects, status, call, finish };
}

const settle = () => new Promise((resolve) => setTimeout(resolve, 0));

// The edge label has no caller: it is the one whose status changes.
// The code cannot tell a caller that started connect() from one that shares it.
const seen = (s: Status) => (s === 'connecting' ? 'waiting' : s);
const graph = readGraph(new URL('../spec/out/graph.dot', import.meta.url));
const steps = (path: Edge[]) => {
  let from = graph.init;
  return path.map(({ to, action }) => {
    const [a, b] = [graph.states.get(from)!, graph.states.get(to)!];
    const who = Object.keys(b.pc).filter((c) => a.pc[c] !== b.pc[c]);
    from = to;
    const name = who.length === 1 ? `${action}(${who[0]})` : action;
    return { to, action, who: who[0], name };
  });
};
const paths = allPaths(graph)
  .map(steps)
  .map((path) => [path.map((s) => s.name).join(' → '), path] as const);

test.each(paths)('%s', async (_name, path) => {
  const { connects, status, call, finish } = world();

  for (const { to, action, who, name } of path) {
    if (action === 'Call') call(who);
    else if (action === 'ConnectOk') finish('ok', who);
    else if (action === 'ConnectFails') finish('fail', who);
    else if (action === 'Retry') status[who] = 'idle';
    else throw new Error(`no mapping for action ${action}`);
    await settle();

    const model = graph.states.get(to)!;
    expect(connects.length, 'at most one connect() at a time').toBeLessThanOrEqual(1);
    expect({ step: name, connecting: connects.length, ...status }).toEqual({
      step: name,
      connecting: model.connecting,
      a: seen(model.pc.a),
      b: seen(model.pc.b),
    });
  }
});

First, replay the Step 2 spec against the original function. TLC stops at the first violation, so to get the full graph, run it once with a config that leaves out the INVARIANT line:

$ npx vitest run src/lazy-connect.tla.test.ts
 ❯ src/lazy-connect.tla.test.ts (108 tests | 80 failed)
   × Call(a) → Call(b) → ConnectOk(a) → ConnectOk(b)
   × Call(a) → Call(b) → ConnectOk(a) → ConnectFails(b) → Retry(b) → Call(b)
   ...

AssertionError: at most one connect() at a time: expected 2 to be less than or equal to 1

The spec has 108 behaviors up to their first loop. The real function followed the spec at every step of all of them, and broke the rule on the 80 where both callers were connecting at once. The TLC counterexample is now a failing vitest on your real code.

After Step 4, the fixed function against the fixed spec: 68 behaviors, all pass. To check the replay is not passing by accident, run the fixed function against the Step 2 spec: 80 of 108 fail, first at the second Call. The spec says b starts a second connect(); the fixed code shares the first one. The replay notices when the code and the spec differ, not just when the rule breaks.

The replay checks steps and states, not whole runs. “Every caller gets the connection in the end” is checked by TLC on the spec.

Project layout and CI

One script checks the spec and writes the graph; the replay always reads a fresh one.

One repo. The spec sits in its own folder. The graph is written from it on every test run and never committed:

./
├── .github/workflows/ci.yml
├── spec/
│   ├── lazy-connect.md             the spec in plain text: written with the agent, reviewed by people
│   ├── LazyConnect.tla             the same spec in TLA+, generated from the text
│   ├── LazyConnect.cfg             which spec and properties TLC checks
│   └── out/                        graph and TLC's working files, git-ignored
├── src/
│   ├── lazy-connect.ts             the real function
│   ├── lazy-connect.test.ts        normal unit tests
│   └── lazy-connect.tla.test.ts    replays spec/out/graph.dot against lazy-connect.ts
├── tools/tla2tools.jar             downloaded, git-ignored
├── .gitignore                      node_modules, spec/out/, tools/
├── package.json
└── tsconfig.json

Scripts in package.json:

"scripts": {
  "tla:install": "mkdir -p tools && curl -sLo tools/tla2tools.jar https://github.com/tlaplus/tlaplus/releases/download/v1.7.4/tla2tools.jar",
  "tla:check": "java -jar tools/tla2tools.jar -deadlock -cleanup -metadir spec/out/meta -dump dot,actionlabels spec/out/graph spec/LazyConnect.tla",
  "pretest": "npm run tla:check",
  "typecheck": "tsc",
  "test": "vitest run"
}

pretest runs before npm test, so the replay always walks the graph of the current spec.

TLC and the replay both need Java, so CI is one job:

The CI workflow: .github/workflows/ci.yml (30 lines)

.github/workflows/ci.yml

name: CI

on:
  push:
    branches: [main]
  pull_request:

jobs:
  check:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v7
      - uses: actions/setup-java@v6
        with:
          distribution: temurin
          java-version: 21
      - uses: actions/setup-node@v7
        with:
          node-version: 24
          cache: npm
      - uses: actions/cache@v6
        with:
          path: tools
          key: tla-${{ hashFiles('package.json') }}
      - run: npm ci
      - run: test -f tools/tla2tools.jar || npm run tla:install
      - run: npm run typecheck
      - name: Check the spec, then replay every behavior against the real function
        run: npm test

What fails when:

Change	Where CI fails
A spec change breaks OneConnect or EveryoneGetsIt	npm test, in pretest: TLC prints the counterexample
The function changes and no longer follows the spec	lazy-connect.tla.test.ts: the path and step where the code and the spec differ
The spec changes, the function does not	lazy-connect.tla.test.ts: the new paths no longer match the old function
The spec gets a new action	lazy-connect.tla.test.ts: no mapping for action ...

Making changes

Change the text spec first and check it, then change the code until the replay passes.

Changing the flow (for example, the connection can drop and must reconnect):

1. Change the text spec first: a new action, the variables it touches, and a rule if there is a new “must never happen” or “must always happen”.
2. Ask the agent to update LazyConnect.tla from it, and to list what it changed in the words of the text.
3. Run npm run tla:check until TLC passes.
4. Change the function. Map the new action in lazy-connect.tla.test.ts.
5. Run npm test until the replay passes. Commit the text, the spec, the function and the replay test together.

When the graph grows: walking every path works while the spec is small. Past a few thousand paths, replay a sample. TLC’s -simulate mode writes random runs, and Apalache and Quint write traces as ITF JSON (see the Quint page for a replay built on those).

Reviewing a pull request: read the text spec diff. A new await in the code with no new step in the text means the spec no longer splits the code where it can interleave. That is the one mistake the replay cannot catch, because the replay follows the spec’s steps.

Strengths

• Every order of steps is checked. TLC tries them all in the spec, in under a second at this size.
• Liveness, not only safety. “Every caller gets the connection in the end” is checked, not only “nothing bad happens”.
• A short, readable failing trace. You get the shortest order that breaks the spec, not a bug that shows up once in a while at startup.
• Fixes checked before code. You can check a fix in the spec, then replay every behavior of a small spec against the real TS code.

Limitations

• No proof about the TS code. TLC checks the spec. The replay checks the code on the spec’s behaviors, but not liveness.
• The spec takes effort. You choose where the steps split. If you merge steps that the real code keeps apart, the spec hides the bug.
• Only what the spec models. A connection that drops later, or more than one process, is not in this spec, so TLC says nothing about it.
• Unfamiliar syntax. /\, ', EXCEPT and <> take a day to learn. Quint runs the same checkers with a friendlier language.

How to start in your own project

1. Pick one flow where order matters: a lazy connection, a signal and a timer, a retry loop, a lock, a saga.
2. Write a text spec next to the code. List the variables, including the ones outside your code: calls in flight, what each caller has seen.
3. Make one action per step between two awaits in the real code, and one action per way a call can end.
4. Write the rules as “this must never happen” and “this must always happen in the end”, and say which steps are fair (callers call, calls return) and which are not (a call may fail).
5. Let an agent turn the text into TLA+, with each part tagged by the line of the text it comes from.
6. Run TLC with 2 or 3 actors, then dump the graph and replay it against the real code with controlled fakes.

Related

• Quint for TypeScript developers: a TLA+-based language with the same checkers underneath.
• The TLA+ home page and the TLA+ Video Course by Leslie Lamport.
• Learn TLA+, a practical guide by Hillel Wayne.
• TLA+ examples, a large set of real specs.
• TLA+ tools on GitHub and Apalache on GitHub.