A formal proof really can’t have a specification bug. You say in the declaration what proposition you intend to prove and if you succeed in instantiating that type then you have succeeded in your proof.

The system also will only allow that proof to be used for the proposition you have declared so even if you somehow declared the wrong thing and proved it without realising, that wouldn’t affect the consistency of the system at all.