Formal verification for Rust 🦀 by translation to Coq 🐓

Still a work in progress!

The translation works at the level of the HIR intermediate representation of Rust.

From the root of this repository, run:

cargo install --path lib/

Then in any Rust project, to generate a Crate.v file with the Coq translation of the crate:

cargo coq-of-rust

To run the tests (regenerate the Coq files that are acting as a reference):

cargo run --bin coq-of-rust -- translate --path examples-from-rust-book

There is a bit of code taken from the Creusot project, to make the Cargo command coq-of-rust and run the translation in the same context as Cargo.