tla-precheck

TLA+ PreCheck — Formal Design Verification

Overview

tla-precheck translates a TypeScript state machine DSL (.machine.ts) into TLA+ specifications, then runs the TLC model checker to exhaustively verify invariants and graph equivalence. Odin integrates it as an opt-in design verification step in the Architect → Guardian flow.

When to Use

Write a .machine.ts file when the feature involves:

• Entity lifecycle management — status transitions, state machines with guard conditions
• Concurrent operations on shared state — multiple actors mutating the same resource
• Financial/billing state changes — charges, refunds, subscriptions where invariant violations cause real damage
• Distributed workflow coordination — where guard conditions are scattered across files/services
• Any invariant that must hold across all possible interleavings — not just the happy path

Complexity level (L1/L2/L3) is a secondary signal. Even a small L1 feature can contain a high-risk lifecycle invariant.

The .machine.ts DSL

A machine definition describes states, events, transitions, and invariants:

import { defineMachine } from 'tla-precheck';

export default defineMachine({
  moduleName: 'AgentRuns',

  constants: {
    Users: { type: 'set', values: ['u1', 'u2'] },
    MaxConcurrent: { type: 'number', value: 1 },
  },

  state: {
    runs: { type: 'map', keys: 'Users', values: ['idle', 'queued', 'running', 'completed'] },
  },

  init: {
    runs: { u1: 'idle', u2: 'idle' },
  },

  actions: {
    QueueRun: {
      guard: (s) => Object.values(s.runs).some((v) => v === 'idle'),
      update: (s) => {
        const user = Object.keys(s.runs).find((u) => s.runs[u] === 'idle')!;
        s.runs[user] = 'queued';
      },
    },
    StartRun: {
      guard: (s) => {
        const running = Object.values(s.runs).filter((v) => v === 'running').length;
        return running < MaxConcurrent && Object.values(s.runs).some((v) => v === 'queued');
      },
      update: (s) => {
        const user = Object.keys(s.runs).find((u) => s.runs[u] === 'queued')!;
        s.runs[user] = 'running';
      },
    },
    CompleteRun: {
      guard: (s) => Object.values(s.runs).some((v) => v === 'running'),
      update: (s) => {
        const user = Object.keys(s.runs).find((u) => s.runs[u] === 'running')!;
        s.runs[user] = 'completed';
      },
    },
  },

  invariants: {
    AtMostOneRunning: (s) =>
      Object.values(s.runs).filter((v) => v === 'running').length <= MaxConcurrent,
  },
});