stateproof

stateproof lets you write a model in TypeScript and check every reachable state. It compiles a subset of TypeScript to TLA+, is MIT licensed, is not on npm, and its own README example fails.

stateproof compiles a TypeScript state machine to TLA+ and checks it with TLC. Here: a subscription renewed after a cancel.

Using stateproof

The code below is in formal-methods-samples/stateproof-subscription. We ran it from the repository at commit 4cb6308 (March 2026), on Node 24 with Java 25. The output is from our run.

The problem

renew also runs on canceling plans, so a canceled plan is charged and active again.

A subscription service lets a customer cancel at any time. The plan then runs to the end of the paid period, and until then the customer can resume it. At the end of each period a renewal job charges every live plan and keeps it active:

// subscription.ts (shortened)
.transition('renew', { from: ['active', 'canceling'], to: 'active' })

“Live” was taken to include plans that are canceling. So a plan canceled during the period is charged again and made active at the next renewal, as if the customer had never canceled.

Install and set up

The README says pnpm add @stateproof/core, but the package is not on npm. It runs from source; the sample’s setup script clones it at the commit above:

git clone https://github.com/HexaField/stateproof

Needs Java for TLC.

Writing the machine (use AI)

A fluent builder of states, context, transitions and invariants, translated to TLA+ from their source text.

import { machine } from '@stateproof/core'

export const subscription = machine('Subscription')
  .states('trial', 'active', 'canceling', 'canceled')
  .initial('trial')
  // Flat data next to the state: set when the customer cancels.
  .context({ canceledByUser: false })
  .transition('activate', { from: 'trial', to: 'active' })
  .transition('cancel', {
    from: 'active',
    to: 'canceling',
    action: (ctx) => {
      ctx.canceledByUser = true
    }
  })
  .transition('resume', {
    from: 'canceling',
    to: 'active',
    action: (ctx) => {
      ctx.canceledByUser = false
    }
  })
  .transition('renew', { from: ['active', 'canceling'], to: 'active' })
  .transition('expire', { from: 'canceling', to: 'canceled' })
  .transition('resubscribe', {
    from: 'canceled',
    to: 'active',
    action: (ctx) => {
      ctx.canceledByUser = false
    }
  })
  // Must hold in every reachable state.
  .invariant('canceled plans are not renewed', (ctx) => !(ctx.canceledByUser && ctx.state === 'active'))

Guards, actions and invariants are not run by the checker. stateproof reads their source text with fn.toString() and translates it into TLA+. The renew line above became:

renew ==
  /\ state \in {"active", "canceling"}
  /\ state' = "active"
  /\ UNCHANGED canceledByUser

The same machine also runs in your code, and there the bug is real. createRuntime(subscription), then activate, cancel and renew, leaves the runtime in active with canceledByUser still true; the sample’s test checks it.

Running it

The trace: activate, cancel, renew.

// verify.ts (shortened)
const result = await verify(subscription, { tlcPath: resolve(jar) })

The result, without the generated tlaSpec and the raw tlcOutput:

{
  "ok": false,
  "statesExplored": 6,
  "distinctStates": 4,
  "depth": 4,
  "duration": 404,
  "violations": [
    {
      "invariant": "canceled_plans_are_not_renewed",
      "trace": [
        { "action": "state", "state": { "state": "trial", "canceledByUser": false }, "expectedState": "trial" },
        { "action": "state", "state": { "state": "active", "canceledByUser": false }, "expectedState": "active" },
        { "action": "state", "state": { "state": "canceling", "canceledByUser": true }, "expectedState": "canceling" },
        { "action": "state", "state": { "state": "active", "canceledByUser": true }, "expectedState": "active" }
      ],
      "type": "invariant"
    }
  ]
}

The trace is activate, cancel, renew. Every step says "action": "state", so which transition ran has to be read from the difference between two states. The invariant’s name comes back with its spaces turned into underscores.

Fixing the bug

Renew active plans only: ok: true, 4 states.

The fix: the renewal job now renews active plans only; a canceling plan runs out and expires:

Diff style

// A subscription: a canceled plan runs to the end of its period, and the customer can resume it until then.
import { machine } from './vendor/stateproof/packages/core/src/index.ts';

