This sort of stuff is maybe not useful in most simple systems and issues, one where "write test, fix bug, re-deploy" feels right. But when you have tighter cou

This sort of stuff is maybe not useful in most simple systems and issues, one where "write test, fix bug, re-deploy" feels right. But when you have tighter coupling and a lot more business rules, this stuff becomes useful. For example, imagine that you are writing a billing system. Beyond just the code, there's a design that expects a passing of time and an ordering of operations (user signs up to the system, after a bit they will get invoiced, the amount invoiced will be right, perhaps there's pro-rating) In models where there are a lot of moving parts and where you _don't_ really have locality of code, then this stuff becomes more useful. If you've ever had a bug that exposes an issue not just with the code, but with the entire system and set of assumptions it's built on, it's possible that something like TLA+ could help you a lot for that system