This post reads like an accidental advertisement for approaches like Verus [1], which couple the implementation and verification so you can't end up with a model that diverges from the actual implementation. I'm personally much more optimistic about the verus approach, but I freely admit that's my builder bias speaking.

[1] https://github.com/verus-lang/verus

I remember NVIDA sponsored a TLA+ challenge last year https://foundation.tlapl.us/challenge/index.html

Yes

Its why I built

tlaplus-process-studio.com

https://github.com/RCSnyder/tlaplus-process-studio

Then drop it into any dark factory agent harness and a PRD and you get working software at a fraction of the time

Like https://github.com/RCSnyder/lights-out-swe

Or https://github.com/nWave-ai/nWave

Orthe millions of others