Comment by jononor

Apparently they're getting very good: https://emschwartz.me/new-life-hack-using-llms-to-generate-c...

I try not to use them too much because I want to build the skill of using SMTs directly for now.

I've found them to be bad, for the most part. There aren't enough blog posts and examples of code out there for them to leach from.

Besides which, I would argue the process of writing proof in the language is integral to building the understanding you need to deal with the results. You'll spot bugs as you're creating the model.

I tried it many months ago and it was garbage. But this was trying smtlib directly. Maybe via the python bindings it works better?