I’ve toyed around with parsing the TLA+ spec and generating property based test assertions from the invariants.

It doesn’t fully close the specification gap but if it could be made robust it might be a good tool.

Generating code directly from the high level specification is called, synthesis, and is still in research mode.

Projects like Synquid[0] have come a ways but are still far from being able to express even trivial programs.

[0] https://www.csail.mit.edu/research/synquid-synthesis-liquid-...