[charcircuit]

>Of course formal methods cannot prevent or even detect wrong specifications

A wrong specification can give you a wrong or insecure result. That was my point. Formal methods aren't a sliver bullet and your system still needs to be robust to failures.

>so why not add the step and create a hybrid system that verifies the generated result?

Because the time spent writing a specification is time wasted if there ends up being no issues with the generated code.