An announcement is here. A quote:
From Laurent Théry
Date: Thursday 20 September 2012, 20:24
Re: [Coqfinitgroup-commits] r4105 – trunkHi,
Just for fun
Feit Thompson statement in Coq:
Theorem Feit_Thompson (gT : finGroupType) (G : {group gT}) : odd #|G| -> solvable G.
How is it proved?
You can see only green lights there:
http://ssr2.msr-inria.inria.fr/~jenkins/current/progress.html
and the final theory graph at:
http://ssr2.msr-inria.inria.fr/~jenkins/current/index.html
How big it is:
Number of lines ~ 170 000
Number of definitions ~15 000
Number of theorems ~ 4 200
Fun ~ enormous!
— Laurent
Mathematics under the Microscope 
I find the objections stated in http://mathoverflow.net/questions/18421/how-do-they-verify-a-verifier-of-formalized-proofs rather convincing.
And it worries me that Coq developers appear to not to worry much about exploits, although I am unqualified to judge the actual risks.
http://seclists.org/fulldisclosure/2011/May/73
Re: proving _anything_ in the Coq proof assistant (in addition to code execution). “coqchk” passes too
From: Andreas Bogk
Date: Tue, 03 May 2011 14:55:47 +0200
….
Moral: plugins are part of your trusted computing base. You need to trust them
as much as you need to trust Coq. The good news here is that it requires a
malicious attacker with write access to the source code to pull off such an attack, whereas finding all genuine bugs would already improve security a lot. And defending against the attack boils down to checking for malicious plugins,
which falls into line with defending against compiler backdoors, trojaned
compile hosts etc. “Reflections on trusting trust”, et al.
By: Anonymous on November 5, 2012
at 11:10 am