For TLA it's manual. For other systems, like Coq for instance, you can extract to another language. (Also important are that systems in this space are differen

For TLA it's manual. For other systems, like Coq for instance, you can extract to another language. (Also important are that systems in this space are different. What something like Coq is good for is completely different to what TLA+ is good for. Another idea in the same vein is property-based-testing. Here the concrete code is tested by invoking random test examples, so you are testing the actual code/implementation. But this also means you can't use typical tricks of model checkers where they can regard whole classes of inputs the "same" in a test).