Comment by UltraSane

Exactly. I view a complete TLA+ specification as a kind of metalanguage that can be used with LLMs to generate code from.