Compiling efficient distributed systems from verified specifications


We compile Go-based distributed systems from specifications written in a variant of PlusCal.

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.

Additional Information

PGo implementation

People: Finn Hackett, Shayan Hosseini

arrow_back Back

Systopia lab is supported by a number of government and industrial sources, including Cisco Systems, the Communications Security Establishment Canada, Intel Research, the National Sciences and Engineering Research Council of Canada (NSERC), Network Appliance, Office of the Privacy Commissioner of Canada, and the National Science Foundation (NSF).