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.
-
PeasyAI — AI-powered code generation for P. Generate state machines, specifications, and test drivers from design documents. Integrates with Cursor and Claude Code via MCP with 27 tools, ensemble generation, auto-fix pipeline, and 1,200+ RAG examples.
-
PObserve — Runtime monitoring and conformance checking. Validate that your production system conforms to its formal P specifications by checking service logs against P monitors — bridging the gap between design-time verification and runtime behavior.
| Component | Description |
|---|---|
| P Language | Model distributed systems as communicating state machines. Specify safety and liveness properties. |
| PeasyAI | AI-powered code generation from design documents with auto-fix and human-in-the-loop support. |
| P-Checker | Systematically explore interleavings of messages and failures to find deep bugs. Additional backends: PEx, PVerifier. |
| PObserve | Validate service logs against P specifications in testing and production. |
Using P, developers model their system designs as communicating state machines — a mental model familiar to developers who build systems based on microservices and service-oriented architectures. Teams across AWS that build some of its flagship products — from storage (Amazon S3, EBS), to databases (Amazon DynamoDB, MemoryDB, Aurora), to compute (EC2, IoT) — have been using P to reason about the correctness of their system designs.
📄 Systems Correctness Practices at Amazon Web Services — Marc Brooker and Ankush Desai, Communications of the ACM, 2025.
P has helped developers in three critical ways:
-
P as a Thinking Tool — Writing formal specifications forces developers to think about their system design rigorously, bridging gaps in understanding. A large fraction of bugs can be eliminated in the process of writing specifications itself!
-
P as a Bug Finder — Model checking finds corner-case bugs in system design that are missed by stress and integration testing.
-
P Boosts Developer Velocity — After the initial overhead of creating formal models, future updates and feature additions can be rolled out faster as non-trivial changes are rigorously validated before implementation.
✨ Programming concurrent, distributed systems is fun but challenging, however, a pinch of programming language design with a dash of automated reasoning can go a long way in addressing the challenge and amplifying the fun! ✨
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.
