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).

This makes sense to me but if I continue with the "fancy testing" analogy it seems like there is no accounting for interactions beyond the system itself: it has perfect unit and integration testing but only for a myopic amount of global state.

I am curious about the limits of what one can expect this language to solve and therefore the types of programs/domains to which it is more/less suited. Why is determining quorum the canonical use case?

> But under the covers, all formal verification schemes are (imho) best viewed as "very fancy testing".

This is misleading. Testing and formal verification are vastly different.