Skip to content

Commit c196458

Browse files
ankushdesaiankushdesai
committed
Redesign home page with PeasyAI and PObserve highlights
Add prominent "What's New" section featuring PeasyAI and PObserve, toolchain image at the top, and framework overview grid cards. Made-with: Cursor
1 parent c117e6e commit c196458

File tree

1 file changed

+71
-17
lines changed

1 file changed

+71
-17
lines changed

‎Docs/docs/index.md‎

Lines changed: 71 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -18,37 +18,91 @@
1818

1919
---
2020

21-
!!! danger "The Challenge"
22-
Distributed systems are notoriously hard to get right. Programming these systems is challenging because of the need to reason about correctness in the presence of myriad possible interleaving of messages and failures. Unsurprisingly, it is common for service teams to uncover correctness bugs after deployment. **Formal methods can play an important role in addressing this challenge!**
21+
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.
2322

24-
!!! abstract "P Overview"
25-
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. P supports several backend analysis engines (based on automated reasoning techniques like model checking and symbolic execution) to check that the distributed system modeled in P satisfies the desired correctness specifications.
23+
![P framework toolchain overview](toolchain.jpg){ align=center }
2624

27-
??? question "Why formal methods? How is AWS using P?"
28-
The following re:Invent 2023 talk answers this question, provides an overview of P, and its impact inside AWS:
25+
---
2926

30-
<div align="center">
31-
<a href="https://www.youtube.com/watch?v=FdXZXnkMDxs">
32-
<img src="https://img.youtube.com/vi/FdXZXnkMDxs/hqdefault.jpg" style="width:40%;">
33-
</a>
34-
</div>
27+
## :material-new-box:{ .lg } What's New
3528

36-
[(Re:Invent 2023) Gain confidence in system correctness & resilience with Formal Methods](https://youtu.be/FdXZXnkMDxs?si=iFqpl16ONKZuS4C0)
29+
<div class="grid cards" markdown>
30+
31+
- :material-robot-outline:{ .lg .middle } **PeasyAI — AI-Assisted P Development**
32+
33+
---
34+
35+
Generate P state machines, specifications, and test drivers from design documents using AI. Integrates with **Cursor** and **Claude Code** via MCP with 27 tools, ensemble generation, auto-fix pipeline, and 1,200+ RAG examples.
36+
37+
[:octicons-arrow-right-24: Get started with PeasyAI](getstarted/peasyai.md)
38+
39+
- :material-monitor-eye:{ .lg .middle } **PObserve — Runtime Monitoring**
40+
41+
---
42+
43+
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, without additional instrumentation.
44+
45+
[:octicons-arrow-right-24: Learn about PObserve](advanced/pobserve/pobserve.md)
46+
47+
</div>
3748

3849
---
3950

40-
## Impact at AWS
51+
## :material-shield-check:{ .lg } The P Framework
4152

42-
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 (SOAs). 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.
53+
<div class="grid cards" markdown>
54+
55+
- :material-file-document-edit-outline:{ .lg .middle } **P Language**
56+
57+
---
4358

44-
For example, Amazon S3 used P to formally reason about the core distributed protocols involved in its strong consistency launch. P is also being used for programming safe robotics systems in Academia and was first used to implement and validate the USB device driver stack that ships with Microsoft Windows 8 and Windows Phone.
59+
Model distributed systems as communicating state machines. Specify safety and liveness properties. A programming language — not a mathematical notation.
60+
61+
- :material-robot-outline:{ .lg .middle } **PeasyAI**
62+
63+
---
64+
65+
AI-powered code generation from design documents. Generates types, machines, specs, and tests with auto-fix and human-in-the-loop support.
66+
67+
- :material-shield-check-outline:{ .lg .middle } **P-Checker**
68+
69+
---
70+
71+
Systematically explore interleavings of messages and failures to find deep bugs. Reproducible error traces for debugging. Additional backends: PEx, PVerifier.
72+
73+
- :material-monitor-eye:{ .lg .middle } **PObserve**
74+
75+
---
76+
77+
Validate service logs against P specifications in testing and production. Ensure implementation conforms to the verified design.
78+
79+
</div>
80+
81+
[:octicons-arrow-right-24: Learn more about the P framework](whatisP.md)
82+
83+
---
84+
85+
## :material-aws:{ .lg } Impact at AWS
86+
87+
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.
4588

4689
!!! abstract "Further Reading"
4790
:material-file-document: [**Systems Correctness Practices at Amazon Web Services**](https://cacm.acm.org/practice/systems-correctness-practices-at-amazon-web-services/) — _Marc Brooker and Ankush Desai_, Communications of the ACM, 2025.
4891

49-
## Experience and Lessons Learned
92+
??? question "Why formal methods? How is AWS using P?"
93+
The following re:Invent 2023 talk provides an overview of P and its impact inside AWS:
94+
95+
<div align="center">
96+
<a href="https://www.youtube.com/watch?v=FdXZXnkMDxs">
97+
<img src="https://img.youtube.com/vi/FdXZXnkMDxs/hqdefault.jpg" style="width:40%;">
98+
</a>
99+
</div>
100+
101+
[(Re:Invent 2023) Gain confidence in system correctness & resilience with Formal Methods](https://youtu.be/FdXZXnkMDxs?si=iFqpl16ONKZuS4C0)
102+
103+
---
50104

51-
In our experience of using P inside AWS, Academia, and Microsoft, we have observed that P has helped developers in three critical ways:
105+
## :material-lightbulb-on:{ .lg } Experience and Lessons Learned
52106

53107
<div class="grid cards" markdown>
54108

0 commit comments

Comments
 (0)