TLA+ is less a programming language and more a systems modeling language. It's like writing a mathematical proof for your system where you describe each action

TLA+ is less a programming language and more a systems modeling language. It's like writing a mathematical proof for your system where you describe each action the system takes, the invariants to describe "correctness" of the system and its state, and the TLA checker runs some kind of analysis of every possible state described by your model and that the invariants still hold true for all possible states. To me, it's like running a unit test in parallel where all possible inputs are provided concurrently. I'm not an expert on it, but I've worked with it some to verify distributed systems at a FAANG company (with the oversight of real experts)--so it does get used there!