Distributed systems are difficult to engineer - they are subject to subtle communication semantics, complex interleavings, and failure scenarios that cannot happen within a single system. Tools and modeling languages, such as PlusCal and TLA+, are available to help developers and architects give a high-level description of a system, then perform logic on that system, be that via user-guided formal proofs or systematic exploration via model checking. A common problem is that corresponding such models to a practical implementation, a complex and time-consuming process that can introduce bugs to an otherwise abstractly correct system, is left up to the developer.

PGo compiles PlusCal formal specifications into Go implementations. PGo is designed to reduce the developer burden of implementing a correct distributed system specification, and increases developers' confidence in the correctness of their implementations.