I can’t understand any of this. It’s saying everything and nothing at the same time. Whatever TLA+ is this article makes it sound like the most tedious and academic thing ever.

* You define initial states and all possible state transitions.

* It will brute force all states.

* You can add a variety of assertions.

Four-letter acronyms or longer.

Here's my regular engineer explanation:

TLA+ is a specific kind of formal verification framework for software. The overall idea is that you can "prove" that some software works, rather than the typical "seems like it works" we aim for.

But under the covers, all formal verification schemes are (imho) best viewed as "very fancy testing". There are a few kinds of this fancy testing. TLA+ is the kind that can auto-generate all the relevant test cases for your code (there's more to it than that, but this definition works for now). So now instead of "I wrote a bunch of test cases, all that I could think of, and they pass" you have "I used TLA+ so I know I'm exercising all the possible test cases and they pass".

Here's the problem though: to achieve that trick, you have to write your code in a special language (TLA+). It isn't a tool that can be just pointed at regular production code.

So what you get to "prove" is a translation of your actual code into TLA+ code. It may be possible to auto-translate one to the other (I asked the original author if they did that, but no reply yet). Usually it's a manual process. Therefore you have "proof" but not quite as you know it, because you proved something different than what runs. But still more useful than a wet finger raised into the wind.

For this reason it's typically only used on narrow risky pieces of code (quorum voting is the canonical use case).