https://github.com/p-org/P Skip to content Navigation Menu Toggle navigation Sign in * Product + GitHub Copilot Write better code with AI + Security Find and fix vulnerabilities + Actions Automate any workflow + Codespaces Instant dev environments + Issues Plan and track work + Code Review Manage code changes + Discussions Collaborate outside of code + Code Search Find more, search less Explore + All features + Documentation + GitHub Skills + Blog * Solutions By company size + Enterprises + Small and medium teams + Startups By use case + DevSecOps + DevOps + CI/CD + View all use cases By industry + Healthcare + Financial services + Manufacturing + Government + View all industries View all solutions * Resources Topics + AI + DevOps + Security + Software Development + View all Explore + Learning Pathways + White papers, Ebooks, Webinars + Customer Stories + Partners * Open Source + GitHub Sponsors Fund open source developers + The ReadME Project GitHub community articles Repositories + Topics + Trending + Collections * Enterprise + Enterprise platform AI-powered developer platform Available add-ons + Advanced Security Enterprise-grade security features + GitHub Copilot Enterprise-grade AI features + Premium Support Enterprise-grade 24/7 support * Pricing Search or jump to... Search code, repositories, users, issues, pull requests... Search [ ] Clear Search syntax tips Provide feedback We read every piece of feedback, and take your input very seriously. [ ] [ ] Include my email address so I can be contacted Cancel Submit feedback Saved searches Use saved searches to filter your results more quickly Name [ ] Query [ ] To see all available qualifiers, see our documentation. Cancel Create saved search Sign in Sign up Reseting focus You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session. You switched accounts on another tab or window. Reload to refresh your session. Dismiss alert {{ message }} p-org / P Public * Notifications You must be signed in to change notification settings * Fork 179 * Star 3k The P programming language. p-org.github.io/p/ License MIT license 3k stars 179 forks Branches Tags Activity Star Notifications You must be signed in to change notification settings * Code * Issues 11 * Pull requests 0 * Discussions * Actions * Projects 0 * Security * Insights Additional navigation options * Code * Issues * Pull requests * Discussions * Actions * Projects * Security * Insights p-org/P master BranchesTags [ ] Go to file Code Folders and files Name Name Last commit Last commit message date Latest commit History 4,170 Commits .github/workflows .github/workflows Bld Bld Docs Docs Ext Ext Icon Icon Src Src Tst Tst Tutorial Tutorial .gitattributes .gitattributes .gitignore .gitignore .gitmodules .gitmodules CODE_OF_CONDUCT.md CODE_OF_CONDUCT.md CONTRIBUTING.md CONTRIBUTING.md Directory.Build.props Directory.Build.props LICENSE.txt LICENSE.txt P.sln P.sln README.md README.md View all files Repository files navigation * README * Code of conduct * MIT license [icon] Formal Modeling and Analysis of Distributed (Event-Driven) Systems NuGet GitHub license GitHub Action (CI on Windows) GitHub Action (CI on Ubuntu) GitHub Action (CI on MacOS) Tutorials Challenge: 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! P Overview: 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 satisfy the desired correctness specifications. If you are wondering "why do formal methods at all?" or "how is AWS using P to gain confidence in correctness of their services?" , the following re:Invent 2023 talk answers this question, provides an overview of P, and its impact inside AWS: (Re:Invent 2023 Talk) Gain confidence in system correctness & resilience with Formal Methods (Finding Critical Bugs Early!!) [6874747073] Impact: P is currently being used extensively inside Amazon (AWS) for analysis of complex distributed systems. For example, Amazon S3 used P to formally reason about the core distributed protocols involved in its strong consistency launch. Teams across AWS are now using P for thinking and reasoning about their systems formally. P is also being used for programming safe robotics systems in Academia. P was first used to implement and validate the USB device driver stack that ships with Microsoft Windows 8 and Windows Phone. Experience and lessons learned: In our experience of using P inside AWS, Academia, and Microsoft. We have observed that P has helped developers in three critical ways: (1) P as a thinking tool: Writing formal specifications in P forces developers to think about their system design rigorously, and in turn helped in bridging gaps in their understanding of the system. A large fraction of the bugs can be eliminated in the process of writing specifications itself! (2) P as a bug finder: Model checking helped find corner case bugs in system design that were missed by stress and integration testing. (3) P helped boost developer velocity: After the initial overhead of creating the formal models, future updates and feature additions could be rolled out faster as these non-trivial changes are rigorously validated before implementation. Programming concurrent, distributed systems is fun but challenging, however, a pinch of programming language design with a dash of automated reasoning can go a long way in addressing the challenge and amplify the fun!. Let the fun begin! You can find most of the information about the P framework on: http:/ /p-org.github.io/P/. What is P?, Getting Started, Tutorials, Case Studies and related Research Publications. If you have any further 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. About The P programming language. p-org.github.io/P/ Topics programming-language distributed-systems state-machine robotics asynchronous systematic-testing event-driven model-checking formal-methods p formal-verification Resources Readme License MIT license Code of conduct Code of conduct Activity Custom properties Stars 3k stars Watchers 108 watching Forks 179 forks Report repository Releases 80 tags Contributors 45 * @ankushdesai * @lovettchris * @ellab123 * @alexreinking * @ejacksonMSR * @pdeligia * @aman-goel * @dijkstracula * @thisiscam * @akashlal * @exists-forall * @Eric-Le-Ge * @mchadalavada * @yzhang90 + 31 contributors Languages * C# 43.1% * OpenEdge ABL 26.5% * Java 22.3% * C 6.6% * Python 0.8% * Shell 0.3% * Other 0.4% Footer (c) 2024 GitHub, Inc. Footer navigation * Terms * Privacy * Security * Status * Docs * Contact * Manage cookies * Do not share my personal information You can't perform that action at this time.