While people are steaming ahead on finessing the proof of the classification of finite simple groups (CFSG), we have a formal proof in Coq of one of the first major components: the Feit-Thompson odd-order theorem. Note that the proof in Coq took a team, lead by Georges Gonthier, six years. A large part of this was formalising two books that contain the required material for the odd-order theorem, and its proof.

Are there any efforts, or planned efforts, to take on more large-scale components of the proof of the CFSG?

Candidate results, taken from Wikipedia, include the Brauer–Fowler theorem (which is on par with the odd-order theorem as being foundational for the programme), the signalizer functor theorem, the Trichotomy theorem and the Classical involution theorem. Note that the team developed tools (character theory, Galois theory...) that ideally could be re-used.

Are the components developed for the odd-order theorem able to be ported for other CFSG projects? Or are they too specific?

And finally: anyone like to make a guess at how long such an effort would take? ;-)

statementand (completely omitted) proof of ATLAS sounds pretty easy to me, but of a very different flavor than formalizing the proof of CFSG (and different is good if your goal is to learn about formal math). Moreover, one should check that the formalization is usable by using it to formally prove conditional theorems. $\endgroup$ – Ben Wieland Jun 26 '15 at 17:58