pnueli

pnueli is an explicit-state model checker written in TypeScript. A spec is a plain TypeScript object, and the checker walks every reachable state.

pnueli walks every reachable state of a plain TypeScript spec, with symmetry, partial-order reduction and liveness. Here: a lock with a lease.

Using pnueli

The code below is in formal-methods-samples/pnueli-distributed-lock.

The problem

A lease can expire while a node is paused, and its late write overwrites newer data.

Several identical nodes share a lock with a lease. A node takes the lock, then writes to shared storage. The lease can expire while the node is paused (a long GC pause, a slow disk) between taking the lock and writing. Another node then takes the lock and writes, the first node wakes up and writes too, and the storage now holds older data on top of newer data. The usual fix is a fencing token: every lock grant carries a number that goes up, and the storage rejects a write whose token is older than one it has already accepted.

There are two questions. Safety: can the storage ever take a write older than one it already took? Liveness: does every node keep getting its writes in, or can one be shut out forever?

Install and set up

pnpm add -D @botiroff/pnueli

The example uses version 0.2.0.

Writing the spec (use AI)

Each action has a step that returns the next states, and reads and writes for partial-order reduction.

The transitions live in a plain file, lock.ts. Each function takes a state and returns the next one, or null when the step does not apply. The write step is where the bug is: the storage accepts every write, whatever its token:

// lock.ts (shortened)
export function write(s: State, i: number): State | null {
  const node = s.nodes[i];
  if (node?.phase !== 'holding' || node.token === null) {
    return null;
  }
  const accepted = {
    ...s,
    newest: Math.max(s.newest, node.token),
    stale: s.stale || node.token < s.newest,
  };
  return withNode(accepted, i, { ...node, phase: 'wrote' });
}

The node never checks its own lease before writing, because in the real world it cannot: the pause can happen right after the check. The lease expiring is its own action, so it can happen at any point between “acquires lock” and “writes”. Tokens are renumbered by rank after every step (the storage only compares them), which keeps the state space finite even though nodes take the lock again and again. So t0 is the oldest token still in use, not a fixed number.

The pnueli spec wraps these functions in actions. It takes the module as an argument, so the same spec runs on the original code and on the fix:

// lock.pnueli.ts (shortened)
export type Lock = typeof import('./lock.js');

// No next state (null) means the action is disabled here.
function step(next: State | null): State[] {
  return next === null ? [] : [next];
}

function nodeActions(i: number, n: number, lock: Lock): Action<State>[] {
  return [
    {
      name: `n${i} acquires lock`,
      process: i,
      // The fields the action touches; partial-order reduction trusts this list.
      reads: ['nodes', 'epoch'],
      writes: ['nodes', 'epoch'],
      step: (s) => step(lock.acquire(s, i)),
    },
    {
      name: `n${i} writes`,
      process: i,
      reads: ['nodes', 'newest', 'stale'],
      writes: ['nodes', 'newest', 'stale'],
      step: (s) => step(lock.write(s, i)),
    },
    // n${i} releases lock, on process i
    // lease of n${i} expires, on process n (the clock)
  ];
}

// Symmetry: the nodes are interchangeable, so sort them into one canonical order.
function sortNodes(s: State): State {
  return { ...s, nodes: [...s.nodes].sort((a, b) => stateKey(a).localeCompare(stateKey(b))) };
}

export const noStaleWrite: Invariant<State> = {
  name: 'the store never takes a write older than one it already took',
  reads: ['stale'],
  holds: (s) => !s.stale,
};

export function lockSpec(n: number, store: string, lock: Lock, symmetry: boolean): Spec<State> {
  return {
    name: `lock, ${n} nodes, store ${store}${symmetry ? ', symmetry' : ''}`,
    // One process per node, plus one for the lease clock.
    processes: n + 1,
    init: [lock.init(n)],
    actions: Array.from({ length: n }, (_, i) => nodeActions(i, n, lock)).flat(),
    invariants: [noStaleWrite],
    ...(symmetry ? { symmetry: sortNodes } : {}),
  };
}

Running it

A shortest trace in five steps: n0’s lease expires, n1 writes, n0 writes an older token over it.

// lock.pnueli.test.ts (shortened)
import * as lock from './lock.js';
import * as fixedLock from './lock.fixed.js';

// Walks every reachable state.
checkExhaustive(lockSpec(3, 'accepts any write', lock, false));
checkExhaustive(lockSpec(3, 'accepts any write', lock, true));
// Checks "eventually the goal holds" under weak fairness.
checkLiveness(lockSpec(3, 'fencing', fixedLock, true), someNodeWrites);
checkLiveness(lockSpec(2, 'fencing', fixedLock, false), n0Writes);

