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.