stifinder

stifinder is a state-space explorer for JavaScript and TypeScript. It answers a question most checkers do not ask: not only “is there a failing trace”, but “what is the failing trace that needs the fewest things to go differently than expected”.

stifinder reports the failure that needs the fewest deviations from the expected schedule. Here: an outbox relay with crashes and retries.

Using stifinder

The code below is in formal-methods-samples/stifinder-outbox.

The problem

A broker retry can deliver an outbox event twice.

A transactional outbox. The order service writes the order and an outbox row in one transaction. A relay reads the row, publishes the event to a broker, and marks the row sent. The relay can crash at any step and restart, and the broker can time out after it has already delivered the message, so the relay retries.

The rules: every committed order is published, and the consumer applies each order at most once.

Install and set up

pnpm add -D stifinder valsem

Needs Node 22+.

Writing the model (use AI)

A model is initialState, getEvents, applyEvent and invariants. Event index 0 is the expected step; the rest are faults.

// stifinder-model.ts (shortened)
export function outboxModel(relay: Relay): Model<State, Event> {
  return {
    initialState: relay.initial,
    // Index 0 is the expected step; the rest are faults, each with its own budget key.
    getEvents: (s) => [
      ...expected(relay, s),
      ...(relay.publishing(s) ? [{ event: 'broker times out after delivery', cost: ['retry'] }] : []),
      ...(s.relay === 'idle' ? [] : [{ event: 'relay crashes', cost: ['crash'] }]),
    ],
    applyEvent: (s, e) => ({ to: effects[e](relay, s) }),
    invariant: (s) => (s.applied > 1 ? { error: new Error('the order was applied twice') } : undefined),
    // Checked only when no events are left.
    terminalInvariant: (s) =>
      s.applied === 0 ? { error: new Error('the committed order was never published') } : undefined,
  };
}

Running it

One retry duplicates the event. Runs without a fault are clean.

exploreIteratively tries zero faults first, then one, and so on, up to the budget:

const result = await exploreIteratively(outboxModel(outbox), { baseBudget: { crash: 2, retry: 2 } });

result.violation.error; // the order was applied twice
result.violation.steps; // commit, read row, broker times out after delivery, publish
result.violation.cost;  // { retry: 1, __deviations__: 1 }

One retry is enough. A relay that marks the row before publishing fails the other rule: one crash between the two steps loses the event.

Fixing the bug

An idempotency key at the consumer. 7 states, exhaustive: true, for any number of crashes and retries.

The consumer checks an idempotency key and drops a delivery it has already applied:

Diff style

export function consume(applied: number): number {
  return applied + 1;
  return applied > 0 ? applied : applied + 1;
}

const fixed = await exploreIteratively(outboxModel(fixedOutbox), { baseBudget: { crash: 2, retry: 2 } });

fixed.violation;  // null
fixed.exhaustive; // true, 7 states

Faults are a budget, not part of the state, so a complete clean run holds for any number of crashes and retries.

Project layout and CI

Commit the model and the test. CI runs the test like any other test on Node 22+. No API key.

./
├── .github/workflows/ci.yml
├── src/relay.ts                   the real relay and consumer
└── model/
    ├── outbox.ts                  the steps, as plain functions
    ├── stifinder-model.ts         events, faults and rules
    └── outbox.stifinder.test.ts   runs the search in Vitest

Everything is committed; nothing is generated. stifinder is a library with no CLI. exploreIteratively returns a result and does not throw, so the test checks two things: violation is null, and exhaustive is true. A run that finds nothing is complete only when exhaustive is true.

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

# .github/workflows/ci.yml (steps)
- uses: actions/setup-node@v7
  with:
    node-version: 22
- run: npm ci
- run: npm test

What fails when:

The model can apply an order twice, or lose it: the violation check, with the steps and the faults they need.
The budget is too small to reach every state: the exhaustive check.
Only the real code changes: nothing. The test does not run src/.

Making changes

Change the code, make the same change in the model, run the test, commit both.

Change the real code.
Make the same change in model/outbox.ts, by hand or with a coding agent. Nothing checks that the two match.
A new fault, like a timeout or a crash at a new step, is a new event in getEvents with its own budget key. Add the key to baseBudget.
Run npm test.
Commit the code and the model together.

Strengths

It tells you what the failure costs. It finds the failure with the fewest faults (crashes, retries) first, then the shortest.
It says if the search was complete. A clean full run covers any number of faults, while in pnueli it covers only the limits written in the spec.
It checks how the run ends. A rule on the final state comes with the steps that break it.
A deeper search does not start over. Earlier results are kept when you raise the fault limit.
Small to set up. You need only the npm package and four functions: the start state, the possible events, what each event does, and the rules.

Limitations

It checks the model, not your code. There is nothing to check your real code against the model.
It is a checking engine only. There are no named actions.
Faults must be written into the model. Crashes and retries are events you add yourself.
Always pass a budget. With the default baseBudget of {}, every fault is over budget and the search finds nothing, even when the code is broken.