The output below is printed from the results by a small formatter in the test. Without fencing, three nodes:

lock, 3 nodes, store accepts any write [exhaustive]: FAILED, 75 states
  invariant "the store never takes a write older than one it already took" does not hold
    (initial)              n0 idle, n1 idle, n2 idle | store t0
    n0 acquires lock       n0 holding t1 lease, n1 idle, n2 idle | store t0
    lease of n0 expires    n0 holding t1, n1 idle, n2 idle | store t0
    n1 acquires lock       n0 holding t1, n1 holding t2 lease, n2 idle | store t0
    n1 writes              n0 holding t0, n1 wrote t1 lease, n2 idle | store t1
    n0 writes              n0 wrote t0, n1 wrote t1 lease, n2 idle | store t1 STALE
lock, 3 nodes, store accepts any write, symmetry [exhaustive]: FAILED, 18 states
  invariant "the store never takes a write older than one it already took" does not hold
    (initial)              n0 idle, n1 idle, n2 idle | store t0
    n0 acquires lock       n0 idle, n1 idle, n2 holding t1 lease | store t0
    lease of n2 expires    n0 holding t1, n1 idle, n2 idle | store t0
    n1 acquires lock       n0 holding t1, n1 idle, n2 holding t2 lease | store t0
    n2 writes              n0 holding t0, n1 idle, n2 wrote t1 lease | store t1
    n0 writes              n0 idle, n1 wrote t0, n2 wrote t1 lease | store t1 STALE

Five steps: n0 takes the lock, its lease runs out while it is paused, n1 takes the lock and writes, and n0 wakes up and writes an older token over it. The search is breadth-first, so this is a shortest trace, and it stops at the first broken invariant. With symmetry it stops after 18 states instead of 75. The trace is the same five steps, but it prints canonical states, where the nodes are sorted after every step, so the node names in the states no longer line up with the names in the actions.

Fixing the bug

The storage rejects older tokens and safety holds. The liveness check shows n0 can still be shut out forever.

The fix is one branch in the write rule: the storage rejects a write that carries an older token than the newest one it took.

Diff style

export function write(s: State, i: number): State | null {
  const node = s.nodes[i];
  if (node?.phase !== 'holding' || node.token === null) {
    return null;
  }
  const accepted = {
    ...s,
    newest: Math.max(s.newest, node.token),
    stale: s.stale || node.token < s.newest,
  };
  return withNode(accepted, i, { ...node, phase: 'wrote' });
}

export function write(s: State, i: number): State | null {
  const node = s.nodes[i];
  if (node?.phase !== 'holding' || node.token === null) {
    return null;
  }
  if (node.token < s.newest) {
    return withNode(s, i, { phase: 'idle', lease: false, token: null });
  }
  const accepted = {
    ...s,
    newest: Math.max(s.newest, node.token),
    stale: s.stale || node.token < s.newest,
  };
  return withNode(accepted, i, { ...node, phase: 'wrote' });
}

export function write(s: State, i: number): State | null {
  const node = s.nodes[i];
  if (node?.phase !== 'holding' || node.token === null) {
    return null;
  }
  if (node.token < s.newest) {
    return withNode(s, i, { phase: 'idle', lease: false, token: null });
  }
  const accepted = {
    ...s,
    newest: Math.max(s.newest, node.token),
    stale: s.stale || node.token < s.newest,
  };
  return withNode(accepted, i, { ...node, phase: 'wrote' });
}

export function write(s: State, i: number): State | null {
  const node = s.nodes[i];
  if (node?.phase !== 'holding' || node.token === null) {
    return null;
  }
  if (node.token < s.newest) {
    return withNode(s, i, { phase: 'idle', lease: false, token: null });
  }
  const accepted = {
    ...s,
    newest: Math.max(s.newest, node.token),
    stale: s.stale || node.token < s.newest,
  };
  return withNode(accepted, i, { ...node, phase: 'wrote' });
}

With the fix the invariant holds. States visited to prove it, with no reduction, with symmetry, and with symmetry plus partial-order reduction (checkReduced):

┌─────────┬───────┬──────┬──────────┬────────────────┐
│ (index) │ nodes │ none │ symmetry │ symmetryAndPor │
├─────────┼───────┼──────┼──────────┼────────────────┤
│ 0       │ 2     │ 37   │ 19       │ 19             │
│ 1       │ 3     │ 283  │ 51       │ 51             │
│ 2       │ 4     │ 2521 │ 119      │ 119            │
└─────────┴───────┴──────┴──────────┴────────────────┘

