Skip to main content

6 posts tagged with "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.

5 min read

We are diversifying ourselves to apply formal verification on 3锔忊儯 new languages with Solidity, Rust, and TypeScript. In this article we describe our approach. For these three languages, we translate the code to the proof system 馃悡Coq. We generate the cleanest馃Ъ possible output to simplify the formal verification馃搻 effort that comes after.

Formal verification is a way to ensure that a program follows its specification in馃挴% of cases thanks to the use of mathematical methods. It removes far more bugs and security issues than testing, and is necessary to deliver software of the highest quality馃拵.