Skip to content
<open-source>
Oeiuwq Faith Blog OpenSource Porfolio

p-org/P

The P programming language.
Source code at GitHub https://p-org.github.io/P/
p-org/P.json
{
  "createdAt": "2015-06-21T06:26:36Z",
  "defaultBranch": "master",
  "description": "The P programming language.",
  "fullName": "p-org/P",
  "homepage": "https://p-org.github.io/P/",
  "language": "C#",
  "name": "P",
  "pushedAt": "2026-03-14T15:59:11Z",
  "stargazersCount": 3584,
  "topics": [
    "asynchronous",
    "distributed-systems",
    "event-driven",
    "formal-methods",
    "formal-verification",
    "model-checking",
    "p",
    "programming-language",
    "state-machine",
    "systematic-testing"
  ],
  "updatedAt": "2026-03-21T14:21:36Z",
  "url": "https://github.com/p-org/P"
}

Formal Modeling and Analysis of Distributed Systems

NuGet GitHub license GitHub Action (CI on Windows) GitHub Action (CI on Ubuntu) GitHub Action (CI on MacOS) Tutorials

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

Section titled “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 — Marc Brooker and Ankush Desai, Communications of the ACM, 2025.

Why Teams Choose P

Section titled “Why Teams Choose P”
BenefitDescription
Thinking ToolWriting specifications forces rigorous design thinking—many bugs are caught before any code runs.
Bug FinderModel checking uncovers corner-case bugs that stress testing and integration testing miss.
Faster IterationAfter initial modeling, changes can be validated quickly before implementation.

What’s New

Section titled “What’s New”

PeasyAI — AI-Powered Code Generation

Section titled “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

Section titled “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

The P Framework

Section titled “The P Framework”
ComponentDescription
P LanguageModel distributed systems as communicating state machines. Specify safety and liveness properties.
P CheckerSystematically explore message interleavings and failures to find deep bugs. Additional backends: PEx, PVerifier.
PeasyAIAI-powered code generation with auto-fix and human-in-the-loop support.
PObserveValidate service logs against P specifications.

Let the fun begin!

Section titled “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]!(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.