@shelldozer @0xabad1dea Considering the calculus of inductive constructions is consistent, Gallina is well-defined and MetaRocq works to prove the implementation of CiC within Rocq using it's own spec, which has been proven to be correct I'd say that the verification mechanism is, within the spec, correct:
https://metarocq.github.io/coqcoqcorrect