AI is pretty decent at writing TLA+ specs, but the specs are often bloated, and AI misses the simpler system. If you try to write TLA+ with LLMs and they produce a 500 LoC monstrosity with very abbreviated names, consider that this is not at all how TLA+ is supposed to feel. Leslie Lamport, the creator of TLA+, also recommends using a lot of comments in specs (the language is meant to be machine-checkable but is also notionally terse).

If you want to 'prompt your way' with TLA+, this is a decent one for ChatGPT. But don't expect to do wonders and find a better abstraction than you and if you run it 'agentically' with TLC in the loop, it will bloat the spec in no time:

Write the smallest TLA+ model that captures only the safety-relevant state of [the thing you're modeling]. Do not model implementation data structures unless they affect the property. Use clear names, not abbreviations. Start with: constants, variables, TypeOK, Init, and 2–4 invariants. Use copious amounts of comments at the module level (use multi-line comments) and for each key variable, action, invariant, and temporal property (use one or more single-line comments). Prefer fewer variables and coarser atomic steps unless finer interleavings are essential. Keep the spec under 100 LoC (excluding comments) unless there is a specific reason not to. After writing it, list what was intentionally abstracted away.