We are getting very close to be in a position of officially accepting @UncombedCoconut 's [Decider] Finite Automata Reduction decider (the method is also presented extensively here).
In a nutshell, the method gives a very efficient algorithm for finding a regular language that describes the eventuallyhalting configurations of a TM. That way, the TM can be proven to be nonhalting if the initial, all0 configuration is not part of the language. This approach is closely related to @heiner and @sligocki CTL method.
Following the requirements of [Debate & Vote] Decidersâ€™ validation process, the method is close to the finish line because:
 The decider follows the principles of our reproducibility and verifiability statement.
 It decides 99% of the currently undecided machines (it only leaves a few hundreds undecided machine out of the current 535,801).
 The decider has been reproduced independently by @TonyG (here) and by @cosmo (here).
 The method has been formally presented and proven correct here (still WIP but currently in a good readable state).
One notable feature of the method is that, it is very well suited to verification: for a given machine decided by Finite Automata Reduction, it is easy to provide a certificate with the necessary and sufficient data (mainly consisting in a specific finite automaton) which allow to conclude that the machine doesnâ€™t halt. Moreover, the task of verifying that such certificates are valid is computationally simple.
Hence, a verification format for FAR has been proposed by @TonyG and @UncombedCoconut has been proposed and several independent verifiers for FAR proofs have been built (here and here).
This brings us to the point of this topic: refinding from scratch all FAR proofs that have been found by @UncombedCoconut (and combined in this ~15Mb DVF file (DVF stands for Decider Validation File)) requires months of compute power and quite an expertise to accelerate the search algorithm in certain cases. However:

All those proofs, combined in the ~15Mb DVF file, are easy to verify: it takes roughly 5 minutes on a 8core laptop to verify all ~500k proofs using the slow (but hopefully easy to follow) Python implementation of the verifier.

Finding from scratch ~90% of those proofs only require little compute time (~10m computation using @UncombedCoconutâ€™s rust implementation).
Hence, here is what I propose, and please feel free to express your opinion on this post:
 We officially accept all machines that have a FAR certificate present in the DVF file, regardless of how hard was the proof to produce.
 We require that ~70% of the proofs of the DVF file to be refound independently. The Python independent implementation of the decider, available here, could achieve this goal using a few hours of compute time.
So, maybe put a heart reaction if you are OK with that plan and/or express your opinion in this thread