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 wit

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-practice-8f20d72bce4f#.u3grkd2i3 https://medium.com/espark-engineering-blog/formal-methods-in... [1] https://learntla.com/introduction/ https://learntla.com/introduction/