There is a PR for a Lean backend producing both C++ and Rust: https://github.com/leanprover/lean/pull/1090 Note, however, that this is purely focused on executing Lean code, not integrating with other C++/Rust sources.
My first thought was why Lean vs Isabelle/HOL or Coq given all they have that can be leveraged? And selectively depending on how challenging or different you want your project.
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.