tla-precheck

tla-precheck is a TypeScript tool. You write a state machine once in a restricted TypeScript DSL; it is model-checked with TLA+ and TLC, and the runtime code is generated from the same source. That avoids the translation problem that breaks stateproof.

tla-precheck checks a small TypeScript DSL with TLC and generates the runtime code. Here: a ticket shop’s one-seat limit.

Using tla-precheck

The code below is in formal-methods-samples/tla-precheck-tickets. We ran it with tla-precheck 0.1.7 and Java 25. The output is from our run.

The problem

The limit counts only held seats, so a customer can buy one seat and hold another.

A ticket shop lets a customer hold a seat, then buy it or let it go, and a sold seat can be refunded. The rule is one seat per customer. The hold is allowed when the seat is free and the customer holds no other seat:

// tickets.machine.ts (shortened)
hold: {
  params: { s: "Seats", c: "Customers" },
  guard: and(
    eq(index(status, param("s")), lit("free")),
    eq(count("Seats", "x", and(
      eq(index(holder, param("x")), param("c")),
      eq(index(status, param("x")), lit("held"))
    )), lit(0))
  ),
  updates: [setMap("status", param("s"), lit("held")), setMap("holder", param("s"), param("c"))]
}

The count looks only at held seats. Once a customer buys their seat, it is sold, not held, and nothing stops them from holding a second one.

In tla-precheck this machine is the code: npx tla-precheck build generates the runtime adapters from it, so the bug and the fix both live in the .machine.ts file.

Install and set up

npm install -D tla-precheck
curl -fsSL -o tla2tools.jar https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar
export TLA2TOOLS_JAR=$PWD/tla2tools.jar

npx tla-precheck setup is meant to download TLC, but in tla-precheck 0.1.7 it rejects the download with “TLC checksum mismatch”, so download the jar yourself. The path in TLA2TOOLS_JAR must be absolute.

Needs Java 17+ for TLC, and a tsconfig.json in the folder you run from (without one, check stops with TS5083).

Writing the machine (use AI)

Guards, updates and invariants are built from DSL functions; proof.tiers sets the domains to check.

The rest of the machine: the state, the other actions, the rule, and how big a world to check.

// tickets.machine.ts (shortened)
export const ticketsMachine = defineMachine({
  version: 2,
  moduleName: "Tickets",
  variables: {
    status: mapVar("Seats", enumType("free", "held", "sold"), lit("free")),
    holder: mapVar("Seats", optionType(domainType("Customers")), lit(null))
  },
  // The checker tries every value of each action's params.
  actions: {
    hold: { /* above */ },
    buy: {
      params: { s: "Seats", c: "Customers" },
      guard: and(eq(index(status, param("s")), lit("held")), eq(index(holder, param("s")), param("c"))),
      updates: [setMap("status", param("s"), lit("sold"))]
    },
    // release (held to free) and refund (sold to free) look the same
  },
  // Must hold in every reachable state.
  invariants: {
    oneSeatPerCustomer: {
      description: "A customer never has more than one seat, held or sold",
      formula: forall("Customers", "c", lte(count("Seats", "x", eq(index(holder, param("x")), param("c"))), lit(1)))
    }
  },
  proof: {
    defaultTier: "pr",
    tiers: {
      pr: {
        domains: {
          // symmetry: the two customers are interchangeable, so each state is checked once.
          Customers: modelValues("c", { size: 2, symmetry: true }),
          Seats: ids({ prefix: "s", size: 3 })
        },
        // Estimated before TLC starts, so an oversized run fails at once.
        budgets: { maxEstimatedStates: 1000, maxEstimatedBranching: 20 }
      }
    }
  }
});

Running it

TLC breaks oneSeatPerCustomer: c1 holds s1, buys it, and holds s3.

npx tla-precheck check tickets.machine.ts

check validates the machine, estimates the state space (729 states allowed by the types here), runs TLC, then checks that TLC and the TypeScript interpreter found the same state graph. It prints the estimate, “Estimate passed. Running TLC verification…”, and then one JSON result. It exited with code 1, the certificate said "proofPassed": false, and its proofOutput field held TLC’s trace (shortened):

