Our tool coq-of-rust is translating Rust 🦀 programs to the proof system Coq 🐓 to do formal verification on Rust programs. Even if we are able to verify realistic code, such as an ERC-20 smart contract,
coq-of-rust still has some limitations:
- fragile trait handling
- difficulties in ordering the definitions, in their order of dependencies as required by Coq
We will present how we plan to improve our tool to address these limitations.