That probably helps to reduce the occurrence of issues, but I feel you are still ultimately relying on the correctness of proof assistants like Coq. And I am sure that bugs are occasionally found in Coq!
Indeed it does happen and it's unavoidable. You have to pick your axioms from somewhere and sometimes we pick the wrong ones or we find errors in our definitions. There's no "complete" or "perfect" system.
