[k__]

Someone writes theorems, prove them in their head, and try to write down that proof.

Someone else reads both and tries to reason about the proof and theorem and notifies the creator of there are mismatches.

A more practical person goes and translates all that math/theory to code.

Another practical person will check implementation and theory and notify the implementor of mismatches.

TLA+ is basically an automated version of step two in this process. Someone has an idea for a theorem, writes it down in TLA+ and the system will notifyil if it makes any sense.