Posted by Georgi Guninski on May 30
coq developers appear to do forensics this way:
http://article.gmane.org/gmane.science.mathematics.logic.coq.club/6228
the academic approach (detached from current implementations imho) is:
How to Believe a Machine-Checked Proof, Robert Pollack
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.72.7610&rep=rep1&type=pdf
Source: Re: OT: best practices in formal verification and security