P

Formal Modeling and Analysis of Distributed Systems 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. (Re:Invent 2023) Gain confidence in system correctness & resilience with Formal Methods 📄 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 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 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 AI-powered code generation with auto-fix and human-in-the-loop support. 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/ 🐳 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): docker run --rm -it -v "$PWD":/workspace ghcr.io/p-org/p:latest See the installation guide for details. 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.