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".
Formal verification is incredibly, amazingly good if you achieve it, but it's not the same as "perfect".