effect-machine

effect-machine is a statechart library for Effect. Its testing module includes a bounded breadth-first explorer with invariants and shortest counterexamples.

The search works only over Effect statecharts, and async work is not run during the search.

effect-machine explores Effect statecharts breadth-first, with invariants and coverage. Here: a checkout paid for the wrong cart.

Using effect-machine

The code below is in formal-methods-samples/effect-machine-checkout.

The problem

Back during a pending payment lets the reply for the old cart mark the new cart paid.

A checkout sends a charge for the cart total and waits for the reply. While it waits, the user can press Back, add an item and check out again. The first reply can still arrive while the second charge is pending.

The rule: in Paid, the paid amount is the cart total.

Install and set up

pnpm add @typeonce/effect-machine effect@4.0.0-rc.116
pnpm add -D @effect/vitest@4.0.0-rc.116

effect-machine 0.38.0 needs exactly effect 4.0.0-rc.116, and ESNext.Disposable in the tsconfig lib.

Writing the machine

States and events come from Effect schemas; .handle(...) says what each event does.

export const States = Machine.state({
  // Shared by every state: the number of items in the cart.
  fields: { items: Schema.Number },
  states: {
    Cart: {},
    PaymentPending: { fields: { amount: Schema.Number } },
    Paid: { fields: { amount: Schema.Number } },
  },
});
export const targets = Machine.targets(States);

export const Events = Machine.events({
  AddItem: {},
  Checkout: {},
  Back: {},
  // The payment reply carries the amount it was for.
  PaymentSucceeded: { amount: Schema.Number },
});

type Root = { root: { items: number } };

export const machine = Machine.make({ root: States, events: Events }).handle({
  root: () => ({ items: 1 }),
  initial: { target: targets.root.Cart },
  states: {
    Cart: {
      on: {
        AddItem: { update: targets.root, data: ({ root }: Root) => ({ items: root.items + 1 }) },
        Checkout: { target: targets.root.PaymentPending, data: ({ root }: Root) => ({ amount: root.items * price }) },
      },
    },
    PaymentPending: {
      on: {
        Back: { target: targets.root.Cart },
        PaymentSucceeded: { target: targets.root.Paid, data: ({ event }) => ({ amount: event.amount }) },
      },
    },
    Paid: {},
  },
});

Running it

Only when every reply still in flight is offered does it find the bug: paid 10 for a cart of 20.

MachineTest.explore walks the machine breadth-first and checks the rule in every state. It only sends the events the test offers, so the test offers every payment reply that can still arrive:

// checkout.effect-machine.test.ts (shortened)
// Every charge still waiting for its reply: each Checkout adds one, each reply removes one.
function inFlight(steps: readonly Step[]): number[] {
  const amounts = new Set<number>();
  for (const { event, before } of steps) {
    if (event._tag === 'Checkout' && States.matches(before, 'Cart')) amounts.add(before.value.items * price);
    if (event._tag === 'PaymentSucceeded') amounts.delete(event.amount);
  }
  return [...amounts].sort((a, b) => a - b);
}

const error = yield* Effect.flip(
  MachineTest.explore(machine, {
    events: ({ snapshot, trace }) => [
      ...userEvents(snapshot),
      ...inFlight(trace.steps).map((amount) => ({ _tag: 'PaymentSucceeded', amount })),
    ],
    // Two snapshots with different replies in flight are different states.
    stateKey: ({ snapshot, trace }) => JSON.stringify([snapshot, inFlight(trace.steps)]),
    invariants: [invariant],
  }),
);

{"_tag":"Checkout"} → {"_tag":"Back"} → {"_tag":"AddItem"} → {"_tag":"Checkout"} → {"_tag":"PaymentSucceeded","amount":10}
[ 'paid 10 for a cart of 20' ]

That is the shortest counterexample: check out one item, go back, add a second, check out again, and the reply to the first charge marks the order paid at 10 for a cart of 20.

Two easier versions of the same test miss it. With the charge written as an invoke, the explorer never runs it, so Paid is never reached (4 states, complete). With only the reply to the current charge offered, it passes (12 states, complete).

Fixing the bug

Remove Back from PaymentPending. The same exploration passes.

The fix removes Back from PaymentPending:

Diff style

PaymentPending: {
  on: {
    Back: { target: targets.root.Cart },
    PaymentSucceeded: { target: targets.root.Paid, data: ({ event }) => ({ amount: event.amount }) },
  },
},

The same exploration, with every reply still in flight, passes:

{ states: 6, plannedTransitions: 7, retainedEdges: 7, maxDepth: 3 } Complete

Project layout and CI

Commit the machine and the test. CI runs the test like any other Vitest test. Nothing else to install.

./
├── .github/workflows/ci.yml
├── src/checkout.ts                        the machine
└── src/checkout.effect-machine.test.ts    the events to offer, the rule, the exploration

Both files are committed; nothing is generated. CI needs no API key, browser or other tool. In a project, the test expects the exploration to pass and checks that completeness._tag is Complete:

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 breaks the rule: vitest run, with the shortest list of events to the bug.
The machine grows past the limits (by default 1,000 states): the Complete check. Without it, the test passes after checking only part of the machine.

Making changes

Change the machine, offer the new events, run the test, commit.

Change the machine.
Add any new event to the events the test offers. The explorer only sends the events you list.
If a new async reply can arrive late, offer it too, like inFlight does.
Run the test. It must pass and report Complete.
Commit the machine and the test together.

Strengths

It checks the machine your app runs. There is no separate model to keep in line with the code.
It checks every state reachable with the events you list. A failure comes back as the shortest list of events that breaks the rule.
Its coverage report is clear. It named the exact step that was never taken, and it says so when it stopped at a limit instead of checking everything.
It does more than explore. It can also generate test scenarios, compare recorded runs with a reference model, and inspect a running machine.

Limitations

You add the async replies yourself. It does not run them while exploring. In the example it reported full coverage and no bug until the replies still in flight were listed by hand in the test.
It only works on code written with effect-machine. pnueli, TLA+ or Quint check a separate model instead.
It needs Effect 4. Today that is a pinned release candidate.