True. That's why formal verification is only one of many techniques in high assurance (A1/EAL7) evaluations. The methods are all a check against each other with the minds of the designers and evaluators being the strongest check. That might seem counter-intuitive given we're doing formal verification due to people's inability to write code. Yet, people equipped properly can see mistakes in good specs or designs much better than they can do tedious work (eg low-level code) without error.
So, in high assurance, we use every tool at our disposal to counter problems and then some for redundancy. Works out fine. That said, I have a nice paper for you if you want to see how screwed up formal verification can get:
Coq's kernel isn't particularly small so bugs are to be expected. The bug exploited in "falso", however, was outside the kernel. It never threatened correctness of existing Coq proofs.
