good is doing a lot of heavy lifting here. The point of TLA+/Pluscal is to have a proof of the soundness of the design.