I do often employ the simple whiteboard methods described, but I've never found the energy to learn and use stuff like TLA+. What fields do people find them useful in?
I've used Alloy for similar things, but only after the fact not during the investigation and as a way to learn Alloy.
I'd use them both again (TLA+ especially) if I could convince people it was worth the time, but it can be difficult to get the time to spend on it at work while also meeting other work obligations.
I've used TLA+ for some personal projects involving concurrent and distributed systems (toys, nothing notable just playing). I used TLA+ to demonstrate that my design worked as I intended, and then started writing code based on the model.
It's more geared towards the static elements of the system, and writing a spec feels quite like writing a relational database schema -- mostly because they're both expressions of relationships.
It seems like a pretty natural path to write a spec in alloy before building out some crud interface.
I think there's a huge tooling gap though. Alloy, TLA+ and friends all seem to be very jvm/UI centric, really targeting a user who is working in the editors the language ships with.
I'd really love to see more tooling to run model checkers in a CI pipeline, or generate stubs and test cases for various languages. If that were in place, I think there would be more stickiness to formal methods.
I've started writing a Go parser for alloy, in part to learn it better, in part because I know go and want to write some tooling that I think go would be a good implementation language for. I don't know if anything will come of it, but at least having a parser would allow for things like a formatter or code generator. If I were feeling ambitious, I might try to implement a model checker.
Helpful to escape the alloy UI:
I looked into what it would take to tackle it from the source code, There were some barriers, like the jars not really being published to maven, but the biggest just being the time & energy investment to pick up java again.
I'll definitely be looking into this project and seeing if there's anything I can contribute back.
I came across this when researching/studying Formal Methods but have not yet really sat down and tried it out.
Where you can use these methods - think of the part of your program's behavior you can describe with the article's "whiteboard" methods mentioned in the post above - truth tables, decision tables (! TIL), state machines/statecharts. If you can formulate it that way, not only is it easier to reason about and to test, but if you can also work out what would make it correct, you can run it through an automated checker.