alt Hacker NewsThere are excellent probabilistic extensions to temporal logic out there that are very useful to uncover subtle performance bugs in protocol specifications, see e.g. what PRISM [1] and Storm [2] implement. That is not within the scope of TLA+.
Formal methods are really broad, ranging from lightweight type systems to theorem proving. Some techniques are fantastic for one type of problem but fail at others. This is quite natural, the same thing happens with different programming paradigms.
For example, what is adequate for a hard real-time system (timed automata) is useless for a typical CRUD application.
I really do wish that PRISM can one day add some quality of life features like "strings" and "functions"
(Then again, AIUI it's basically a thin wrapper over stochastic matrices, so maybe that's asking too much...)