# P: a state machine language for checking distributed system designs

> P, from p-org, lets you model a distributed protocol as communicating state machines and then have a checker explore the interleavings. It is a design-time tool, not a runtime library, and its value depends on how much you are willing to model before you write code.

**p-org/P** — The P programming language.

- Repository: https://github.com/p-org/P
- Website: https://p-org.github.io/P/
- Stars: 3,700 · Forks: 225
- Language: C#
- License: MIT
- Published: 2026-09-23 · Updated: 2026-09-23 · Language: en
- Canonical page: https://hysenlabs.com/projects/p-org-p

## The problem P is aimed at, and who feels it

Distributed systems fail in the gaps between executions. A test suite runs a handful of orderings; the bugs live in the orderings it never runs. P's premise is that you write the design down as a set of communicating state machines, state the properties you expect to hold, and let a checker enumerate the interleavings and failure injections rather than hoping a test hits them.

The README frames this as a thinking tool as much as a bug finder: writing the specification forces design decisions to be made explicit before code exists. The stated audience is teams building microservices and service-oriented architectures, and the README names AWS products (S3, EBS, DynamoDB, MemoryDB, Aurora, EC2, IoT) as places where teams used P to reason about designs. That is a claim about adoption in the README, not an independent measurement, but it tells you who the project is written for: engineers on protocols where a wrong interleaving costs data.

If your system is a single process with no concurrency, P has nothing to check. The interesting cases are message-passing designs with retries, timeouts, partial failure and reordering.

## How the P language and checker fit together

A P program is a collection of state machines. Each machine has states, an event queue, and handlers that consume events and transition. Machines communicate by sending events to each other, so the design is expressed as message flow rather than as function calls. Safety and liveness properties are specified separately from the machines, and the checker's job is to search the state space for a violation.

The framework table in the README lists the pieces: the P language itself, the P Checker (which systematically explores message interleavings and failures), and two additional backends named PEx and PVerifier. PeasyAI and PObserve sit alongside as generation and runtime-monitoring tools. The Dockerfile explains the split concretely: the compiler and PChecker are implemented in C#, while the PEx and PSym checker backends run on the JVM and the Java sources target Java 17. That is why the official image ships both a .NET SDK and a JDK. If you install the tool by hand instead of using the image, you are assembling that same pair yourself.

The practical consequence is that the checker is not a static analyzer. It executes your model, so the cost of checking scales with the state space you describe. Models that are too detailed become slow to check; models that are too coarse check quickly and prove little.

## Installing P and compiling your first file

The README points to the installation guide at p-org.github.io/P/getstarted/install/ and offers a Docker image as the way to skip setup. The image bundles the P CLI, .NET SDK, JDK, Maven and graphviz, and is published for amd64 and arm64. The command below mounts the current directory at /workspace and drops you into the toolchain, which is the shortest path to a working `p` command.

```bash
docker run --rm -it -v "$PWD":/workspace ghcr.io/p-org/p:latest
```

Inside that container, `p compile` is the entry point. The README documents a behavior change in P 3.0 and later: compilation reports all type errors in one pass by default, sorted by source location, instead of stopping at the first one. The example output in the README looks like this.

```bash
$ p compile
[Error:] [bad.p:6:4] got type: bool, expected: int

[Error:] [bad.p:8:13] could not find name 'undeclaredVar'

[Error:] [bad.p:9:16] operator '+' requires both operands to be int or both float; got int and string
```

If you want the older behavior, the README gives `--strict-errors` (short form `-se`), which aborts on the first error. The stated reason for the new default is AI fix loops and large refactors: fixing N errors per round trip instead of one. That is a reasonable argument, and it also means error output is longer, which matters if you parse it in CI.

The other installation route named in the README is NuGet: the package is `P` on nuget.org. The README does not spell out the exact `dotnet tool install` invocation, so check the installation guide for the current package id and version before scripting it.

## Where P stops being the right tool

P checks a model, not your implementation. Nothing in the toolchain reads your Go or Java service and tells you it matches the state machine you wrote. That gap is what PObserve is for: the README describes it as checking service logs against P monitors, in testing and in production. If you skip that step, a passing check says your design is sound, not that your code implements the design.

State space is the second limit. Model checking explores interleavings, and interleavings grow fast with the number of machines, message types and in-flight messages. The README does not document a bound on model size or a recommended abstraction strategy, so you should expect to iterate: start with a small number of machines and a coarse message set, and add detail only where the property you care about needs it.

The third limit is the toolchain footprint. The compiler needs a JDK because the build runs the ANTLR4 code generator, and the PEx and PSym backends need Java 17. On a machine where you cannot install a JDK, the Docker image is the practical answer, and that pulls a container runtime into your workflow. The README does not document an offline install path for the image, so plan for registry access.

## P compared with TLA+ and with plain stress testing

