Isn’t the point of TLA+ is to model aspects of design at such high level that no deterministic generation is practical as a rule. The TLA+ models may be useful for LLMs (help find real bugs).