This repository contains formal specifications of programs written in P, a language specifically intended for formal modeling and analysis of distributed systems that aims to make specification more accessible than, say, TLA+, while also aiming to alleviate combinatorial explosion of model state spaces.

For more on how to get started with P, click here.

Common/FailureInjector, Common/Timer, and Common/SharedMemory were written by contributors to the P language and are included in the tutorial tree of the language repository.