Tla Precheck

TLA PreCheck

What This Is

TLA PreCheck is a restricted TypeScript DSL with TLA+ semantics.

You write machines in .machine.ts files. You do NOT write .tla files.

The compiler generates:

• TLA+ spec for TLC model checking (exhaustive proof)
• TypeScript interpreter for runtime execution
• Postgres DDL for database-level enforcement
• Generated adapter with typed per-action functions

The key guarantee: for a chosen finite proof tier, the generated TLA+ and the generated TypeScript interpreter reach the same state graph. Not similar - identical. Mathematically verified.

Think in TLA+, write in TypeScript.

Design Rules

1. One risky workflow per machine. Don't model your whole system. Model the billing state machine. Model the subscription lifecycle. One machine per critical flow. 2. Keep proof domains tiny. 2 users, 3 runs finds most bugs. Scale up in nightly tiers. 3. Fix the design, not the code. If check fails, the state machine design is wrong. Redesign the transitions and invariants. 4. Never edit generated artifacts. Don't touch .tla files, certificates, or adapter code. Regenerate with build. 5. Never write directly to machine-owned tables. All mutations go through the generated adapter or interpreter. 6. Prefer small atomic machines. Multiple small machines composed at the application layer beat one giant spec.

The Three Commands

# 1. Start a new machine
npx tla-precheck init

# 2. Design loop - run until it passes
npx tla-precheck check <machine>

# 3. Ship it - generates adapter + all artifacts for adapter-capable machines
npx tla-precheck build <machine>

The design loop: 1. Write/edit the .machine.ts DSL 2. Run check - it validates, estimates state space, then runs TLC 3. If the model checker finds a bug (invariant violation, stuck state), it tells you exactly what sequence of events caused it 4. Fix the DSL - not a code patch, a design fix 5. Repeat until check passes 6. If the machine declares metadata.runtimeAdapter, metadata.ownedTables, and metadata.ownedColumns, run build to generate the adapter and all artifacts 7. Import the generated adapter functions into your codebase

DSL Quick Reference

Machines have variables, actions, invariants, and proof tiers. If you want build to generate a database adapter, the machine also needs adapter metadata.

Variables

// Scalar: one value
status: scalarVar(enumType("draft", "active", "done"), lit("draft"))

// Map: one value per domain element (like a column per row)
status: mapVar("Runs", enumType("idle", "running", "done"), lit("idle"))
owner: mapVar("Runs", optionType(domainType("Users")), lit(null))

Actions

activate: {
  params: { r: "Runs" },                          // bound parameters
  guard: eq(index(status, param("r")), lit("idle")), // when is this allowed?
  updates: [setMap("status", param("r"), lit("running"))]  // what changes?
}

Invariants

oneActivePerUser: {
  description: "At most one running item per user",
  formula: forall("Users", "u", lte(
    count("Runs", "c", and(
      eq(index(owner, param("c")), param("u")),
      eq(index(status, param("c")), lit("running"))
    )),
    lit(1)
  ))
}

Proof Tiers

proof: {
  defaultTier: "pr",
  tiers: {
    pr: {
      domains: {
        Users: modelValues("u", { size: 2, symmetry: true }),
        Runs: ids({ prefix: "r", size: 3 })
      },
      budgets: { maxEstimatedStates: 10_000 }
    }
  }
}

For the full DSL reference, see references/dsl-cheatsheet.md. For the complete CLI workflow, see references/cli-workflow.md.

What "Done" Means

The machine is verified when: 1. check passes - TLC exhaustively explored every reachable state 2. The equivalence certificate says equivalent: true 3. build succeeds - adapter generated from the proven machine when adapter metadata is declared

After build, your codebase imports typed functions:

import { create, cancel, complete } from "./machine-adapters/MyMachine.adapter";
await create(sql, { u: userId, r: runId });

Each function opens a transaction, locks rows, runs the proven interpreter, diffs state, and writes changes. No hand-written guard logic. No hallucination surface.

Runtime Boundary

• The interpreter IS the runtime semantics - not an advisory check
• The generated adapter is the preferred mutation path when the machine fits the adapter subset (single owned table, all mapVars, one row domain)
• build requires explicit database mapping metadata:
• metadata.runtimeAdapter
• metadata.ownedTables
• metadata.ownedColumns
• If the adapter subset doesn't fit, call the interpreter manually:

  import { resolveMachine } from "tla-precheck/proof";
  import { buildInitialState, enabled, step } from "tla-precheck/interpreter";

  const resolved = resolveMachine(myMachine, "pr");
  const current = buildInitialState(resolved);
  if (!enabled(resolved, current, "activate", { r: "r1" })) {
    throw new Error("Transition not enabled");
  }
  const next = step(resolved, current, "activate", { r: "r1" });

• Storage constraints (Postgres partial unique indexes, CHECK constraints) back cross-row invariants at the database level

CLI Workflow

Installation

npm install -D tla-precheck    # or: bun add -D tla-precheck
npx tla-precheck setup         # install agent skills + TLC
npx tla-precheck doctor        # verify environment

Requirements: Node 18+ or Bun 1.0+. Java 17+ for TLC model checking.

The Design Loop

1. Scaffold a new machine

npx tla-precheck init
# Prompts for a machine name or path, then creates <name>.machine.ts

