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.
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 — Marc Brooker and Ankush Desai, Communications of the ACM, 2025.
| 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. |
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
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
| 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 | AI-powered code generation with auto-fix and human-in-the-loop support. |
| PObserve | Validate service logs against P specifications. |
You can find most of the information about the P framework on: https://p-org.github.io/P/
What is P? | Getting Started | PeasyAI | Tutorials | Case Studies | Publications
If you have any questions, please feel free to create an issue, ask on discussions, or email us.
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 for more information.