A formal proof is only as good as what-you-are-proving maps to what-you-intended-to-prove.

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".

No you can't.

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.

This doesn't track with the real world, though.

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.