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.
If you need to formally verify your Rust codebase to improve the security of your application, email us at email@example.com!