Python (and most languages) and testing likely won't detect the concurrency bug in the above program, unless you get lucky. TLA+ and model checking will.

You use TLA+ to examine a spec or design without the extraneous details and do V&V on it. Then you go back to your code and you can be more confident that what you are making will work as intended. It is complementary, not a full alternative. You'll still want tests for your code.

TLA+ lets you express algorthims that solve NP complete problems concisely. In particular, you can naturally say stuff like "this emits an arbitrary member of the set that satisfies this set of equations".

Of course, you can't execute such programs efficiently. The hope is that a model checker can efficiently prove they cannot hit an assert failure (halt) or find a counterexample.

This is impossible in theory, but often tractable in practice.

You write a compiler and tests to check the Python implementation. If you were to write it in TLA+ you could use a built in solver and specify invariants to check, which are just formulas, without requiring all the boilerplate that a programming language would require in order to be able to simulate examples from the state space.

I wouldn't say it "takes" programmers doing it this way. It's just something that can be in your toolbox if it's useful to you. Sometimes there are benefits to being able to iterate quickly on simpler models before diving into code implementations. Sometimes it wouldn't be warranted. Sometimes you can find a multi-step difficult-to-replicate bug in a specification that is modeling what would actually be multiple complex components in a system that might be in totally different programming languages, and testing them all to completion wouldn't be feasible, but testing a model of them might.

> If it takes a programmer in a specific (unused) programming language to write a specification

TLA+ isn't a programming language, it's a specification language.

Programming languages are much too concrete to evaluate designs; that's why specification languages (like TLA+) exist.

You "test" a TLA+ design by running a model checker (usually TLC) that verifies the design meets the spec (i.e. a bunch of invariants which are the TLA+-equivalent of unit tests).