Generating GO from pluscal specs

PGo is a source to source compiler that translates Modular PlusCal specifications (which use a superset of PlusCal) into Go programs.

Watch the talk to the TLA+ 2019 conf:

You can also read the related paper: Compiling Distributed System Models with PGo