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.
[1] https://www.hillelwayne.com/post/modeling-deployments/
[2] https://medium.com/espark-engineering-blog/formal-methods-in...