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.
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.
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.
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.