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.
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).