An executable specification language based on temporal logic of actions (TLA)

I have been using Quint for some time now, both for verification of my designs via simulation and model checking and as a formalization layer for my AI agents to help eliminate any ambiguity from my requirements. I really helps to have an intermediate layer between natural language specs and code. I have been struggling to make LLMs produce code that fulfills all my requirements and even skills like wayfinder and grill-me (they are very helpful still) lack the structure that executable specifications provide in materializing requirements into a clear design.