p 3.1.0

<div align="center"> <img src="Icon/icon.png" width="20%"> <h2>Formal Modeling and Analysis of Distributed Systems</h2> </div>

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.

<div align="center"> <a href="https://www.youtube.com/watch?v=FdXZXnkMDxs"> <img src="https://img.youtube.com/vi/FdXZXnkMDxs/hqdefault.jpg" style="width:40%;"> </a> <br/> <em><a href="https://youtu.be/FdXZXnkMDxs?si=iFqpl16ONKZuS4C0">(Re:Invent 2023) Gain confidence in system correctness & resilience with Formal Methods</a></em> </div>

📄 Systems Correctness Practices at Amazon Web Services — Marc Brooker and Ankush Desai, Communications of the ACM, 2025.

Why Teams Choose P

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

Let the fun begin!

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.