Formal Methods

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:

• Improvements in the Rust translation to Coq, part 1, part 2, part 3
• Monadic notation for the Rust translation
• Translation of Rust's core and alloc crates

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

• Translation of Python code to Coq
• Simulation of Python code in Coq

Alternate Rust-to-_ translators:

• Hax: Translate Rust to Coq (like above) or F*.
• Aeneas + Charon: Translate Rust's MIR to pure lambda calculus / F* / Coq / HOL / Lean. Currently has some strict limitations like no nested loops or closures. Paper: Aeneas: Rust verification by functional translation.

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.