Well perhaps you could actually prove the correctness of coq itself. In any case it's just a matter of reliability in the traditional sense: we're going to end

Well perhaps you could actually prove the correctness of coq itself. In any case it's just a matter of reliability in the traditional sense: we're going to end with a small set of statements that will have to be verified by humans upon which we can rest everything else. Those statements will need enough people looking at them to get a level of certainty we're comfortable with. I believe the risk of a major flaw going unnoticed is astronomically low, and the good thing is this certainty propagates all the way to modern proofs if we take care to go through formal verification.