electrolysis

About

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

Installation

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).