TLA+ is the obvious comparison: it also targets distributed protocol design and model checking. The difference in approach is what you write. TLA+ specifications are mathematical: you describe state transitions as predicates over variables and let the model checker enumerate behaviors. P makes the state machine the first-class syntax, so the model looks closer to an actor or service design, and the toolchain generates executable checkers from it. Teams that already think in state machines tend to find P's shape more direct; teams that think in invariants and set theory tend to prefer TLA+.

The other comparison is not a tool but a habit: stress testing and integration testing with fault injection. Those find real bugs, and the README's own framing puts model checking against them, saying it uncovers corner-case bugs that stress and integration testing miss. The honest reading is that they are complementary. A model check covers orderings a test will not reach; a test covers implementation details a model does not describe. If your team will only ever do one of the two, testing is the one that runs against production code.

## Maintenance, releases and the MIT licence

The repository is not archived, and its last push was on 2026-09-03. The most recent releases listed are PeasyAI v1.0.0 on 2026-03-05, v0.3.0 on 2026-03-03 and v0.2.0 on 2026-02-26. Note what those version numbers belong to: they are PeasyAI releases, the AI code generation component, not releases of the P compiler or checker. The README does not describe a separate release cadence for the core toolchain, so if you need to pin a compiler version, check the NuGet package page rather than assuming the GitHub release feed tracks it.

The project is licensed MIT, per the badge and LICENSE.txt. For most users that is the least restrictive option available and imposes no source-disclosure obligation on your models or your generated code. That is a description of the licence text, not legal advice; if your organization has rules about which licences are acceptable for tooling in a regulated pipeline, run it past whoever owns that policy.

Upgrade cost is the real maintenance question. The P 3.0 change to multi-error compilation is a behavior change in the default, and the README documents `--strict-errors` as the escape hatch. That is the pattern to expect: defaults move, flags preserve the old behavior. The README does not document a deprecation policy or a version compatibility matrix, so a CI job that pins the CLI version is safer than one that floats.

## PeasyAI and PObserve: what they change

PeasyAI generates P state machines, specifications and test drivers from design documents. The README says it integrates with Cursor and Claude Code over MCP, exposes 27 specialized tools for P development, uses ensemble generation with an auto-fix pipeline, and draws on more than 1,200 RAG examples. Those are the README's numbers. The auto-fix pipeline is the reason multi-error compilation exists: an LLM loop that sees all errors at once can fix several per round trip.

The caveat is that generated P is still P. A model that compiles is not a model that says what you meant, and a checker that finds no violation in a wrong model is worse than no check at all, because it produces confidence you have not earned. Treat generation as a way to get a first draft of a state machine, then read it.

PObserve addresses the other end: it validates that production systems conform to their formal P specifications by checking service logs against P monitors. The README says it works in testing and production environments. That is the piece that closes the model-to-code gap, and it is also the piece with the most operational surface: log formats, monitor placement and the volume of checks in production are all things the README does not detail.

## Conclusion

P is worth adopting when a protocol's failure modes are hard to reproduce in test: replication, failover, consensus, queueing. It is the wrong tool for UI work, for one-process code, and for anyone who will not maintain a model alongside the implementation. Before committing, verify that the checker backend you need is documented for your platform, that the Docker image tag you plan to pin exists for your architecture, and that your team can read the P language reference well enough to write invariants. The repository's last push was on 2026-09-03.

## FAQ

### What is the P programming language from p-org?

It is a state machine based language for formally modeling and specifying distributed systems, where a design is written as communicating state machines and a checker explores message interleavings and failures for violations of safety and liveness properties.

### What does p compile report when a P file has several type errors?

In P 3.0 and later, p compile reports all type errors in one pass by default, sorted by source location, with cascade suppression. Passing --strict-errors or -se restores the older abort-on-first-error behavior.

### How do I install P without setting up .NET and a JDK myself?

The README points to an official Docker image that bundles the P CLI, .NET SDK, JDK, Maven and graphviz, published for amd64 and arm64. Running it with the current directory mounted at /workspace gives you a working p command.

### Does P check my actual implementation code?

No. P checks the model you write. PObserve is the component the README describes for validating that production systems conform to their P specifications by checking service logs against P monitors.

### Is P free to use in a commercial product?

The repository is licensed MIT, per the license badge and LICENSE.txt. That is the licence text, not legal advice, so route it through your own policy if you have one.

## Sources

- [License: MIT](https://github.com/p-org/P/blob/master/LICENSE)
- [p-org/P on GitHub](https://github.com/p-org/P)
- [Project website](https://p-org.github.io/P/)
- [README](https://github.com/p-org/P/blob/master/README.md)
- [Releases](https://github.com/p-org/P/releases)

---

Hysen Labs editorial analysis, written from the project's own repository and release notes. Cite the canonical page: https://hysenlabs.com/projects/p-org-p