Symmetry cuts states quickly: 51 states instead of 283 at three nodes, and 119 instead of 2,521 at four. Partial-order reduction found nothing more to cut, because every action reads and writes the shared nodes array, so no two actions are independent in this model. That is the reduction being correctly conservative.

Safety is fixed. Liveness, under weak fairness, is different. “Some node gets a write in” keeps happening, so the system as a whole always makes progress:

lock, 3 nodes, store fencing, symmetry [exhaustive]: ok, 51 states

“n0 gets a write in” does not:

lock, 2 nodes, store fencing [exhaustive]: FAILED, 37 states
  the system can loop forever without ever reaching "n0 gets a write in". The cycle is fair: processes 1, 0, 2 keep moving; processes 2, 0, 1 are blocked
    (initial)              n0 idle, n1 idle | store t0
  then forever
    n0 acquires lock       n0 holding t1 lease, n1 idle | store t0
    lease of n0 expires    n0 holding t1, n1 idle | store t0
    n1 acquires lock       n0 holding t1, n1 holding t2 lease | store t0
    lease of n1 expires    n0 holding t1, n1 holding t2 | store t0
    n1 writes              n0 holding t0, n1 wrote t1 | store t1
    n0 writes              n0 idle, n1 wrote t0 | store t0
    n1 releases lock       n0 idle, n1 idle | store t0
    n1 acquires lock       n0 idle, n1 holding t1 lease | store t0
    lease of n1 expires    n0 idle, n1 holding t1 | store t0
    n0 acquires lock       n0 holding t2 lease, n1 holding t1 | store t0
    lease of n0 expires    n0 holding t2, n1 holding t1 | store t0
    n1 writes              n0 holding t1, n1 wrote t0 | store t0
    n1 releases lock       n0 holding t1, n1 idle | store t0
    n1 acquires lock       n0 holding t1, n1 holding t2 lease | store t0
    n1 writes              n0 holding t0, n1 wrote t1 lease | store t1
    n0 writes              n0 idle, n1 wrote t0 lease | store t0
    n1 releases lock       n0 idle, n1 idle | store t0

This is a lasso: a path into a loop that can repeat forever. In the first six steps of the loop n0 takes the lock, pauses past its lease, and wakes up to find that n1 has written with a newer token, so the fenced storage rejects its write. The cycle is fair, because every process either moves in it or is blocked somewhere in it, so this is not a scheduler that simply never runs n0. Fencing keeps the data safe, but it does nothing for progress: a node whose lease keeps running out can be shut out forever.

Project layout and CI

Commit the model, the spec and the test. CI runs the test like any other test. No Java, no API key.

./
├── .github/workflows/ci.yml
├── src/lock-client.ts             the real lock and storage code
└── model/
    ├── lock.ts                    the steps, as plain functions
    ├── lock.pnueli.ts             the spec: actions, rules, symmetry
    └── lock.pnueli.test.ts        runs the checks in Vitest

Everything is committed; nothing is generated. pnueli is a library with no CLI. checkExhaustive and checkLiveness return a result and do not throw, so the test must check ok:

expect(checkExhaustive(lockSpec(3, 'fencing', lock, true)).ok).toBe(true);

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

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

What fails when:

The model lets the storage take an older write: the checkExhaustive test, with the shortest trace.
The model can stop every node from writing: the checkLiveness test, with the loop.
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/lock.ts, by hand or with a coding agent. Nothing checks that the two match.
If the change adds an action or a state field, add it to the spec, with the fields it reads and writes. If that list is wrong, the check can skip some orders and miss a bug.
Run npm test, and fix the code and the model until the rules hold.
Commit the code and the model together.

Strengths

It checks every reachable state of the model. It tries every order of steps, and a failure comes back as the shortest list of steps that breaks the rule.
It checks “eventually” rules too. In the example every “never” rule passed; only the “eventually” check showed that n0 can be shut out forever, as a loop that never ends.
It skips states that are mirror copies. Treating the nodes as interchangeable cut the check from 2,521 states to 119 at four nodes.
Plain TypeScript, no Java. You write the model as state and actions and install only the npm package; unlike stateproof and tla-precheck, there is no translation step.

Limitations

It checks the model, not your code. Your real async code is not run; to check it, you need a separate testing tool.
The number of states must stay finite. A counter that only goes up makes it endless, so you renumber such values by hand in the model.
Fewer kinds of “eventually” rules. TLA+ covers more.