Do theorem provers demonstrate their own correctness?
I recommend reading Pollack's How to believe a machine-checked proof. It explains how proof assistants are designed to minimize the amount of critical code.

There are many levels of formal verification (that's the phrase you're looking for in place of "proven") of a proof assistant:


Verify that the algorithms used by the proof assistant are correct.
Verify that the implementation of (the critical core of) the proof assistant is correct.
Verify that the compiler for the language in which the proof assistant is implemented is correctly designed and implemented.
Verify that the hardware on which the proof assistant runs is correctly designed and built.
Compute the probability that a cosmic ray passes through the CPU and tricks your proof assistant every time you run it.
Estimate the likelihood that you are insane.


People put serious effort into these (well, at least the first four). For example,
steps 1 and 2 are addressed in Coq Coq Correct!, and steps 3 and 4 in the amazing award-winning CompCert project.