Comment by fpvandoorn

There is no unconditional proof that CIC is sound. Thanks to Gödel, the best you can do is relative consistency proofs, something like "in ZFC with omega (i.e. infinitely) many inaccessible cardinals, you can prove that the theory of Lean is consistent". Such a relatively consistency proof can be fully formalized in Lean (and in fact, in much weaker systems than Lean).