Formal Modeling and Analysis of Distributed Systems
[](https://www.nuget.org/packages/P/)
[](https://github.com/p-org/P/pkgs/container/p)
[](https://raw.githubusercontent.com/p-org/P/master/LICENSE.txt)
[](https://github.com/p-org/P/actions/workflows/tutorials.yml?query=branch%3Amaster)
---
P is a state machine based programming language for formally modeling and specifying complex distributed systems. P allows programmers to model their system design as a collection of communicating state machines and provides automated reasoning backends to check that the system satisfies the desired correctness specifications.
## Impact
P enables developers to model system designs as communicating state machines—a natural fit for microservices and service-oriented architectures. Teams across AWS building flagship products—from storage (S3, EBS), to databases (DynamoDB, MemoryDB, Aurora), to compute (EC2, IoT)—use P to reason about the correctness of their designs. P has helped these teams eliminate several critical bugs early in the development process.
> 📄 [**Systems Correctness Practices at Amazon Web Services**](https://cacm.acm.org/practice/systems-correctness-practices-at-amazon-web-services/) — _Marc Brooker and Ankush Desai_, Communications of the ACM, 2025.
### Why Teams Choose P
| Benefit | Description |
|---------|-------------|
| **Thinking Tool** | Writing specifications forces rigorous design thinking—many bugs are caught before any code runs. |
| **Bug Finder** | Model checking uncovers corner-case bugs that stress testing and integration testing miss. |
| **Faster Iteration** | After initial modeling, changes can be validated quickly before implementation. |
## What's New
### PeasyAI — AI-Powered Code Generation
Generate P state machines, specifications, and test drivers directly from design documents.
- Integrates with **Cursor** and **Claude Code** via MCP
- 27 specialized tools for P development
- Ensemble generation with auto-fix pipeline
- 1,200+ RAG examples for context-aware generation
👉 [Get started with PeasyAI](https://p-org.github.io/P/getstarted/peasyai/)
### PObserve — Runtime Monitoring
Validate that production systems conform to their formal P specifications.
- Check service logs against P monitors
- Bridge design-time verification with runtime behavior
- Works in both testing and production environments
👉 [Learn about PObserve](https://p-org.github.io/P/advanced/pobserve/pobserve/)
### Multi-Error Compilation (P 3.0+)
`p compile` reports ALL type errors in one pass by default, sorted by source
location. Cascade-suppression keeps root causes surfacing without downstream
noise:
```
$ 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
```
Use `--strict-errors` (or `-se`) to restore the legacy abort-on-first
behavior:
```
$ p compile --strict-errors
[Error:] [bad.p:6:4] got type: bool, expected: int
```
The new default is particularly useful with AI fix loops (PeasyAI, Cursor)
and large refactors — fix N errors per LLM round-trip instead of N
round-trips per N errors.
## The P Framework
| Component | Description |
|-----------|-------------|
| **P Language** | Model distributed systems as communicating state machines. Specify safety and liveness properties. |
| **P Checker** | Systematically explore message interleavings and failures to find deep bugs. Additional backends: PEx, PVerifier. |
| **[PeasyAI](https://p-org.github.io/P/getstarted/peasyai/)** | AI-powered code generation with auto-fix and human-in-the-loop support. |
| **[PObserve](https://p-org.github.io/P/advanced/pobserve/pobserve/)** | Validate service logs against P specifications. |
## Let the fun begin!
You can find most of the information about the P framework on: **[https://p-org.github.io/P/](https://p-org.github.io/P/)**
> 🐳 **Want to skip the setup?** Use the official Docker image, which bundles the P CLI, .NET SDK, JDK, Maven, and graphviz (available for `amd64` and `arm64`):
> ```shell
> docker run --rm -it -v "$PWD":/workspace ghcr.io/p-org/p:latest
> ```
> See the [installation guide](https://p-org.github.io/P/getstarted/install/#alternative-use-the-docker-image) for details.
[What is P?](https://p-org.github.io/P/whatisP/) | [Getting Started](https://p-org.github.io/P/getstarted/install/) | [PeasyAI](https://p-org.github.io/P/getstarted/peasyai/) | [Tutorials](https://p-org.github.io/P/tutsoutline/) | [Case Studies](https://p-org.github.io/P/casestudies/) | [Publications](https://p-org.github.io/P/publications/)
If you have any questions, please feel free to create an [issue](https://github.com/p-org/P/issues), ask on [discussions](https://github.com/p-org/P/discussions), or [email us](mailto:ankushdesai@gmail.com).
> _P has always been a collaborative project between industry and academia (since 2013). The P team welcomes contributions and suggestions from all of you! See [CONTRIBUTING](CONTRIBUTING.md) for more information._
