SpecCraft TS

SpecCraft TS is the TypeScript engine of SpecCraft. It is a model checker as a library: the spec is ordinary TypeScript data and functions, and the library explores every reachable state, checks invariants, and returns the shortest trace to a state that breaks one. Other tools of this kind are pnueli, stifinder and Polygraph.

Using SpecCraft TS

The example is examples/crosswalk in the repository, run with npx tsx run.ts. A pedestrian button is added to a car light that already cycles on its own timer. The one rule that matters: the walk signal is only on while the car light is red.

A spec is state, actions with a guard and an effect, and invariants:

import type { Spec } from '@speccraft-io/core';

type State = { carLight: 'green' | 'yellow' | 'red'; walkSignal: 'walk' | 'dontwalk'; requested: boolean };

export const spec: Spec<State> = {
  init: () => ({ carLight: 'green', walkSignal: 'dontwalk', requested: false }),
  actions: [
    { name: 'press button', guard: (s) => !s.requested, effect: (s) => ({ ...s, requested: true }) },
    { name: 'car turns yellow', guard: (s) => s.carLight === 'green', effect: (s) => ({ ...s, carLight: 'yellow' }) },
    { name: 'car turns red', guard: (s) => s.carLight === 'yellow', effect: (s) => ({ ...s, carLight: 'red' }) },
    // The bug: never checks that the car light is red.
    {
      name: 'grant walk',
      guard: (s) => s.requested && s.walkSignal === 'dontwalk',
      effect: (s) => ({ ...s, walkSignal: 'walk', requested: false }),
    },
    { name: 'end walk', guard: (s) => s.walkSignal === 'walk', effect: (s) => ({ ...s, walkSignal: 'dontwalk' }) },
    {
      name: 'car turns green',
      guard: (s) => s.carLight === 'red' && s.walkSignal === 'dontwalk',
      effect: (s) => ({ ...s, carLight: 'green' }),
    },
  ],
  invariants: [
    {
      name: 'pedestrians only get a walk signal while car traffic is stopped',
      check: (s) => s.walkSignal !== 'walk' || s.carLight === 'red',
    },
  ],
};

explore(spec) walks every reachable state breadth-first:

Step 1: the spec, as first written
  visited 12 states
  VIOLATED: pedestrians only get a walk signal while car traffic is stopped
  trace: press button -> grant walk

Step 2: the fixed spec
  visited 8 states
  holds: pedestrians only get a walk signal while car traffic is stopped

The fix adds s.carLight === 'red' to the grant walk guard. Then checkConformance(spec, real) walks the same state graph against a real implementation:

Step 1b: checking the real, shipped implementation against that same buggy spec
  conforms on all 12 reachable states - the real code has the same bug

Step 3: checking a real implementation against the proven-correct spec
  MISMATCH on "grant walk"
  trace: press button -> car turns yellow -> car turns red -> grant walk
  expected: {"carLight":"red","walkSignal":"walk","requested":false}
  actual:   {"carLight":"red","walkSignal":"walk","requested":true}

Step 4: the fixed implementation
  conforms on all 8 reachable states

The real code forgot to clear requested after granting the walk, so the next cycle would grant a walk nobody asked for. No invariant is broken in that state yet; the mismatch shows the code and the spec disagree.

Inline specs

The second mode puts the spec on the real class. Decorators (or a plain annotate() call) attach a guard and effect to each real method and map real fields to small spec values: a cart’s item list becomes 'none' | 'one' | 'many' per item. Async calls go through a channel the explorer controls, so it delivers every reply in every order.

@spec.Model<CartState>({
  invariants: {
    "a settled quote was quoted for the cart's current items": (s) =>
      s.deliveryStatus !== 'idle' || s.quotedForItems === null || sameLevels(s.quotedForItems, s.items),
  },
})
export class Cart {
  @spec.State(itemLevels) items: CartItem[] = [];
  @spec.State deliveryStatus: DeliveryStatus = 'idle';

  @spec.Action<CartState, ['A' | 'B', number, number]>({
    name: 'add item',
    args: [['A', 1, 5], ['B', 1, 9]],
    guard: () => true,
    effect: (s, name) => requested(s, { ...s.items, [name]: s.items[name] === 'none' ? 'one' : 'many' }),
  })
  addItem(name: string, quantity: number, cost: number): void {
    // the real method
  }
}

exploreAnnotated(Cart, (env) => new Cart(explorableDeps(env))) checks the spec and the class in one run. In the annotated cart example, the spec holds, and the real class applies a stale delivery quote the spec rejects: a quote for an older cart arrives after a newer one.

Results on the samples

SpecCraft TS was also run on the examples from the other tool pages:

Example	Result
Webhook double charge	All 20 reachable states, a 4-step trace to the double charge; the fixed spec holds in all 12
Stock reservation	All 25 reachable states, the shortest trace to negative stock; the fixed spec holds in 13, and the real class matches it in all 13. It missed the quantity-0 bug Hegel found, because the spec only tries quantities 1 and 2
Distributed lock	The same five-step trace after 566 states; the fenced store holds in 37, 283 and 2,521 states. Conformance on a real lock client finds the one step where plain storage accepts a write the spec rejects. It cannot find the lock-out pnueli’s liveness check finds
Checkout	All 26 reachable states and a five-step trace; the fixed spec has 8
Transactional outbox	Four-step traces for the lost event (27 states) and the duplicate (71 states); the fixed relay holds in 39, within the bounds in the spec
Autosave	A stale save in 6 steps, where three fake-timer tests pass on the buggy code
Job lease	The late renewal in 29 states, where the Effect cancel tests pass on the buggy code

Strengths

The model is plain TypeScript. Nothing is translated, and the model can call your own helper functions.
Only the npm package. No Java or other tools are needed.
It checks every reachable state of the model. When a rule breaks, you get the shortest list of actions that breaks it.
It can check your real class against the model. With rules on a real class, it also tries every order of async replies.

Limitations

Only what the model allows is checked. What the code does where the model says no is not tried.
No “eventually” rules yet. It only checks rules that must hold in every state.
Only the values you pick. A bug that needs another value is missed, like the quantity-0 bug above.
Built for small models. Large models run out of time or memory sooner.