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:
We will present how we plan to improve our tool to address these limitations.
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.
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 translate match patterns from Rust to Coq. The specificity of Rust patterns is to be able to match values either by value or reference.
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 stable coins such as the 💲USDT.
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:
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.
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 💎.