Is TLA+ pseudocode? It doesn't actually do anything, right? Your example with updating servers, it will never actually update the servers, right? After you try it out in TLA+, you still have to write the real code in some other language, like Bash.

If so, then isn't there still a risk of bugs in your Bash program, from typos, leaving out something from the TLA+ plan, or otherwise miscopying it?

If so, TLA+ does less than I thought. But I can see how it might be useful to work out a complex algorithm and scan it for holes.