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