Skip to main content

What is coq-of-rust

coq-of-rust is a transpiler from the πŸ¦€Β Rust programming language to the πŸ“Β Coq proof language. It allows formal verification on Rust programs. You can download it from GitHub.

coq-of-rust generates a shallow embedding of Rust into Coq. We run the translation from the THIR level of the Rust compiler. The generated Coq code is more verbose than the source Rust as we explicit all the low-level details, such as the sequencing of effects or the implicit borrowing/dereferencing.


If you want to formally verify Rust programs, contact us atΒ!


coq-of-rust translates the Rust code:

fn balance_of(&self, owner: AccountId) -> Balance {

to the Coq code:

(* Generated by coq-of-rust *)
Definition balance_of
(self : ref ltac:(Self))
(owner : erc20.AccountId.t)
: M ltac:(erc20.Balance) :=
let* self : M.Val (ref ltac:(Self)) := M.alloc self in
let* owner : M.Val erc20.AccountId.t := M.alloc owner in
let* Ξ±0 : ref erc20.Erc20.t := self in
erc20.Erc20.t::["balance_of_impl"] Ξ±0 (borrow owner).


To formally verify a Rust project using coq-of-rust we work as follows:

  1. translate the Rust code to Coq using coq-of-rust
  2. define the memory of the program (how the values will be allocated)
  3. write simulation functions for each function of the Rust code, to give a simpler and more functional definition of the code
  4. verify that these simulations are equivalent to the source code
  5. prove properties over these simulations

As some of the work is very verbose and repetitive, such as the definition of the simulation functions, but thankfully generative AI tools such as Github Copilot are better and better at code generation.