This article notwithstanding, I don't think the right mental framework to approach TLA+ is to think of it as a way to verify your code. I view TLA+ as a formal

This article notwithstanding, I don't think the right mental framework to approach TLA+ is to think of it as a way to verify your code. I view TLA+ as a formal design language. It is there to verify and explore the consequences of architectural and design decisions. It is also there to present a formal design document that engineers can refer to as a common artifact when discussing various design decisions. Now architecture and design is a very vague domain. It could be anything from specific algorithms all the way up to entire distributed systems (and indeed TLA+ can be used for any of those), but the point is that it is a separate entity from code. I also think in the current formal methods environment this is where TLA+ can make the most impact. It is a far less risky business proposition to use TLA+ to record design decisions where the maturity of its toolchain has minimal impact on your actual codebase vs using a formal methods toolchain that directly affects the code you write, where the maturity of that toolchain is an extremely important business decision.