5 posts tagged with "coq-of-rust"

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.

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.

In our project coq-of-rust we translate programs written in Rust to equivalent programs in the language of the proof system Coq 🐓, which will later allow us to formally verify them. Both Coq and Rust have many unique features, and there are many differences between them, so in the process of translation we need to treat the case of each language construction separately. In this post, we discuss how we translate the most complicated one: traits.

To formally verify Rust programs, we are building coq-of-rust, a translator from Rust 🦀 code to the proof system Coq 🐓. We generate Coq code that is as similar as possible to the original Rust code, so that the user can easily understand the generated code and write proofs about it. In this blog post, we explain how we are representing side effects in Coq.

With our project coq-of-rust we aim to translate high-level Rust code to similar-looking Coq code, to formally verify Rust programs. One of the important constructs in the Rust language is the method syntax. In this post, we present our technique to translate Rust methods using type-classes in Coq.