An LLM-generated TLA+ model can be verified for certain things in a way that LLM-generated code can't. It's infamously hard to exhaustively unit-test concurrency.

Whether or not you're modeling the right things or verifying the right things, of course... that's always left as an exercise for the user. ;)

(How to prove the implementation code is guaranteed to match the spec is a trick I haven't seen generalized yet, either, too.)