Skip to main content

13 min read

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.

13 min read

In this blog post, we present our development steps to build a tool to translate Go programs to the proof system Coq.

The goal is to formally verify Go programs to make them totally bug-free. It is actually possible to make a program totally bug-free, as formal verification can cover all execution cases and kinds of properties thanks to the use of mathematical methods. This corresponds to the highest level of the Evaluation Assurance Levels used for critical applications, such as the space industry.

All the code of our work is available on GitHub at github.com/formal-land/coq-of-go-experiment.

5 min read

We present an experiment coq-of-hs that we have made on the translation of Haskell programs to the proof system Coq聽馃悡. The goal is to formally verify Haskell programs to make them totally bug-free.

Indeed, even with the use of a strict type system, there can still be bugs for properties that cannot be expressed with types. An example of such a property is the backward compatibility of an API endpoint for the new release of a web service when there has been code refactoring. Only formal verification can cover all execution cases and kinds of properties.

The code of the tool is at: github.com/formal-land/coq-of-hs-experiment (AGPL license)

6 min read

Ensuring Flawless Software in a Flawed World

In this blog post, we present what formal verification is and why this is such a valuable tool to improve the security of your applications.

4 min read

We continue our work on the coq-of-rust tool to formally verify Rust programs with the Coq proof assistant. We have upgraded the Rust version that we support, simplified the translation of the traits, and are adding better support for the standard library of Rust.

Overall, we are now able to translate about 80% of the Rust examples from the Rust by Example book into valid Coq files. This means we support a large subset of the Rust language.

7 min read

Our tool coq-of-rust enables formal verification of 馃聽Rust code to make sure that a program has no bugs. This technique checks all possible execution paths using mathematical techniques. This is important for example to ensure the security of smart contracts written in Rust language.

Our tool coq-of-rust works by translating Rust programs to the general proof system 馃悡聽Coq. Here we explain how we translatematch patterns from Rust to Coq. The specificity of Rust patterns is to be able to match values either by value or reference.

21 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 show how we formally verify an ERC-20 smart contract written in Rust for the Aleph Zero blockchain. ERC-20 smart contracts are used to create new kinds of tokens in an existing blockchain. Examples are stablecoins such as the 馃挷USDT.

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.