Human writes the requirements, contains flaw. Human or AI translate that to specifications, and eventually code.

It does not matter if the middle man is human or AI, or written in "traditional language" or "formal verification". Bugs will be there as human failed to defined a bullet proof requirements.