From README:

At the heart of coq-of-rust is the translation of Rust programs to the proof system Coq 🐓. Once some Rust code is translated to Coq, it can then be verified using standard proof techniques.

Here is an example of a Rust function:

fn add_one(x: u32) -> u32 {
    x + 1
}

Running coq-of-rust, it translates in Coq to:

Definition add_one (τ : list Ty.t) (α : list Value.t) : M :=
  match τ, α with
  | [], [ x ] =>
    ltac:(M.monadic
      (let x := M.alloc (| x |) in
      BinOp.Panic.add (| M.read (| x |), Value.Integer Integer.U32 1 |)))
  | _, _ => M.impossible
  end.

Functions such as BinOp.Panic.add are part of the standard library for Rust in Coq that we provide. We can then express and verify specifications on the code in Coq.

Blog:

The same group also recently started coq-of-python, which is the same thing but for Python:

Alternate Rust-to-_ translators:

Other Rust formal verification projects:

  • Creusot: Formally verifies Rust code with annotations representing preconditions/postconditions/assertions, by translating the MIR to Why3 then solving.
  • Kani: Formally verifies Rust code with annotations, by using model checking powered by CBMC.
  • Verus: Formally verifies a Rust DSL with syntax extensions to represent preconditions/postconditions/assertions, by using the Z3 SMT solver.