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