We continued our work on coq-of-rust, a tool to formally verify Rust programs using the proof system Coq 🐓. This tool translates Rust programs to an equivalent Coq program, which can then be verified using Coq's proof assistant. It opens the door to building mathematically proven bug-free Rust programs.
We present two main improvements we made to coq-of-rust:
- Using the THIR intermediate language of Rust to have more information during the translation to Coq.
- Bundling the type-classes representing the traits of Rust to have faster type-checking in Coq.