Hey, author here. While right now TLA+ is most popular with cloud and infrastructure companies, that's more because it already has a reputation there than anything. As u/bmays mentioned, at my previous job we were using it to verify device setup, vendor integrations, and business logic. We only had ten engineers in the company, but our estimates it usually cut development time by a quarter and almost entirely eliminated post-release fires. I've also heard stories from a lot of people who've learned TLA+ from my material and, while I can't give identifying details, I can provide some high-level descriptions of what they did with it:

* A few different groups verified business ETLs with it, finding corner cases which would lose or corrupt data. Similarly, I a lot of use for deployment procedures.

* A lot of people are using it for testing optimizations: write a TLA+ spec of your system, write a spec of the optimizations, and check that they have the same behavior.

* Finding bugs in microservices. I get a _ton_ of emails about this.

* Lots of specific domain problems: trading algorithms, robotics, etc.

The main benefit of TLA+ (and formal specification in general) is that it gives you a way of both writing a precise design of your system and checking the design itself for bugs. That's something so rare in mainstream programming that many people don't even know it's possible. That's why I want to make this stuff more accessible.

Does that answer your question?