A tool for formally verifying Rust programs by transpiling them into definitions in the Lean theorem prover.
- Masters thesis: Simple Verification of Rust Programs via Functional Purification - thesis|presentation
- Official reference and coverage
- Blog post: A Formal Verification of Rust's Binary Search Implementation
Because electrolysis uses rustc's unstable private API, you need a nightly compiler. Because the API is highly unstable, you need a very specific nightly version, for which you should use rustup.rs. After installing rustup, you can build this project by executing
electrolysis$ rustup override add $(cat rust-nightly-version)
electrolysis$ rustup component add rust-src
electrolysis$ cargo run core
This will build the project and export all code from the core crate necessary for binary_search (see also thys/core/config.toml) into thys/core/generated.lean (this file already exists in case you just want to examine the correctness proof).