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.

## Monad for side effects in Rust

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.

## Representation of Rust methods 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.

## Current formal verification efforts 💪

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 💎.

## Latest blog posts on our formal verification effort on Tezos

Here we recall some blog articles that we have written since this summer, on the formal verification of the protocol of Tezos. For this project, we are verifying a code base of around 100,000 lines of OCaml code. We automatically convert the OCaml code to the proof system Coq using the converter coq-of-ocaml. We then apply various proof techniques to make sure that the protocol of Tezos does not contain bugs.

## Upgrade coq-of-ocaml to OCaml 4.14

In an effort to support the latest version of the protocol of Tezos we upgraded `coq-of-ocaml`

to add compatibility with OCaml 4.14. The result is available in the branch `ocaml-4.14`

. We describe here how we made this upgrade.

## Status update on the verification of Tezos

Here we give an update on our verification effort on the protocol of Tezos. We add the marks:

- ✅ for "rather done"
- 🌊 for "partially done"
- ❌ for "most is yet to do"

On the website of project, we also automatically generates pages such as Compare to follow the status of the tasks.

## Make Tezos the first formally verified cryptocurrency

Our primary goal at Formal Land 🌲 is to make Tezos the first crypto-currency with a formally verified implementation. With formal verification, thanks to mathematical methods, we can check that a program behaves as expected for all possible inputs. Formal verification goes beyond what testing can do, as testing can only handle a finite amount of cases. That is critical as cryptocurrencies hold a large amount of money (around $3B for Tezos today). The current result of our verification project is available on nomadic-labs.gitlab.io/coq-tezos-of-ocaml. Formal verification is also key to allowing Tezos to evolve constantly in a safe and backward compatible manner.

## New blog posts and Meetup talk

Recently, we added two new blog posts about the verification of the crypto-currency Tezos:

- Verify the Michelson types of Mi-Cho-Coq to compare the types defined in the Tezos code for the Michelson interpreter and in the Mi-Cho-Coq library to verify smart contracts;
- Translate the Tenderbake's code to Coq to explain how we translated the recent changes in Tezos to the Coq using coq-of-ocaml. In particular we translated the code of the new Tenderbake consensus algorithm.

We also talked at the Lambda Lille Meetup (in French) to present our work on `coq-of-ocaml`

for Tezos. A video on the Youtube channel of the Meetup should be available shortly. We thanks the organizers for hosting the talk.

## Verification of the use of data-encoding

We added a blog post about the verification of the use of data-encodings in the protocol of Tezos. Currently, we work on the verification of Tezos and publish our blog articles there. We use coq-of-ocaml to translate the OCaml code to Coq and do our verification effort.