![\"TLA](\"tla-precheck-banner.jpeg\")
\n\n \n
\n The Problem -\n How It Works -\n Before & After -\n Quickstart -\n Install -\n The Design Loop -\n Technical Reference\n
\n\n---\n\nWrite your state machine once. The compiler mathematically checks every possible state\nfor bugs, then generates the runtime code. One source of truth. No drift. No if/else\nchains. No praying your guards are consistent across services.\n\nTLA PreCheck uses [TLA+](https://lamport.azurewebsites.net/tla/tla.html) model checking\nunder the hood - the same math Amazon used to find bugs in DynamoDB that no amount of\ntesting could catch. You don't need to know TLA+. You write TypeScript. The compiler\nhandles the rest.\n\n## How It Works\n\nYou write the state machine once in a restricted TypeScript DSL. The compiler generates\neverything else:\n\n```\n +---> TLA+ Spec -----------> TLC Model Checker (proves design correct)\n |\nMachine DSL (one source of truth) --+---> TypeScript Interpreter (runtime execution)\n |\n +---> Generated Adapter ----> Typed functions you import\n |\n +---> Postgres DDL ---------> Database-level enforcement\n```\n\nThen it proves the TLA+ spec and the TypeScript interpreter produce **bit-identical state\ngraphs** across every reachable state. Not \"similar.\" Identical. Mathematically verified.\n\nIf they diverge, your build fails. If an invariant is violated in any reachable state,\nyour build fails. No bugs ship.\n\n## Before and After\n\n**Before: scattered if/else guards across your codebase**\n\n```typescript\n// api/runs/cancel.ts - hope this matches the other 6 places that check run status\nif (run.status === \"queued\" || run.status === \"running\") {\n if (run.owner === userId || isAdmin(userId)) {\n await db.update(\"agent_runs\", { id: runId, status: \"cancelled\" });\n } else {\n throw new Error(\"Not authorized to cancel this run\");\n }\n} else {\n throw new Error(\"Cannot cancel a run that is not active\");\n}\n\n// api/runs/complete.ts - is this consistent with cancel? who knows\nif (run.status === \"running\") {\n await db.update(\"agent_runs\", { id: runId, status: \"completed\" });\n} else {\n throw new Error(\"Can only complete a running run\");\n}\n\n// background/sweep.ts - third place with status logic, probably slightly different\nif (run.status === \"running\" && isStale(run)) {\n await db.update(\"agent_runs\", { id: runId, status: \"failed\" });\n}\n```\n\n**After: one DSL, proven correct, generated functions**\n\n```typescript\n// The machine - every guard, every transition, every invariant in one place\nexport const agentRunsMachine = defineMachine({\n version: 2,\n moduleName: \"AgentRuns\",\n variables: {\n status: mapVar(\"Runs\", enumType(\"idle\", \"queued\", \"running\", \"completed\", \"failed\", \"cancelled\"), lit(\"idle\")),\n owner: mapVar(\"Runs\", optionType(domainType(\"Users\")), lit(null))\n },\n actions: {\n create: {\n params: { u: \"Users\", r: \"Runs\" },\n guard: and(\n eq(index(status, param(\"r\")), lit(\"idle\")),\n eq(index(owner, param(\"r\")), lit(null)),\n eq(count(\"Runs\", \"c\", and(\n eq(index(owner, param(\"c\")), param(\"u\")),\n isin(index(status, param(\"c\")), activeStatuses)\n )), lit(0))\n ),\n updates: [\n setMap(\"status\", param(\"r\"), lit(\"queued\")),\n setMap(\"owner\", param(\"r\"), param(\"u\"))\n ]\n },\n cancel: {\n params: { r: \"Runs\" },\n guard: isin(index(status, param(\"r\")), activeStatuses),\n updates: [setMap(\"status\", param(\"r\"), lit(\"cancelled\"))]\n },\n // complete, fail, sweepStale...\n },\n invariants: {\n oneActivePerUser: {\n description: \"At most one queued or running run per user\",\n formula: forall(\"Users\", \"u\", lte(\n count(\"Runs\", \"c\", and(\n eq(index(owner, param(\"c\")), param(\"u\")),\n isin(index(status, param(\"c\")), activeStatuses)\n )),\n lit(1)\n ))\n }\n }\n});\n```\n\n```typescript\n// Your application code - no if/else, no guards, just function calls\nimport { create, cancel, complete } from \"./machine-adapters/AgentRuns.adapter\";\n\n// Each function: opens transaction, locks rows, runs proven interpreter,\n// diffs state, writes changes. If transition is invalid, throws.\nawait create(sql, { u: userId, r: runId });\nawait cancel(sql, { r: runId });\nawait complete(sql, { r: runId });\n```\n\nThe scattered if/else checks are gone. The guard logic lives in the DSL, was proven\ncorrect by the model checker across every possible state, and executes inside the\ngenerated adapter. Your code just calls functions.\n\n## The Mathematical Guarantee\n\nWhen TLA PreCheck passes:\n\n1. **Design is correct** - TLC exhaustively checked every reachable state, every\n interleaving, every edge case. Not sampled. Every single one.\n2. **Interpreter matches the proof** - the TypeScript interpreter and TLC produce\n bit-identical state graphs. The code you run is the spec you proved.\n3. **Database enforces invariants** - generated Postgres constraints (partial unique\n indexes, CHECK constraints) enforce critical invariants at the storage level,\n closing race conditions no application code can prevent.\n4. **Raw writes are blocked** - lint rule catches any code that bypasses the generated\n adapter and writes directly to machine-owned tables.\n\n## Quickstart\n\nIf you are trying TLA PreCheck from GitHub, you do not need to install it globally first.\n\n### 1. Prepare your machine\n\n```bash\nnpx tla-precheck setup\nnpx tla-precheck doctor\n```\n\n`setup` installs the agent skill and downloads the pinned TLC jar into `~/.tla-precheck`.\n`doctor` confirms Java, TLC, and skill installation.\n\n### 2. Start in your codebase\n\n```bash\nnpx tla-precheck init\n```\n\nThat prompts for a machine name or path and creates `MIT License
\n","readmeFilename":"README.md"}