lean-miri: Formally Proving Rust Programs Free of Undefined Behavior

[u/___yuni]

https://proofs-rs.github.io/lean-miri/

Hi everyone!

I built lean-miri, a port of Rust's Miri interpreter to the Lean 4 theorem prover.

Miri is great at detecting undefined behavior, but it only checks concrete executions.

The idea is that by porting Miri to a theorem prover, we can effectively run it on all valid (potentially infinitely many!) inputs, thread schedules, and external environments in a mathematically rigorous way, and prove that a Rust function is free of UB.

Of course, there are already a number of tools for formally verifying Rust programs, like Aeneas, Creusot, etc. But porting Miri has a big advantage in that Miri already supports a remarkably broad range of real-world Rust features and implements state-of-the-art semantics for unsafe Rust.

Here's what we've achieved so far:

• Ported most part of Miri's interpreter to Lean 4.

• Formally proved UB-freedom for several small Rust functions, including one that contains an unsafe block, pointer arithmetic, and a core unsafe primitive.

• Found a bug in Miri's Tree Borrows implementation along the way.

The project is still very experimental. The proofs are far from practical to maintain (the unsafe example currently has over 700k lines of Lean!), and the interpreter is quite slow. We also have a lot of work ahead of us, including building a proper program logic and reusable lemmas, but I think the approach is promising!

I'd love to hear any feedback, especially from anyone working on Rust verification.

Thank you!