A Formal Verification of Rust's Binary Search Implementation

This post is about my ongoing master’s thesis under Jeremy Avigad at Carnegie Mellon University, in which I’m trying to tackle formal verification of Rust programs in the interactive theorem prover Lean, and a first result of the project: a complete verification of the Rust stdlib’s binary search function. Putting the ‘Formal’ into ‘Formaldehyde’ Formal Verification is the act of mathematically re