Plugging this again if you want a quick visualizer client side program to go back and forth with an ai. Granted opus 5.5 can probably 1 shot this now

https://tlaplus-process-studio.com/

https://github.com/RCSnyder/tlaplus-process-studio

Also the hard part is connecting the tla+ spec to the implementation code with traces