I've written formal proofs with bugs more than once. Reality is much messier than you can encode into any proof and there will ultimately be a boundary where the real systems you're trying to build can still have bugs.

Formal verification is incredibly, amazingly good if you achieve it, but it's not the same as "perfect".