Thank you for the write-down, it is very interesting!

Is there some reason why Rocq is the proof assistant of choice and not one of the others?

also.... https://www.youtube.com/watch?v=c3sOuEv0E2I

It is as simple as: the person who contributed the proofs/implementations chose Rocq.

I did some small proofs in Dafny for a few of the simpler deciders (most of which didn't end up being used).

At the time, I found Dafny's "program extraction" (i.e. transpilation to a "real" programming language) very cumbersome, and produced extremely inefficient code. I think since then, a much improved Rust target has been implemented.

Its focus around constructible objects does lend itself well to the kind of proofs needed for non-halting. Usually they involve lemmas about the 'syntax' of a TM's configuration and how it evolves over time, and the actual number-based math is relatively simple. (With the exception of Skelet #17, which involves fiddly invariants of finite sequences.)