@stateproof/core

TypeScript state machines → TLA+ model checking → exhaustive verification

Property-based testing says "we checked 10,000 random inputs." Stateproof says "we checked all 847,293 reachable states."

---

What It Does

Define state machines with a fluent TypeScript DSL. Stateproof compiles them to TLA+, runs the TLC model checker to exhaustively verify every reachable state, and generates test traces you can run in Vitest.

TypeScript DSL  →  AST  →  TLA+ Spec  →  TLC Model Checker  →  VerifyResult
                    ↓                                                ↓
               Runtime Machine                                Violation Traces
                    ↓                                                ↓
              Generated Code                                  Generated Tests

The spec is the implementation. Guards and actions execute at runtime too.

Quick Start

pnpm add @stateproof/core

import { machine, verify, createRuntime, generateTLA } from '@stateproof/core'

const counter = machine('BoundedCounter')
  .states('counting', 'done')
  .initial('counting')
  .context({ value: 0 })
  .transition('increment', {
    from: 'counting',
    guard: (ctx) => ctx.value < 5,
    action: (ctx) => {
      ctx.value += 1
    }
  })
  .transition('finish', {
    from: 'counting',
    to: 'done',
    guard: (ctx) => ctx.value >= 5
  })
  .invariant('bounded', (ctx) => ctx.value <= 5)
  .invariant('done means five', (ctx) => ctx.state !== 'done' || ctx.value >= 5)

// Generate TLA+ and verify exhaustively
const result = await verify(counter)
console.log(result.ok) // true — all states satisfy all invariants
console.log(result.statesExplored) // every reachable state checked

// Or use the spec as a runtime state machine
const rt = createRuntime(counter)
rt.send('increment') // true
rt.context.value // 1
rt.send('finish') // false — guard blocks (value < 5)

Concurrent Composition

Where stateproof earns its keep. Model N processes competing for shared resources — TLC explores every possible interleaving.

import { machine, concurrent, generateConcurrentTLA } from '@stateproof/core'

const worktree = machine('WorktreeBinding')
  .states('free', 'acquiring', 'bound', 'working', 'releasing')
  .initial('free')
  .context({ owner: '' })
  .transition('acquire', {
    from: 'free',
    to: 'acquiring',
    action: (ctx) => {
      ctx.owner = 'agent'
    }
  })
  .transition('bind', { from: 'acquiring', to: 'bound' })
  .transition('start_work', { from: 'bound', to: 'working' })
  .transition('release', {
    from: ['working', 'bound'],
    to: 'releasing',
    action: (ctx) => {
      ctx.owner = ''
    }
  })
  .transition('freed', { from: 'releasing', to: 'free' })

const system = concurrent('MultiAgentWorktrees')
  .instances('worktree', worktree, { count: 3 })
  .shared('totalActive', 0)
  .invariant(
    'no double allocation',
    '\\A i, j \\in Worktrees: i # j => worktree_owner[i] = "" \\/ worktree_owner[j] = "" \\/ worktree_owner[i] # worktree_owner[j]'
  )

const { spec, cfg } = generateConcurrentTLA(system.build())
// TLC exhaustively checks all interleavings of 3 agents

What You Get

Feature	Description
machine()	Fluent builder — states, context, transitions, guards, actions, invariants, liveness
concurrent()	Compose N instances with shared state and interactions
verify()	Compile to TLA+, run TLC, get structured results with violation traces
createRuntime()	Use the spec as an executable state machine
generateRuntimeCode()	Emit standalone TypeScript from the spec
generateTests()	BFS trace generation — coverage and violation strategies
generateTLA()	Inspect the generated TLA+ directly
toMermaidStateDiagram()	Visualise specs as Mermaid diagrams
diffSpecs()	Structural diff between spec versions
CLI	stateproof check, verify, generate, tla, mermaid, diff
Vitest plugin	Integrate verification into your test suite

Why Not Just Property-Based Testing?

Property-based testing (QuickCheck, fast-check) generates random inputs. It's good but probabilistic — you're sampling the state space and hoping you hit the edge cases.

TLC model checking is exhaustive. It builds the complete state graph and checks every single reachable state against every invariant. If there's a violation, it gives you the exact step-by-step path to reproduce it. No randomness, no coverage gaps.

The tradeoff is that model checking requires bounded state spaces. Stateproof handles this automatically — guards naturally bound the exploration, and verify() options let you set explicit bounds.

Requirements

• Node.js 18+
• Java (for TLC model checking) — optional; compilation, runtime, and test generation work without it

Documentation

• Architecture
• DSL Reference
• TLA+ Compilation
• Examples
• Implementation Phases

License

ISC