I actually started the project in Isabelle: https://github.com/Kha/electrolysis/tree/isabelle/thys. Automation was nice, translating Rust traits not so much. You really want them to be type classes, which Isabelle only supports for the single-parametric case.

As of right now, the project would probably be easier in Coq. But I'm confident that Lean 3 will eventually feature more powerful automation (and no Ltac). It is, after all, being developed by Leonardo de Moura, one of the creators of Z3.