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 che

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.