There are really two separate questions that you seem to be conflating here.
The first is how to state the CFSG in a way that could be mechanically formalized. The second is how to state the CFSG that adequately reflects how human mathematicians think about it.
For the former question, one straightforward possibility for the sporadic groups, since we know their orders, is simply to state something like, "There exists a unique simple group, not in one of the aforementioned families, of each of the following orders: 7920, 95040," etc. This is the barest possible statement that could count as a classification theorem, and for a computer, it provides (in principle) enough information to reconstruct the groups in question.
For the second question, though, there's no sharp boundary demarcating where the classification theorem ends and the detailed study of the properties of the sporadic groups begins. There's also no canonical way of describing a particular group of interest in a way that satisfies a human that he or she now "knows what the group is." But there's nothing unique about group theory here. Any sufficiently large and complicated mathematical object is going to suffer from this problem. There will be some bare-minimum way of referring to it that in principle picks it out from the amorphous universe of all mathematical objects but that fails to answer basic questions about it. There will be a continuum of theorems that answer other basic questions, shading off into questions that we can't answer. It is a matter of opinion how many questions we have to be able to answer before we can claim to have "adequately described" the object.
Here is an answer from my point of view, immersed as I am -- Geoff
is right -- in the second generation project. First, a few general
comments. Our overriding purpose has been to expound a coherent proof
of CFSG that is supported completely by what we call ``Background
Results,'' an explicit and restricted list of published books and
papers, plus the assertion that every one of the $26$ sporadic groups
is determined up to isomorphism, as a finite simple group, by its
so-called centralizer-of-involution pattern. This list has changed
over the years. In our first volume it is explicitly listed as we
conceived it at the time (1990's). Further additions, mostly of
post-first-generation publications, are noted as they have been
adopted in subsequent volumes. (Some of these additions are
characterizations of some sporadic groups--for example, the Monster
and Baby Monster--by weaker data than centralizer-of-involution
pattern, so that they supplant the earlier Background Results
characterizing those groups.) The biggest additions, by far, are
Aschbacher and Smith's monumental books on the quasi-thin problem,
since we were hardly going to do it as well ourselves, let alone
better. Whatever errors may be in the second-generation proof,
therefore, are either in the Background Results or in our series.
Naturally, we have taken ideas and arguments from many papers and
books outside the Background Results in formulating our
proof. Occasionally in the course of understanding these results, or
adapting them for our purposes, we have uncovered gaps. None of these
is at all comparable in scope (by orders of magnitude) to the
well-known quasi-thin gap that Aschbacher and Smith bridged; in that
sense, they could be called ``minor.'' To deal with these gaps, when
they threatened our proof, we have either found alternative arguments
ourselves, or asked the authors for help. In every case, so far, the
gap has been closed in one of these two ways. However, and
unfortunately for the purposes of answering your question, we have not
kept a log of these incidents. Nor have we by any means intended to
examine every paper needed in the first-generation proof this way. We
are guided just by what we need in the second generation.
Here is an example of a minor gap that came to our attention in the
preparation of volume $9$. We needed a certain characterization of the
$7$- and $8$-dimensional orthogonal groups over the field of $3$
elements. We were guided by an important paper by Aschbacher that had
appeared relatively late and without much fanfare in the first
generation. There was an apparent gap -- very technical -- in the
paper, and Professor Aschbacher promptly supplied us with a
correction.
Another example that I know well, from before the CFSG, came in $1972$
in my paper pointing to the possible existence of the sporadic group
$Ly$. I asserted that if such a group existed, then every nonidentity
element of order a power of $5$ actually would have order
$5$. Koichiro Harada wrote me shortly thereafter that on the contrary,
there would be elements of order $25$. He was
right; I had miscalculated. Luckily, the miscalculation did not
affect the rest of the paper.
Best Answer
There has been a lot of work done on various generalizations of the concept of the building, to apply them to sporadic groups. These generalizations are variously known as diagram geometries, chamber systems, etc. Names like G.Stroth, S.Smith, M.Ronan, A. Delgado, D. Goldschmidt, B. Stellmacher, etc. spring to mind. There is an "elementary" book on diagram geometries by A.Pasini (a review of the latter is here.) There is a series of books by A.A.Ivanov (some of them are jointly with S.Shpectorov) developing a theory of this sort to deal with a majority of sporadics.
Indeed, one needs a weakening of the classical buildings to cover sporadics. Instead of starting from a weak BN-pair, one can weaken Tits' axioms from his "Local approach to buildings" to develop a theory dealing with sporadics. E.g. Witt designs for Mathieu groups (already from 1938) are extensions (in certain well-defined way) of the affine plane of order 3 and of the projective plane of order 4. Similar things can be done with $HS$, $Suz$, Fischer's sporadic groups, $He$, $McL$, $Co_3$, $Co_2$, and $BM$. (E.g. --- cannot resist citing myself here: the 3-transposition graph for $Fi_{22}$ can be characterized as the extension of the polar space for $U_6(2)$.) This appears to work when the underlying combinatorics is not too complicated (and the corresponding permutation representation has low rank).
Regarding the $BN$-pairs approach, I must say I don't recall details, having done very little work on these things in past 15 years. In a nutshell, one cannot hope for "real" apartments, etc., so one instead looks at amalgams of parabolic subgroups. Instead of a definition, let me giev you a toy example, $GL_4(2)$ and its Borel subgroup $B$ (taken to be the upper-traingular matrices, say). Then you have "minimal parabolics" $P_i$, i.e. subgroups generated by $B$ and $e_{i+1,i}$, for $i=1,2,3$ (here $e_{ij}$ denotes the matrix with 1 at position $ij$ and on the main diagonals, and 0s elsewhere). Then, you get maximal parabolics, $P_{ij}$, generated by $P_i\cup P_j$. This is what is called a rank 3 amalgam (as you have 3 minimal parabolics).
Your geometry then consists of cosets of $B$, $P_i$'s, $P_{ij}$'s in the whole group and in each other. The amalgam is now the set-theoretic union of $B$, $P_i$'s, $P_{ij}$'s, and you can study its universal completion, i.e. the biggest group where is can be embedded into. By tweaking the groups which can arise as $B$, $P_i$'s, $P_{ij}$'s, one covers more cases than buildings, and tries to stay away from infinite universal completions for ranks at least 3.
PS. IMHO, Aschbacher sometimes tends to ignore prior work, re-inventing the wheel in different terminology.