The safety of Coq is a consequence of the consistency or strong normalisation of the calculus of the inductive constructions. And, as you can see, this is a proof assistant which satisfies the Bruijn principle. Because it's a small trusted piece of software. As you can see the type checker is only little over 5.000 lines of code.

---