TLA+: you mean the transitions of one variable are formally proven. Whilst a plus, this is not that different from how compilers were written since the 1980s.

TLA+: you mean the transitions of one variable are formally proven. Whilst a plus, this is not that different from how compilers were written since the 1980s. Never saw any crash happen there. You should think of these systems like you think of garbage collection. They lower (sometimes eliminate) one particular kind of problem, and that's it. It does not prove the code works, doesn't OOM, doesn't segfault, doesn't dos itself, doesn't enter infinite loop, etc.