Error: Invariant oneSeatPerCustomer is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ holder = [s1 |-> "__NULL__", s2 |-> "__NULL__", s3 |-> "__NULL__"]
/\ status = [s1 |-> "free", s2 |-> "free", s3 |-> "free"]

State 2: <hold("s1",c1) line 23, col 3 to line 27, col 39 of module Tickets>
/\ holder = [s1 |-> c1, s2 |-> "__NULL__", s3 |-> "__NULL__"]
/\ status = [s1 |-> "held", s2 |-> "free", s3 |-> "free"]

State 3: <hold("s2",c2) line 23, col 3 to line 27, col 39 of module Tickets>
/\ holder = [s1 |-> c1, s2 |-> c2, s3 |-> "__NULL__"]
/\ status = [s1 |-> "held", s2 |-> "held", s3 |-> "free"]

State 4: <buy("s1",c1) line 29, col 3 to line 33, col 25 of module Tickets>
/\ holder = [s1 |-> c1, s2 |-> c2, s3 |-> "__NULL__"]
/\ status = [s1 |-> "sold", s2 |-> "held", s3 |-> "free"]

State 5: <hold("s3",c1) line 23, col 3 to line 27, col 39 of module Tickets>
/\ holder = [s1 |-> c1, s2 |-> c2, s3 |-> c1]
/\ status = [s1 |-> "sold", s2 |-> "held", s3 |-> "held"]

40 states generated, 25 distinct states found, 0 states left on queue.

Customer c1 holds s1, buys it, and holds s3. The step where c2 holds s2 plays no part: the trace is not the shortest one, which would take three steps. It ran in about a second and a half.

Fixing the bug

Count every seat the customer has. The proof passes, and both backends agree on 37 states.

The fix: the hold now counts every seat the customer has, held or sold:

Before the fix Diff With the fix

// A ticket shop: customers hold a seat, then buy it or let it go, and a sold seat can be refunded. Each customer may have one seat, held or sold.
import {
  and, count, defineMachine, domainType, enumType, eq, forall, ids, index, lit, lte,
  mapVar, modelValues, optionType, param, setMap, variable
} from "tla-precheck";
const status = variable("status");
const holder = variable("holder");
export const ticketsMachine = defineMachine({
  version: 2,
  moduleName: "Tickets",
  variables: {
    status: mapVar("Seats", enumType("free", "held", "sold"), lit("free")),
    holder: mapVar("Seats", optionType(domainType("Customers")), lit(null))
  },
  actions: {
    hold: {
      params: { s: "Seats", c: "Customers" },
      guard: and(
        eq(index(status, param("s")), lit("free")),
        eq(count("Seats", "x", and(
        eq(count("Seats", "x", eq(index(holder, param("x")), param("c"))), lit(0))
          eq(index(holder, param("x")), param("c")),
          eq(index(status, param("x")), lit("held"))
        )), lit(0))
      ),
      updates: [setMap("status", param("s"), lit("held")), setMap("holder", param("s"), param("c"))]
    },
    buy: {
      params: { s: "Seats", c: "Customers" },
      guard: and(eq(index(status, param("s")), lit("held")), eq(index(holder, param("s")), param("c"))),
      updates: [setMap("status", param("s"), lit("sold"))]
    },
    release: {
      params: { s: "Seats" },
      guard: eq(index(status, param("s")), lit("held")),
      updates: [setMap("status", param("s"), lit("free")), setMap("holder", param("s"), lit(null))]
    },
    refund: {
      params: { s: "Seats" },
      guard: eq(index(status, param("s")), lit("sold")),
      updates: [setMap("status", param("s"), lit("free")), setMap("holder", param("s"), lit(null))]
    }
  },
  invariants: {
    oneSeatPerCustomer: {
      description: "A customer never has more than one seat, held or sold",
      formula: forall("Customers", "c", lte(count("Seats", "x", eq(index(holder, param("x")), param("c"))), lit(1)))
    }
  },
  proof: {
    defaultTier: "pr",
    tiers: {
      pr: {
        domains: {
          Customers: modelValues("c", { size: 2, symmetry: true }),
          Seats: ids({ prefix: "s", size: 3 })
        },
        budgets: { maxEstimatedStates: 1000, maxEstimatedBranching: 20 }
      }
    }
  }
});
export default ticketsMachine;