2. Edit the machine

Open the .machine.ts file. Define:

• Variables: the state your machine tracks
• Actions: guarded transitions that change state
• Invariants: properties that must hold in every reachable state
• Proof tiers: bounded domains for model checking

3. Check the design

npx tla-precheck check billing

This runs three steps: 1. Validate - checks the DSL for structural errors 2. Estimate - computes state space size, fails fast if over budget 3. Verify - runs TLC to exhaustively explore every reachable state

If TLC finds an invariant violation, it outputs the exact sequence of transitions (error trace) that leads to the bug. Fix the machine design and re-run.

4. Build artifacts

npx tla-precheck build billing

This runs check first, then generates:

• TLA+ spec and config (for inspection)
• Postgres storage contract (DDL)
• Typed adapter module at src/machine-adapters/Billing.adapter.ts

build requires explicit database mapping metadata in the machine:

• metadata.runtimeAdapter
• metadata.ownedTables
• metadata.ownedColumns

Without that metadata, check can still pass but build will stop at adapter generation and show the metadata shape to add.

5. Import and use

import { activate, cancel } from "./machine-adapters/Billing.adapter";

// Each function: opens transaction, locks rows, runs proven interpreter,
// diffs state, writes changes. Throws if transition is invalid.
await activate(sql, { r: runId });
await cancel(sql, { r: runId });

If the machine does not fit the adapter subset, use the interpreter directly:

import { resolveMachine } from "tla-precheck/proof";
import { buildInitialState, enabled, step } from "tla-precheck/interpreter";
import billingMachine from "./billing.machine.js";

const resolved = resolveMachine(billingMachine, "pr");
let state = buildInitialState(resolved);

if (enabled(resolved, state, "submit", { o: "o1" })) {
  const next = step(resolved, state, "submit", { o: "o1" });
  if (next !== null) {
    state = next;
  }
}

Advanced Commands

Fast estimation (no Java needed)

npx tla-precheck estimate billing.machine.ts
npx tla-precheck estimate billing.machine.ts --tier nightly

Generate TLA+ for inspection

npx tla-precheck generate billing.machine.ts

Generate Postgres constraints

npx tla-precheck generate-db billing.machine.ts

Verify live database schema

bunx tla-precheck verify-db billing

Requires DATABASE_URL env var. Bun runtime only.

Verify all machines in a directory

npx tla-precheck verify-all dist/
npx tla-precheck verify-all dist/ --all-tiers

Lint for raw writes

npx tla-precheck lint billing
npx tla-precheck lint-all src/

Environment Variables

CI Integration

steps:
  - run: npm install
  - run: npx tla-precheck check src/billing.machine.ts
  - run: npx tla-precheck check src/subscription.machine.ts

If any check fails, the build fails. That is the gate.

DSL Cheatsheet

Expression Kinds (13 total)

No other expression forms are allowed. This restriction is what makes equivalence provable.

Update Kinds (2 total)

Value Types

Variable Kinds

// Scalar: single value
mode: scalarVar(enumType("sleeping", "awake", "eating"), lit("sleeping"))

// Map: function from domain to codomain (like a DB column)
status: mapVar("Runs", enumType("idle", "queued", "running"), lit("idle"))

Proof Domain Types

// Model values: interchangeable (enables symmetry reduction)
Users: modelValues("u", { size: 2, symmetry: true })

// IDs: concrete string identifiers
Runs: ids({ prefix: "r", size: 3 })  // generates "r1", "r2", "r3"

// Explicit values
Statuses: values(["draft", "active"])

Machine Structure

import {
  defineMachine, variable, scalarVar, mapVar,
  enumType, domainType, optionType,
  lit, param, eq, lte, and, or, not, isin, count, forall, index,
  setVar, setMap, setOf,
  modelValues, ids
} from "tla-precheck";

const myVar = variable("myVar");

export const myMachine = defineMachine({
  version: 2,
  moduleName: "MyMachine",
  variables: { /* ... */ },
  actions: { /* ... */ },
  invariants: { /* ... */ },
  proof: {
    defaultTier: "pr",
    tiers: { /* ... */ }
  },
  // Required for `build` if you want generated adapter output
  metadata: {
    ownedTables: ["my_table"],
    ownedColumns: { my_table: ["status", "owner"] },
    runtimeAdapter: {
      schema: "public",
      table: "my_table",
      rowDomain: "Runs",
      keyColumn: "id",
      keySqlType: "bigint"
    }
  }
});

export default myMachine;

check does not require this metadata. build does.

Manual Interpreter Usage

import myMachine from "./my.machine.js";
import { resolveMachine } from "tla-precheck/proof";
import { buildInitialState, enabled, step } from "tla-precheck/interpreter";

const resolved = resolveMachine(myMachine, "pr");
let state = buildInitialState(resolved);

if (enabled(resolved, state, "activate", { r: "r1" })) {
  const next = step(resolved, state, "activate", { r: "r1" });
  if (next !== null) {
    state = next;
  }
}

Hard Limits

• Graph-equivalence tiers: max 100,000 estimated states, max 10,000 branching
• Proof domains: max 100 values
• Actions: max 4 parameters
• TLC: 4GB heap, auto workers, 60s timeout
• DOT files: max 50MB