Docs

Overview

What P is, and how it differs from the tests you already write.

Two clients each read a shared counter, add one and write it back. Your unit tests pass because they run the calls in one fixed order, but in production both clients can read 0, and one update is lost. P finds that ordering in milliseconds, from a short model of the design, before any service code exists.

A model, a spec and your code

P is a language for writing small, runnable descriptions of a system's design. You use it to check two kinds of thing:

You, or an agent, write a model of the design. snappea check runs it thousands of times, each with a different ordering of messages, and the spec flags any run that breaks a rule. None of your service code is involved.

Is P my code?: No. A model describes your design: the components, the messages they send, and what each does when a message arrives. It's usually a few hundred lines, and it runs only inside the checker.
Does it check my code?: The checker runs the model, not your code. A spec is a rule written in P, like "stock never goes negative". The same spec checks the model at design time and, through events your tests record, your code at test time.
How does a model help?: It finds bugs that depend on timing: races, reordered or lost messages, retries and crashes. Unit tests rarely hit these bugs, and they cost the most to fix once the code is written.

How it differs from a unit test

In a unit test, you pick one scenario and its order of events. In a P test, you describe the setup, and the checker picks the order: which message arrives first and which component runs next. It runs thousands of orderings and stops at the first one that breaks a rule.

counter0

A read–

B read–

unit testA readA writeB readB write

Two clients each read the counter, then write back what they read plus one. The answer should be 2.

Simplified: each read here includes the counter's reply. The real model also lets each message wait in an inbox, so there are many more orderings.

	Unit test	P model check
Runs	your code	a model of your design
Who picks the order	you, once	the checker, thousands of times
Finds	logic bugs on the path you wrote	bugs that need an unlucky ordering
When	after the code exists	before it, and alongside it

Worked example: a lost update

Each machine is a state machine with an inbox. send puts an event in another machine's inbox, and the checker decides when it's delivered. Here the Counter serves reads and writes, and each Client reads, then writes back the value plus one:

LostUpdate.p

machine Counter {
var value: int;
start state Serving {
  on eRead do (c: Client) { send c, eValue, value; }
  on eWrite do (v: int) { value = v; }
  on eGet do (m: Main) { send m, eValue, value; }
}
}

machine Client {
start state Run {
  entry (input: (counter: Counter, owner: Main)) {
    var v: int;
    send input.counter, eRead, this;
    receive { case eValue: (x: int) { v = x; } }
    send input.counter, eWrite, v + 1;
    send input.owner, eDone;
  }
}
}

The test machine, Main, starts the Counter and two Clients. Once both Clients are done, it asserts that the counter reached 2:

assert final == 2, format("expected 2 increments, counter is {0}", final);

test tcTwoClients [main=Main]: { Main, Counter, Client };

Check it:

$ snappea check LostUpdate.p tcTwoClients
Checking generatedOutput: 1 test case
FAIL  tcTwoClients (bug found after 9 schedules, 8 workers, 0.00s)
      Assertion Failed: LostUpdate.p:68:7 expected 2 increments, counter is 1
      Replay: snappea replay PCheckerOutput/tcTwoClients/bug.schedule LostUpdate.p
1 of 1 test case failed in 0.01s, peak memory 9 MB. Output: PCheckerOutput/

The trace shows exactly how the update was lost:

counter0

A read–

B read–

final–

1/10 Main creates the Counter and two Clients. The counter starts at 0.

The fix is a design change: replace the read and write with one eIncrement event that the Counter applies itself. With that change, snappea check covers every possible ordering through automatic exhaustive exploration and finds no bug.

on eIncrement do { value = value + 1; }

Open this model in the Playground →

The same rules, checking your code

A spec observes events and asserts rules about them. This one checks an inventory service. Specs check models in the same way.

inventory.p (excerpt)

spec InventoryCorrect observes eStocked, eReserved, eReleased {
var available: int;
state Ready {
  on eReserved do (p: (order: string, units: int)) {
    available = available - p.units;
    assert available >= 0, "reservation exceeds available stock";
  }
  // ...
}
}

Your code emits the events after each change succeeds, and your ordinary tests check them:

Python

def reserve(self, sku, order, units):
    ...
    emit("eReserved", key=sku, order=order, units=units)

def test_release_makes_stock_available_again(inventory_factory):
    with check_spec("InventoryCorrect"):
        inventory = inventory_factory()
        inventory.reserve("coffee", "order-1", 3)
        inventory.release("coffee", "order-1")

There are helpers for Python, Rust, Java and Go. To check events from running services, see live observation across processes and snappea observe. The same emit calls can write production logs for snappea observe: see testing and production.

Where P fits

Design. Write or update the design doc: components, messages, failure cases.

AI agents are well suited to writing models: they can turn a design doc into machines and specs quickly, and rerun the checker after every change. Your part is to read the specs. They are the short, plain statement of what must always be true, and the part of the model worth reviewing line by line.