By a *bona fide* bug in a proof assistant I mean a software flaw which is serious enough to create a possibility of "proving" something which is actually false. This is not a purely academic problem https://cstheory.stackexchange.com/questions/37299/has-a-proof-checker-bug-ever-invalidated-a-major-proof. We mathematicians do not have a real reason to care about it for now, but I am convinced that this problem has a good potential to grow to scary proportions once a large scale program of formalization of mathematics is attempted.
Modern mathematics is more hierarchical then common software, and in a very nontrivial way. Because of this, a cleanup after fixing a bug may become rather painful.

I am curious about methods to avoid this which are based on mathematics (as opposed to some sort of management). One method I know about is verifying the code of a proof assistant using this same proof assistant. Strictly speaking, this is theoretically impossible due to the second Goedel theorem, but the way around it is to make the system stronger (for example, by adding a new axiom). There is a paper by J. Harrison about how it may be done for HOL light, J. Harrison, "Towards self-verification of HOL Light", Automated Reasoning, 2006 - Springer. More recent works in this direction are Myreen, Owens, Kumar, "Steps Towards Verified Implementations of HOL Light" , and Anand, Rahli, "Towards a Formally Verified Proof Assistant", ITP 2014: Interactive Theorem Proving.

*Question 1*. How far did it go? (All the above papers have the word ``towards'' in the title.)

*Question 2*. What can be said about formal verification of a proof assistant which may be of interest to mathematicians? (For example, are there nontrivial alternatives to, or variations of, self-verification?)

*Remark*. The question whether this or similar strategy actually makes a proof assistant perfectly bug-free (in the above sense) would be more appropriate on Computer Science SE, but I would not mind if anyone touches this topic.

thatdifferent from conventional type theory, and Coq is sufficiently flexible, that it's not a big leap to use Coq for homotopy type theory. $\endgroup$