As of February 2024, here is the current situation:
Of the 32632 remaining machines, @UncombedCoconut has undocumented code that produces easy to verify certificates for all but 34 of them. These certificates have been verified by multiple independent sources, and you can find the repository containing all 32598 certificates here. The only reason why they are not counted as official is because there is not yet formal documentation of how to reproduce these certificates - otherwise, we can safely say that they’re counted.
Of the 34 remaining machines, 31 of them can be placed into six specific categories. Five of the six categories, as well as two of the three holdouts, have deciders and/or formal proofs:
- 12 “counter balanced” machines (these have deciders in lijil’s MITMWFAR repo; the machines here correspond to the first 12 lines there, in order): 472097, 321080, 523280, 320969, 8210683, 8210684 8210685, 10818491, 8226493, 572659, 10818510, 1465912
- 2 “counter inverting” machines (these have deciders in lijil’s MITMWFAR repo; the machines here correspond lines 13 and 14 over there, in order): 12781955 (Skelet’s old proof here), 12699987
- 3 “cubic helix” machines (these have deciders in lijil’s MITMWFAR repo; the machines here correspond lines 15 thru 17 over there, in order): 4817065, 5377178, 7138511
- 5 “shift overflow counter” machines (these have all been Coq’ed by meithecatte and int-y, see here): 2204428, 11896831, 11896832, 11896833, 13134219
- 4 “bouncer” machines (these have deciders in TonyGuil’s repo): 347505, 5657318, 9914965, 9980689
- Skelet #1 (68329601) has a proof here and formalized here
- Skelet #10 (3810716) has a proof here and formalized here
This leaves the “cubic finned” category as well as Skelet #17 which have yet to be verified. For Skelet #17 I have a proof, but preferable would be for it to be formalized or automated.