Our tool coq-of-rust enables formal verification of 🦀 Rust code, to make sure that a program has no bugs given a precise specification. We work by translating Rust programs to the general proof system 🐓 Coq.
Here, we present how we translate function bodies from Rust to Coq in an example. We also show some of the optimizations we made to reduce the size of the translation.