export const subscription = machine('Subscription')
  .states('trial', 'active', 'canceling', 'canceled')
  .initial('trial')
  // Flat data next to the state: set when the customer cancels.
  .context({ canceledByUser: false })
  .transition('activate', { from: 'trial', to: 'active' })
  .transition('cancel', {
    from: 'active',
    to: 'canceling',
    action: (ctx) => {
      ctx.canceledByUser = true
    }
  })
  .transition('resume', {
    from: 'canceling',
    to: 'active',
    action: (ctx) => {
      ctx.canceledByUser = false
    }
  })
  .transition('renew', { from: ['active', 'canceling'], to: 'active' })
  .transition('expire', { from: 'canceling', to: 'canceled' })
  .transition('resubscribe', {
    from: 'canceled',
    to: 'active',
    action: (ctx) => {
      ctx.canceledByUser = false
    }
  })
  // Must hold in every reachable state.
  .invariant('canceled plans are not renewed', (ctx) => !(ctx.canceledByUser && ctx.state === 'active'))

// A subscription: a canceled plan runs to the end of its period, and the customer can resume it until then.
import { machine } from './vendor/stateproof/packages/core/src/index.ts';

export const subscription = machine('Subscription')
  .states('trial', 'active', 'canceling', 'canceled')
  .initial('trial')
  // Flat data next to the state: set when the customer cancels.
  .context({ canceledByUser: false })
  .transition('activate', { from: 'trial', to: 'active' })
  .transition('cancel', {
    from: 'active',
    to: 'canceling',
    action: (ctx) => {
      ctx.canceledByUser = true
    }
  })
  .transition('resume', {
    from: 'canceling',
    to: 'active',
    action: (ctx) => {
      ctx.canceledByUser = false
    }
  })
  .transition('renew', { from: ['active', 'canceling'], to: 'active' })
  .transition('renew', { from: 'active', to: 'active' })
  .transition('expire', { from: 'canceling', to: 'canceled' })
  .transition('resubscribe', {
    from: 'canceled',
    to: 'active',
    action: (ctx) => {
      ctx.canceledByUser = false
    }
  })
  // Must hold in every reachable state.
  .invariant('canceled plans are not renewed', (ctx) => !(ctx.canceledByUser && ctx.state === 'active'))

−1 removal 34 lines

+1 addition 34 lines

1 // A subscription: a canceled plan runs to the end of its period, and the customer can resume it until then.

2 import { machine } from './vendor/stateproof/packages/core/src/index.ts';

4 export const subscription = machine('Subscription')

5 .states('trial', 'active', 'canceling', 'canceled')

6 .initial('trial')

7 // Flat data next to the state: set when the customer cancels.

8 .context({ canceledByUser: false })

9 .transition('activate', { from: 'trial', to: 'active' })

10 .transition('cancel', {

11 from: 'active',

12 to: 'canceling',

13 action: (ctx) => {

14 ctx.canceledByUser = true

15 }

16 })

17 .transition('resume', {

18 from: 'canceling',

19 to: 'active',

20 action: (ctx) => {

21 ctx.canceledByUser = false

22 }

23 })

24 .transition('renew', { from: ['active', 'canceling'], to: 'active' })

24 .transition('renew', { from: 'active', to: 'active' })

25 .transition('expire', { from: 'canceling', to: 'canceled' })

26 .transition('resubscribe', {

27 from: 'canceled',

28 to: 'active',

29 action: (ctx) => {

30 ctx.canceledByUser = false

31 }

32 })

33 // Must hold in every reachable state.

34 .invariant('canceled plans are not renewed', (ctx) => !(ctx.canceledByUser && ctx.state === 'active'))

// A subscription: a canceled plan runs to the end of its period, and the customer can resume it until then.
import { machine } from './vendor/stateproof/packages/core/src/index.ts';
export const subscription = machine('Subscription')
  .states('trial', 'active', 'canceling', 'canceled')
  .initial('trial')
  // Flat data next to the state: set when the customer cancels.
  .context({ canceledByUser: false })
  .transition('activate', { from: 'trial', to: 'active' })
  .transition('cancel', {
    from: 'active',
    to: 'canceling',
    action: (ctx) => {
      ctx.canceledByUser = true
    }
  })
  .transition('resume', {
    from: 'canceling',
    to: 'active',
    action: (ctx) => {
      ctx.canceledByUser = false
    }
  })
  .transition('renew', { from: ['active', 'canceling'], to: 'active' })
  .transition('expire', { from: 'canceling', to: 'canceled' })
  .transition('resubscribe', {
    from: 'canceled',
    to: 'active',
    action: (ctx) => {
      ctx.canceledByUser = false
    }
  })
  // Must hold in every reachable state.
  .invariant('canceled plans are not renewed', (ctx) => !(ctx.canceledByUser && ctx.state === 'active'))

