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.
> And even at the end, when asked what he would like to do, he said: "I would like to learn something."
Don't have an exact word to describe how I feel after reading above. Find it beautiful that such an accomplished person wanted to learn something even towards the end of his life.
Email: [email protected]
Blog: https://wyounas.github.io