The same check passes with exit code 0. The key part of the certificate:

{
  "machine": "Tickets",
  "tier": "pr",
  "proofPassed": true,
  "graphEquivalenceAttempted": true,
  "invariantsChecked": ["oneSeatPerCustomer"],
  "deadlockChecked": true,
  "symmetryUsedInProof": true,
  "equivalent": true,
  "tsStateCount": 37,
  "tlcStateCount": 37,
  "tsEdgeCount": 120,
  "tlcEdgeCount": 120
}

TLC found 19 distinct states with symmetry. The equivalence run, without symmetry, found 37 states and 120 edges, and the TypeScript interpreter found the same graph.

Deadlock checking is on by default. Our first version had no refund action, and the fixed machine then failed with “Deadlock reached” once both customers had bought a seat: no action was enabled. A real shop refunds, so the action went into both files.

Project layout and CI

Commit the machine and the generated adapter. CI sets up Java, downloads TLC, runs build and checks the adapter is up to date.

./
├── .github/workflows/ci.yml
├── tsconfig.json                    check stops without one
├── src/
│   ├── tickets.machine.ts           the machine
│   └── machine-adapters/
│       └── Tickets.adapter.ts       written by build, committed
└── .generated-machines/             TLA+ and TLC output, not committed

build writes the adapter only when the machine has metadata.runtimeAdapter (the Postgres table it runs on). The same machine always gives the same file, so CI can check that the committed adapter is up to date:

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

# .github/workflows/ci.yml (steps)
- uses: actions/setup-java@v6
  with: { distribution: temurin, java-version: 21 }
- run: npm ci
- run: curl -fsSL -o tla2tools.jar https://github.com/tlaplus/tlaplus/releases/download/v1.8.0/tla2tools.jar
# build runs check first.
- run: TLA2TOOLS_JAR=$PWD/tla2tools.jar npx tla-precheck build src/tickets.machine.ts
- run: git diff --exit-code src/machine-adapters

What fails when:

• A change breaks a rule: build, with TLC’s trace. The adapter is not written.
• A change leaves no action enabled: build, with “Deadlock reached”.
• The machine changed and the adapter was not rebuilt: git diff.

Making changes

Change the machine, run build, commit the machine and the adapter together.

1. Change tickets.machine.ts. Do not edit the adapter; its first line says “Generated. Do not edit.”
2. For a new rule, add it to invariants.
3. Run build. If the check fails, fix the machine and run it again.
4. Commit the machine and the adapter together.

Without adapter metadata, run check instead of build, and skip the git diff step.

Strengths

• It is fast and fails early. It checks the size first and stops before a run that would be too big; its biggest example checks 29 million states in under 3 minutes.
• It checks its own translation. It checks its translation to TLA+ instead of trusting it, and maps TLC’s steps back to your machine.
• Your code is generated from the checked machine. The transition code comes from the machine, and rules can become Postgres constraints.
• It is built for AI agents. It installs a skill, and the agent edits the machine until the check passes.

Limitations

• The spec language is small. Guards and effects cannot call your own functions or even add numbers, so a counter must be written as a fixed set of values.
• It replaces your code instead of checking it. It does not check existing code.
• No async. It does not check replies that arrive in any order.
• It needs Java. The check runs in TLC.

Links

• Built by the GitHub user kingbootoshi as a solo project, published on npm in March 2026, with no commits since early April 2026.
• tla-precheck on GitHub: https://github.com/kingbootoshi/tla-precheck
• tla-precheck on npm: https://www.npmjs.com/package/tla-precheck