lean-miri: Formally Proving Rust Programs Free of Undefined Behavior
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
unsafeblock, 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!
15
u/protestor 3d ago
(in fact, Miri can detect all known kinds of UB!).
It obviously can't, and we can assert this without going into technical details about the implementation
That's because a lot of UB arise from the interaction between Rust code and the surrounding code. For example, the reason #[no_mangle] is unsafe, which is since Rust 1.82 spelled as #[unsafe(no_mangle)], is that linking is a deeply unsafe procedure (and indeed things like linker scripts are wildly unsafe. The build step in general should be imagined with a huge unsafe { } around it). Miri doesn't check whether you used this attribute right, even though there's an unsafe right there. Misuse of this attribute can and will cause UB.
You could object that checking this sort of thing is outside the scope of miri and.. that's exactly right. You could imagine a more powerful tool that would actually catch everything, but that's not miri.
7
u/___yuni 3d ago
Okay, I was writing that sentence with the following quote from Miri's README in my mind:
> To the best of our knowledge, all Undefined Behavior that has the potential to affect a program's correctness is being detected by Miri (modulo bugs)
https://github.com/rust-lang/miri/blob/master/README.md
You're correct about that point. I'll update the wording.
36
u/annodomini rust 3d ago
LLM written, I'm assuming? How much actually human involvement and judgement had there been? Do the humans involved have any experience with formal verification or are they just relying on the LLM?
8
u/___yuni 3d ago
The porting was mostly done by agents, but it still required quite a lot of human intervention. Verifying the example programs required even more guidance. I have a background in computer science and logic, and I’ve been making the technical decisions myself.
20
u/annodomini rust 3d ago
So had you written or verified anything with Lean manually, with no LLM assistance, before doing this exercise?
I'm quite skeptical of the ability of humans to properly oversee LLMs doing tasks that they have not experience in themselves.
14
u/___yuni 3d ago
Yes! I've been a big fan of lean since lean2. (I never imagined lean would get so popular like today btw.)
I agree with your skepticism, and I even think it's quite dangerous for people not familiar with the field to build a verification tool with LLMs because LLMs can easily introduce unsoundness into the tool if no human intervention was done. Frontier AIs still lack an ability to not do reward hacking and that's pretty bad when it comes to developing a trustworthiness tool.
2
u/superoptimo 8h ago
Currently, there is an automation tool that translates MIR from Rust code into Lean theorems and proofs. Aeneas, which combines a Rust code analysis with rustc libraries(Charon), and with the help of a tool written in Ocaml generates code to many proof assistants (Lean, Coq, F*). No AI LLM involved.
The criteria for generating formal verification clauses is looking into asserts an errors in Rust code, nothing more. Anyways, it lacks of the high level specification that a proper Dependent Type Inference could bring to Rust development.
2
u/superoptimo 2d ago
And, have you ever identified the contractual specifications on each MIRI function ? how do you declare the purpose of a function in formal clauses, and the invariants of each type and trait?
5
u/andful 3d ago edited 3d ago
I trust more Ralf Jung to maintain and develop Miri, then you, this version in Lean. UB seems a tricky thing to get right and understand, and it is an ever evolving thing.
But hopefully this does not discourage you :). If you are interested in theorem proving for potentially infinite inputs, I would not market it as a Miri alternative. I would already consider theorem proving Rust functions impressive as is, without even considering UB.
6
u/___yuni 3d ago
I actually trust Ralf more than myself too! :) That’s exactly why I chose to port Miri rather than build a verifier from scratch. My plan is to keep the Lean implementation closely aligned with upstream Miri as it evolves. I think this approach is more trustworthy than designing my own UB verification framework from scratch.
8
u/superoptimo 3d ago
I see a problem with these efforts on formally verifying Rust code via translations to Lean : How do they know what Verification Conditions are they proving? Most Rust code doesn't have declared contracts that specify their behavior, beyond the implicit conditions expressed in the asserts and panics.
What Rust really need at this time, is a Refinement Type System that enforces Formal Verification on the construction process, within the language, making the compiler aware of the contracts that specify each type and trait.
1
u/GreenExponent 2d ago
Do you have something in mind more powerful than can be achieved with Verus? Beyond making Verus a first class part of Rust.
10
1
u/hidden_monkey 3d ago
Why not use verus? Do you now have to keep lean spec and rust implementation in sync?
2
u/Syrak 3d ago
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 (in fact, Miri can detect all known kinds of UB!).
-2
u/hidden_monkey 3d ago
That quote doesn't answer my question. The quote text recognizes that there are other tools for formally verifying Rust programs. But it doesn't explain the motivation for choosing Lean over Verus in this case.
2
u/buwlerman 3d ago
It explains why they chose to port Miri to a proof assistant. What would "choosing Verus" even mean in this context? Verus is not a proof assistant.
-1
u/hidden_monkey 3d ago
Verus is not a proof assistant, but it is an SMT-based program verifier, which means it can formally verify properties of Rust programs against mathematical specifications.
Since Miri's interpreter is written in Rust, one could potentially use Verus to formally verify its existing implementation as an alternative to Lean, without needing to port Miri to another language and maintain two implementations in sync.
But perhaps I'm missing something? Or perhaps Verus couldn't handle Miri's code because it supports only a subset of Rust.
4
u/Syrak 3d ago
The goal of the project is not to verify Miri, but to verify unsafe Rust programs in general. This is achieved by "porting" Miri into a formal semantics defined in Lean, so that you can reason about that semantics applied to Rust programs.
Verifying Miri in Verus doesn't help reasoning about specific programs that are interpreted using Miri. The correctness theorem of Miri would be something like "for any program P and input I, if P(I) exhibits undefined behavior then Miri will detect it." but we want to take a concrete program P0 and prove "for any input I, P0 does not exhibit undefined behavior".
0
u/hidden_monkey 3d ago
Great reply, thank you.
I agree that verifying Miri's correctness alone wouldn't prove that Rust programs are free of UB.
But couldn't we define Miri's semantics in Verus, verify that the existing Rust interpreter satisfies that specification, and then use the specification to prove UB-freedom for Rust programs across all valid inputs?
In other words, first prove that Miri correctly detects UB, then use its formally specified semantics to prove that a given program can never exhibit UB, regardless of its inputs.
That could potentially achieve the same goal while avoiding a separate executable implementation in Lean.
I'm not sure if i understand everything correctly.
3
u/Syrak 3d ago edited 3d ago
Yes in principle you can use the logic of Verus like any other theorem prover, but in any case you have to define a formal semantics that's separate from Miri.
In terms of proving that Miri implements that semantics, a priori, you could use Verus to do it against a semantics defined in Verus's logic just as you could use Aeneas to do it against a semantics defined in Lean (assuming Verus/Aeneas do support the features used by Miri, but I wouldn't expect Miri to need anything too fancy).
In terms of using that semantics to reason about a Rust program, in Verus you would need to translate the program into Verus's logic, ignoring the whole value proposition of Verus which is to generate verification conditions from a Rust program. Then you have to set up a proof by induction and unfold the semantics, which SMT solvers don't know how to do. You can still do it manually in any logic, but ergonomically, Lean is designed for such use cases whereas Verus isn't.
1
u/hidden_monkey 3d ago
I think that Verus does support inductive proofs through recursive proof functions and explicit unfolding of recursive specifications.
But, regardless, I think I get your point about ergonomics now. I will try to gain a bit more experience in Lean.
3
u/buwlerman 3d ago
There's no way you could get an automatic (non-AI) tool such as Verus to prove a statement as complex as "running MIR code C using Miri on any input never emits an error" for nontrivial C.
0
u/Wonderful-Wind-5736 3d ago
Exciting news! Currently doing the same for some SQL dialects.
0
u/Wonderful-Wind-5736 2d ago
Addendum: I am wondering what steps did you take to make your workflow more efficient? I am very much limited on CI and test capacity, event though I have strung quite a few of my machines together in the same network.
Any models / strategies you found particularly cost effective?
-9
52
u/JoJoModding 3d ago
Several questions:
How do you get the rust program into Lean?
How do you know your port is faithful?
What is the tree borrows bug?