XState

XState is a library for state machines and statecharts in JavaScript and TypeScript. The app runs the machine itself. Its xstate/graph module walks the machine: for the events you list, it finds every state the machine can reach, and a shortest path to each one. You check your rule on those states in a normal test.

It is formal-ish. The walk covers every reachable state, but only of one machine, and only for the events you list.

xstate/graph walks every reachable state of an XState machine. Here: a signup without the terms.

Using XState

The code below is in formal-methods-samples/xstate-signup. We ran it with XState 5.33.2 and Node 24. The output is from our run.

The problem

The review page shows the checkbox again, and Submit does not check it.

A signup has a terms step and a review step. You cannot leave the terms step without ticking the box. The review page shows the checkbox again, so users can change their mind:

signup.ts

import { assign, setup } from 'xstate';

export const signup = setup({
  types: {
    context: {} as { accepted: boolean },
    events: {} as { type: 'TOGGLE' } | { type: 'NEXT' } | { type: 'SUBMIT' },
  },
  actions: { toggle: assign({ accepted: ({ context }) => !context.accepted }) },
}).createMachine({
  initial: 'terms',
  context: { accepted: false },
  states: {
    terms: {
      on: {
        TOGGLE: { actions: 'toggle' },
        NEXT: { target: 'review', guard: ({ context }) => context.accepted },
      },
    },
    // The review page shows the checkbox again, so users can change their mind.
    review: {
      on: {
        TOGGLE: { actions: 'toggle' },
        SUBMIT: 'submitted',
      },
    },
    submitted: { type: 'final' },
  },
});

signup.test.ts

test('you cannot get past the terms without accepting them', () => {
  const actor = createActor(signup).start();
  actor.send({ type: 'NEXT' }); // not accepted: blocked
  expect(actor.getSnapshot().value).toBe('terms');
});

The test passes. The guard on the terms step works. But a user can tick the box, go to review, untick it there, and submit.

Install

npm install xstate

xstate/graph ships with it.

Writing the check

getShortestPaths returns a path to every reachable state; the test checks the rule on each one.

// signup.graph.test.ts (shortened)
import { getShortestPaths } from 'xstate/graph';

test('nobody is signed up without accepting the terms', () => {
  // One shortest path to every state (value and context) these events can reach.
  const paths = getShortestPaths(signup, { events: [{ type: 'TOGGLE' }, { type: 'NEXT' }, { type: 'SUBMIT' }] });
  console.log(`${paths.length} reachable states`);

  // Check the rule on every one of them, and print the path to any that breaks it.
  const broken = paths
    .filter((p) => p.state.value === 'submitted' && !p.state.context.accepted)
    .map((p) => p.steps.map((s) => s.event.type).join(' → '));
  expect(broken).toEqual([]);
});

Running it

6 reachable states, and one 4-step path to a signup without the terms.

$ npx vitest run signup.graph.test.ts
6 reachable states

 × nobody is signed up without accepting the terms

AssertionError: expected [ Array(1) ] to deeply equal []

- Expected
+ Received

- []
+ [
+   "xstate.init → TOGGLE → NEXT → TOGGLE → SUBMIT",
+ ]

The path is a list of events. Send them to the real actor and you get the same bad state, so it doubles as a regression test.

Fixing the bug

Submit checks the box too. 5 reachable states, and the rule holds in all of them.

The fix: Submit checks the box too.

Before the fix Diff With the fix

import { assign, setup } from 'xstate';
export const signup = setup({
  types: {
    context: {} as { accepted: boolean },
    events: {} as { type: 'TOGGLE' } | { type: 'NEXT' } | { type: 'SUBMIT' },
  },
  actions: { toggle: assign({ accepted: ({ context }) => !context.accepted }) },
}).createMachine({
  initial: 'terms',
  context: { accepted: false },
  states: {
    terms: {
      on: {
        TOGGLE: { actions: 'toggle' },
        NEXT: { target: 'review', guard: ({ context }) => context.accepted },
      },
    },
    // The review page shows the checkbox again, so users can change their mind.
    review: {
      on: {
        TOGGLE: { actions: 'toggle' },
        SUBMIT: 'submitted',
        SUBMIT: { target: 'submitted', guard: ({ context }) => context.accepted },
      },
    },
    submitted: { type: 'final' },
  },
});

With the fix, the machine has 5 reachable states, none of them breaks the rule, and the test passes.

Project layout and CI

The graph check is a normal test file next to the machine. CI runs your tests; nothing else to install.

./
├── .github/workflows/ci.yml
└── src/
    ├── signup.ts                  the machine the app runs
    ├── signup.test.ts             normal unit tests
    └── signup.graph.test.ts       walks every reachable state, checks the rule

Everything is committed. Nothing is generated, and CI needs only Node:

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

# .github/workflows/ci.yml (steps)
- run: npm ci
- run: npx vitest run

What fails when:

• A change lets a reachable state break the rule: signup.graph.test.ts, with the list of events that leads to it.
• A new event is not in the test’s events list: nothing fails. The walk never sends that event.

Making changes

Change the machine, add new events and rules to the graph test, run the tests, commit.

1. Change the machine.
2. Add any new event to the events list in signup.graph.test.ts.
3. If the change adds a rule, check it in the same test.
4. Run npx vitest run. If it fails, send the printed events to the real actor to see the bug.
5. Commit the machine and the tests together.

XState machines and TLA+ state machines

Both are called state machines. XState lists named states of one machine; TLA+ and Quint describe variables and try every order of many actors.

Both are called state machines, but they describe different things:

	XState machine	TLA+ or Quint state machine
What you write	Named states and the events that move between them, plus some context data	Variables, and actions that change them
Who lists the states	You, one by one	The checker, from every combination of values
Concurrency	One machine; other machines are separate actors	All actors in one state; every order of their steps is tried
Async work	invoke and promises, outside the walk	Written as steps, so every order is tried
Checking	xstate/graph walks the states; your test checks the rule	A model checker checks invariants and “eventually” rules
Runs in production	Yes, it is the app code	No, it is a separate spec

XState fits when the flow of one component or one process is the problem. When the problem is several things running at once (two tabs, a retry and a timer, two workers), see TLA+ and Quint. More on the difference in State machines and FSMs.

Strengths

• It checks the machine that runs. There is no separate model to write or keep in sync.
• The shortest path to the bug. You get the shortest list of events that breaks your rule, and you can send it to the real machine.
• Nothing extra to install. xstate/graph ships with xstate 5.

Limitations

• It sees only the machine’s own states and events. The async code the machine calls is not checked, and neither are two machines running side by side.
• Only the events you list. An event you do not list is never tried, and data with many values (counters, text) makes the number of states grow fast.
• Your test holds the rules. It lists states and paths but has no rules of its own.
• No “eventually” rules. It cannot check them.

Links

Built by Stately, the company of David Khourshid; open source.

• Stately: https://stately.ai/
• XState: https://stately.ai/docs/xstate
• xstate/graph: https://stately.ai/docs/xstate-graph
• XState on GitHub: https://github.com/statelyai/xstate
• XState on npm: https://www.npmjs.com/package/xstate