Comment by simplegeek

I feel LLMs are indeed getting better at writing models. But, in my experience, they struggle to come up with correct safety and liveness properties unless you closely work with them. And of these two, they struggle the most with correct liveness properties.

Also for some problems I observe that models produced by LLMs often cause state space explosion. For simpler models they can fix this when you guide them though.

I’m sure LLMs will get even better.

That said, I take slightly different approach. Lamport said “If you're thinking without writing, you only think you're thinking.” So taking that advice I always try to write the first draft with hand and once I have the final shape in place I then turn to an LLM for further exploration and experimentation if I have to.