// A subscription: a canceled plan runs to the end of its period, and the customer can resume it until then.
import { machine } from './vendor/stateproof/packages/core/src/index.ts';

export const subscription = machine('Subscription')
  .states('trial', 'active', 'canceling', 'canceled')
  .initial('trial')
  // Flat data next to the state: set when the customer cancels.
  .context({ canceledByUser: false })
  .transition('activate', { from: 'trial', to: 'active' })
  .transition('cancel', {
    from: 'active',
    to: 'canceling',
    action: (ctx) => {
      ctx.canceledByUser = true
    }
  })
  .transition('resume', {
    from: 'canceling',
    to: 'active',
    action: (ctx) => {
      ctx.canceledByUser = false
    }
  })
  .transition('renew', { from: 'active', to: 'active' })
  .transition('expire', { from: 'canceling', to: 'canceled' })
  .transition('resubscribe', {
    from: 'canceled',
    to: 'active',
    action: (ctx) => {
      ctx.canceledByUser = false
    }
  })
  // Must hold in every reachable state.
  .invariant('canceled plans are not renewed', (ctx) => !(ctx.canceledByUser && ctx.state === 'active'))

{
  "ok": true,
  "statesExplored": 7,
  "distinctStates": 4,
  "depth": 4,
  "duration": 261,
  "violations": []
}

The machine has no end state: resubscribe leads out of canceled. That matters, because deadlock checking is on by default and a state with no way out fails the check (see Limitations).

Project layout and CI

Commit the machine and a verify script. CI clones stateproof, sets up Java and runs TLC.

./
├── .github/workflows/ci.yml
├── src/subscription.ts        the machine; your code also runs it with createRuntime
├── stateproof/
│   ├── setup.ts               clones stateproof at a fixed commit
│   └── verify.ts              runs verify() and sets the exit code
└── vendor/stateproof/         the clone, not committed

The TLA+ copy is written to a temp folder on each run, so nothing generated is committed. CI needs Java. stateproof downloads tla2tools.jar if it does not find one, and Node 24 runs the .ts files as they are:

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

# .github/workflows/ci.yml (steps)
- uses: actions/setup-node@v7
  with: { node-version: 24 }
- uses: actions/setup-java@v6
  with: { distribution: temurin, java-version: 21 }
- run: node stateproof/setup.ts
# Without Java or TLC, verify() returns ok: true and 0 states. So verify.ts ends with
# process.exit(result.ok && result.statesExplored > 0 ? 0 : 1)
- run: node stateproof/verify.ts

What fails when:

A change breaks a rule: verify.ts, with the trace to the bug.
A change adds a state with no way out: verify.ts, as a deadlock violation, unless you pass checkDeadlocks: false.
Java or TLC is missing: verify.ts, but only because of the statesExplored check.

Making changes

Change the machine, add a rule if needed, run verify, read the TLA+ for new code, commit.

Change the machine in subscription.ts. Your code runs the same machine, so there is no second copy to update.
For a new rule, add an .invariant(...).
Run verify.ts. In a trace, find which transition ran from the difference between two states.
For a new guard or action, read the TLA+ in the result’s tlaSpec. The translation can be wrong without an error.
Commit the machine.

Strengths

It checks every reachable state. A TLA+ copy is made from your builder code and checked by TLC.
Strong on “eventually” rules. They work through TLC.
It does more than check. It can also draw diagrams, compare versions of a spec and check a real implementation.

Limitations

You have to trust its translation to TLA+. It covers only code the translator understands, and it can be silently wrong (for example, null becomes the string "null"), so what TLC checks and what runs can differ.
ok: true is not enough. A run where TLC could not start still says ok: true; check statesExplored too.
Timing and async are not covered. The check does not look at async code.
It needs Java and some setup. You give it the full path to the TLC jar, and actions that take arguments must be written in raw TLA+.
A final state fails by default. It counts a final state as a deadlock until you pass checkDeadlocks: false; this is why the README’s quick start fails.