I wrote an essay[0] about a non-trivial example I did at my company. We had to work with several finicky APIs and the TLA+ spec caught several critical bugs with it. Plus, it's purely a business logic system, so it's pretty concrete.

If you're interested in learning more, I also wrote a beginner's guide[1] to the language, which contains concrete examples and exercises.

[0] https://medium.com/espark-engineering-blog/formal-methods-in...

[1] https://learntla.com/introduction/