See this[1] paper. Bugs can still occur of course, but if one restricts oneself to valid manipulations the bugs will be found in the specification and reflecte

See this[1] paper. Bugs can still occur of course, but if one restricts oneself to valid manipulations the bugs will be found in the specification and reflected in the code. It's not a magic bullet, and that's one of the reasons TLA+ was invented, it helps with complexity on the specification side. However a method like the one Dijkstra shows in the referenced paper can be used to faithfully implement the TLA+ checked specification. [1] https://www.cs.cmu.edu/~crary/819-f09/Dijkstra75.pdf https://www.cs.cmu.edu/~crary/819-f09/Dijkstra75.pdf