Skip to main content

5 posts tagged with "coq-of-rust"

View All Tags

5 min read

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 atcontact@formal.land!

6 min read

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.

8 min read

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.