> The workflow I'm envisioning here is the plan document we're all making nowadays isn't being translated directly into code, but into a TLA+/Alloy/... model as executable docs and only then lowered into the code space while conformance is continuously monitored

I'm sure we've agreed on this before, but I agree again ;) There are dozens of us at least, dozens! There's also a recent uptick in posts with related ideas, for example this hit the front-page briefly ( https://news.ycombinator.com/item?id=46251667 ).

I was tempted to start with alloy/tla for my own experiments along these lines due to their popularity, but since the available training data is so minimal for everything in the space.. I went with something more obscure (MCMAS) just for access to "agents" as primitives in the model-checker.

> available training data is so minimal for everything in the space

Haven't tried anything other than Alloy yet, but I've got a feeling Anthropic has employed some dark arts to synthesize either Alloy models or something closely related and trained Opus on the result - e.g. GPT 5.1 commits basic syntax errors, while Opus writes models like it's just another day at the office.