It's already in this state. See Coq-in-Coq, where Coq formalizes its own foundations. Note that this is not entirely convincing, because if Coq was in fact inco

It's already in this state. See Coq-in-Coq, where Coq formalizes its own foundations. Note that this is not entirely convincing, because if Coq was in fact inconsistent then the fact that it could prove its consistency is not surprising. But it is impossible to truly overcome this, and it certainly goes a long way to improve confidence in the system.