In this article we show how we re-build the type and naming information of 🦀 Rust code in  Rocq/Coq, the formal verification system we use. A challenge is to be able to represent arbitrary Rust programs, including the standard library of Rust and the whole of Revm, a virtual machine to run EVM programs.
