A TLA+ spec defines both a model and properties (global invariants). How do you know that the properties the LLM specifies are the ones you care about?
My question is concerned with improving quality of AI implementations. Its plainly true, uninteresting, and beside the point to observe that AI cannot read minds.