I recall learning TLA+ around 2015/2016 to solve a hard bug in an OpenStack deployment. I was miffed that I was some 17 years into my career and had only learned about it then. It was so useful!<p>Since then I've used it for similar purposes as this. I try to share with my team when I do this kind of work. But often folks are highly resistant to it so I use it on my own when I'm working on a hard project.<p>Spending the time up-front to work out the design is often more cost effective in terms of time and money than iterating in production towards a, "more correct design." Getting it right first sounds hard, and it's challenging, but it's worth it for the kinds of projects where mistakes are costly, difficult to diagnose and to fix.<p>And I think more software developers are starting to realize this [0] (even if they're using different methods).<p>[0]: <a href="https://www.youtube.com/watch?v=w3WYdYyjek4&t=1333s" rel="nofollow">https://www.youtube.com/watch?v=w3WYdYyjek4&t=1333s</a><p><i>Update</i>: grammar/spelling