I've used it a few times. It was the most useful either to "prove" the conditions for a bug[1], or to gain confidence that an algorithm I had worked on was safe

I've used it a few times. It was the most useful either to "prove" the conditions for a bug[1], or to gain confidence that an algorithm I had worked on was safe under tricky conditions involving concurrency. The main downside of TLA+/PlusCal is that it's so different from programming languages that very few engineers are familiar with it. Even PlusCal which is supposed to provide a Pascal-like syntax that gets translated to TLA+ can be tricky to use and has a few pitfalls that can be frustrating for beginners. The tooling is improving, but some design choices are really not ideal. For example, you write PlusCal in a `.tla` file inside a comment block(!) and when you transpile it to TLA+ the generated code is written after your comment, in the same file[2]. This is just one of a number of baffling decisions that create a ton of friction when using these tools. Others on this page have mentioned issues with scope, this is certainly something I've had to fight with. [1] The bug I wrote a model for was CASSANDRA-8287, "Row Level Isolation is violated by read repair": https://issues.apache.org/jira/browse/CASSANDRA-8287 https://issues.apache.org/jira/browse/CASSANDRA-8287. The error trace describes a clear scenario under which this would happen. [2] See this very simple model for an example of how PlusCal is written in a comment block followed by the TLA+ code that's generated from it: https://gist.github.com/nicolasff/bcc92627485c3d4d9e0c25eeea73b655 https://gist.github.com/nicolasff/bcc92627485c3d4d9e0c25eeea...