General, non-critical software systems. My understanding about TLA+ was that it really shines in critical software systems where the result of the system crashing would be catastrophic. The effort involved in modelling the non-critical systems I work on never seems to outweigh the effort of "write a test, fix the bug, re-deploy"
It's good for temporal errors, like ordering or concurrency. Those are often the hardest bugs to track down with inspection or testing. Model-checkers such as TLA+ can find them fast.
Formal specifications themselves have a few benefits. The first is they force you to make everything explicit that's usually a hidden assumption. From there, they might check the consistency of your system. From there, you might analyze them or generate code from the specs. Spotting hidden or ambiguous assumptions plus detecting interface errors were main benefits in industrial projects going back decades.
However, you can get a taste of the benefits by combining Design-by-Contract with contract/property/spec-based testing and runtime checks. Design-by-Contract is a lot like asserts. Should be easy to learn with more obvious value. I'll also note that tools such as Frama-C and SPARK Ada used with code proving are adding or did add the ability to turn all the specs/contracts into runtime checks. So, that's already available in open source or commercial form. And anything you can't spec, just write tests for. :)
This sort of stuff is maybe not useful in most simple systems and issues, one where "write test, fix bug, re-deploy" feels right.
But when you have tighter coupling and a lot more business rules, this stuff becomes useful.
For example, imagine that you are writing a billing system. Beyond just the code, there's a design that expects a passing of time and an ordering of operations (user signs up to the system, after a bit they will get invoiced, the amount invoiced will be right, perhaps there's pro-rating)
In models where there are a lot of moving parts and where you _don't_ really have locality of code, then this stuff becomes more useful.
If you've ever had a bug that exposes an issue not just with the code, but with the entire system and set of assumptions it's built on, it's possible that something like TLA+ could help you a lot for that system
I'm obviously biased in favor of TLA+, and think it's more useful than people think. But it could also be that another FM might be more useful to you, or that they're not useful at all in your case! Feel free to send me a ping if you want to talk more on this- my email's in the OP link.
