Compiling Distributed System Models into Implementations with PGo - Hackett et al.

Distributed systems are difficult to design and implement correctly. In response, both research and industry are exploring applications of formal methods to distributed systems. For example, Amazon has reported using TLA+ and PlusCal to verify its web services. A key challenge in this domain is the missing link between the formal design of a system and its implementation. Today, this link is bridged through manual and error-prone developer effort.
In this talk we will overview Modular PlusCal (MPCal) language and the PGo1 compiler toolchain. PGo translates MPCal models to PlusCal for model checking and also compiles MPCal models to executable Go code. This allows system designers to use MPCal to model and verify their distributed system designs and then use PGo to extract working implementations of these designs.

Finn Hackett, Shayan Hosseini, Renato Costa, Matthew Do, Ruchit Palrecha, Yennis Ye, and Ivan Beschastnikh