Skip to content
SpecCraft SpecCraft

libpetri

libpetri replaces the async code that manages locks, pool slots and permits and waits for earlier results: async-mutex, p-limit, Promise.all and the code around them. You write the same steps, but each step declares what it takes and what it returns, and the library runs them (the wiring is declarative, the step bodies stay plain async functions).

In return you get one thing that normal code cannot give: a test that proves properties of the steps for every possible order they can run in. Among them: the steps never hang waiting for each other, a pool never gives out more slots than it has, two steps never hold the same thing at once, and a state you name is never reached.

The downside: you rewrite working code with new constructs, and the price is about four times more code. The upside: the model and the code are one thing, in one place. What the check proves is what runs.

TLA+, Quint, pnueli and stifinder check the same kind of program, but on a model that you write and keep matching the code yourself.

Case studies

Section titled “Case studies”

Two accounts, one lock per account, and a transfer that locks the sender first, then the receiver:

transfer.ts
import { Mutex } from 'async-mutex';


export const locks = { alice: new Mutex(), bob: new Mutex() };


export async function transfer(from: 'alice' | 'bob', to: 'alice' | 'bob') {
  await locks[from].runExclusive(() =>
    locks[to].runExclusive(() => {
      // move the money
    }),
  );
}

Two transfers start at the same time, Alice to Bob and Bob to Alice. The first one holds Alice and waits for Bob. The second one holds Bob and waits for Alice. Both wait forever, and every next transfer waits behind them. A test that starts both at once shows it:

transfer.hang.test.ts
it('two transfers at once both finish', async () => {
  await Promise.all([transfer('alice', 'bob'), transfer('bob', 'alice')]);
}, 1000);
 × two transfers at once both finish 1005ms
Error: Test timed out in 1000ms.

Tests rarely catch this, the one-line fix (lock in a fixed order) works only while the code is this small, and with locks, pool slots and permits used together in ten places by five people it stops working.

In libpetri

Section titled “In libpetri”

This is what you write instead. The step body is still an async function; the lines around it say what the step takes and what it returns.

net.fixed.ts
import { PetriNet, Transition, and, one, outPlace, place } from 'libpetri';


export const alice = place<string>('alice');
export const bob = place<string>('bob');
export const done = place<string>('done');


function transfer(from: typeof alice, to: typeof alice) {
  const waiting = place<string>(`${from.name} to ${to.name}`);


  // The fix: one step takes both locks at once, or waits for both.
  const lockBothAndMove = Transition.builder(`${from.name} to ${to.name}: lock both, move`)
    .inputs(one(waiting), one(from), one(to))
    .outputs(and(outPlace(from), outPlace(to), outPlace(done)))
    .action(async (ctx) => {
      // move the money, then free both locks
      ctx.output(from, ctx.input(from));
      ctx.output(to, ctx.input(to));
      ctx.output(done, ctx.input(waiting));
    })
    .build();


  return { waiting, steps: [lockBothAndMove] };
}


export const aliceToBob = transfer(alice, bob);
export const bobToAlice = transfer(bob, alice);


export const net = PetriNet.builder('transfers')
  .transitions(...aliceToBob.steps, ...bobToAlice.steps)
  .build();

The check is a normal vitest test:

transfer.test.ts
const result = await SmtVerifier.forNet(net)
  .initialMarking((b) => b.tokens(aliceToBob.waiting, 1).tokens(bobToAlice.waiting, 1).tokens(alice, 1).tokens(bob, 1))
  .property(deadlockFree())
  .sinkPlaces(alice, bob, done)
  .verify();

For this net the check returns “proven”. Written as two steps like the plain code, it returns the two steps to the hang. Both nets and the test are in formal-methods-samples/libpetri-transfer.

Conclusion

Section titled “Conclusion”

How libpetri compares with the larger, well-known tools for the same job: it is a niche tool, and the others are the better choice, for several reasons.

  1. A separate model is not only a cost: it helps you think, and writing it is where you find the design mistakes. In the model you are free to use any data types you want and to leave out what does not matter. And the code stays free too: you write it with the tools your team already knows. A model can check any rule. libpetri cannot: its net is runtime code.
  2. TLA+ and Quint are far more widespread, more useful as modeling tools, and far more production ready.
  3. TLA+ covers far more: any system as state and next state, protocols, agreement between nodes, and rules about what must eventually happen. There is nothing libpetri can check that TLA+ cannot; every Petri net can be written in TLA+ and checked by TLC.

Comparison of TLA+ and Petri nets:

Both can handle:

  • Two transfers that each hold one account and wait for the other.
  • A connection pool that must never give out more connections than it has.
  • A job that must never run twice at the same time.
  • A report that waits for several fetches and must not start before all of them are done.
  • A worker pool with a fixed number of permits, never more running at once.

Only TLA+ can handle:

  • A rule about a value: a balance never goes negative, a discount never exceeds the price.
  • A fencing token: the store rejects a write whose number is older than one it already took.
  • A late reply from a retry that overwrites newer data.
  • A crash in the middle of a step, and what the restart sees.
  • “Every request eventually gets an answer”, not only “nothing bad happens”.

For AI agents: the author uses it for that, it runs Otto’s commerce assistant, and the check covers more of an agent loop than the case study shows. Timeouts and retries of LLM calls, branching on what the model said, and waiting for a person are all paths the check explores, as things that may or may not happen, the same way a TLA+ model treats them. Neither knows how long anything takes, unless you add a clock to the TLA+ model. One thing a TLA+ model can cover and libpetri’s check cannot is a crash and restart in the middle of a run.

Two real systems on this site, the document workflow and the SQS clone, show the same thing. In both, the rules that matter are about values: which of two results is newer, how many times a message was received against a limit that can change. libpetri’s check does not see values. Both also have rules about what must eventually happen, which libpetri does not have. For both, TLA+ or Quint is the right tool. libpetri is not.

Section titled “Links”

Last updated: