Can LLMs model real-world systems in TLA+?

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

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