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".
You can claim that your spec doesn't violate some invariants in a finite number of steps, you can't claim that the spec contains all the invariants the real system must have and that it doesn't violate them in number of steps + 1.
If you are writing software, it is almost always trying to accomplish a goal outside of itself. It is trying to solve a problem for someone, and how that problem can or should be solved is rarely perfectly clear.
The spec is supposed to map to a real world problem, and there is never going to be a way to formalize that mapping.
I do not make the claim my spec has no bugs.