How valuable is TLA+ for non-concurrent applications? I've always been interested in formal verification (is TLA+ technically that?).
My understanding is that TLA+ is for concurrent applications, but with a broad definition of "concurrent." For example, it could be...
* multiple hosts messaging each other
* multiple threads in one process sharing a data structure
* multiple API calls that all use the same Postgres DB
In other words, any sort of system where different actors can step on each others' toes.
Non-determinism might be a better thing to anchor the value to. For example in a deterministic "normal" programming environment, an if/then/else statement will execute only one out of two possible code paths. You have to run the code with a complementary condition to observe the other code path.
In a non-deterministic environment like TLA+ both possible code paths are executed. You can observe state transitions in both possibilities.
In a deterministic context the combinatorics of code paths can get out of hand quickly. Non-deterministically you have one set of assertions for all code paths, or patterns of paths.
The latter is much less overhead, so it's good to use bounded models (with the TLC model checker) to become confident in the spec, then construct proofs if warranted.