Rust and Lean

Motivation+

The charter says checkable over short: a few more words are a good trade when they let the compiler prove something. Types and capabilities prove a lot, but not that sort sorts or that an index is in bounds. Proofs do.+

Proofs used to be the expensive part. Language models change that. They write tactic proofs well, and Lean tells them exactly what is left to prove, so they can try, read the goal and try again. Writing a proof is becoming as cheap as writing a test, and a proof covers every input.+

Today, proving things about Rust means a separate tool: a fork of the compiler, a translator run by hand, a different spec language, proofs in another repository. The proof drifts from the code, and almost nobody runs it.¹²³+

ra-jit owns the compiler. It already lowers every function to MIR and compiles it one function at a time. It can translate each function to Lean at the same point, keep the result in the same cache, and check the proof in the same edit loop as the type check.+

Design sketch+

Specs are Rust. requires and ensures clauses go after the signature. A spec fn is ordinary Rust that may only be used in specs: it is never compiled to machine code, so it may use unbounded integers and quantifiers. Syntax is illustrative; see the open issues.¹+

Each clause becomes a Lean theorem about the function's Lean definition. ra-jit first tries a fixed list of tactics: omega for integer arithmetic, bv_decide for bit operations, simp and grind for the rest. Most obligations in ordinary code end there, and the author writes nothing.+

fn max(a: u32, b: u32) -> u32
    ensures result >= a, result >= b, result == a || result == b
{
    if a >= b { a } else { b }
}
// ra-jit generates three theorems; omega proves each one.

When the tactics fail, the function carries a proof: a proof by lean { ... } block after its body, in the same .rs file. Inside it is plain Lean, with the obligation as the goal. The proof moves with the code, is reviewed in the same diff, and fails the build when the code changes under it.+

spec fn sorted(v: &[i32]) -> bool {
  Silent
    forall |i: usize, j: usize| i < j && j < v.len() ==> v[i] <= v[j]
}

fn merge(a: &[i32], b: &[i32]) -> Vec<i32>
    requires sorted(a), sorted(b)
    ensures sorted(&result), result.len() == a.len() + b.len()
{
    let (mut i, mut j, mut out) = (0, 0, Vec::with_capacity(a.len() + b.len()));
    while i < a.len() || j < b.len()
        invariant sorted(&out), out.len() == i + j,
            forall |k: usize| k < out.len() ==> (i < a.len() ==> out[k] <= a[i])
                                            && (j < b.len() ==> out[k] <= b[j])
    {
        if j == b.len() || (i < a.len() && a[i] <= b[j]) { out.push(a[i]); i += 1; }
        else { out.push(b[j]); j += 1; }
    }
    out
}
proof by lean {
  -- the goal: the loop invariant holds after each push
  intro i j out hinv hcond
  unfold sorted at *
  split <;> grind [List.getElem_append]
}

Import both ways+

Specs can name existing Lean definitions and theorems. use lean::... brings a Lean name into scope for specs only, so a spec can say "sorted" the way Mathlib says it and a proof can use every lemma Mathlib already has about it.⁴+

use lean::List::SortedLE;   // Mathlib.Data.List.Sort
use lean::List::Perm;       // Lean core

pub fn sort(v: &mut Vec<i32>)
    ensures SortedLE(view(v)), Perm(view(v), view(old(v)))
{
    // ...
}

The other way, every Rust function appears in Lean as a definition, under its crate and module path. A Lean proof can unfold it, rewrite with it and prove lemmas about it, and other proofs can use those lemmas. max from the first example becomes this:+

def max (a b : U32) : Result U32 :=
if a >= b then ok a else ok b

Optionally, Lean code compiled to C could be called from Rust at run time, through a capability (RFC 0001), so a verified Lean decision procedure could run inside a Rust program. This is an open question, below.⁵+

MIR to Lean, one function at a time+

The translation follows Aeneas. Safe Rust's ownership rules make it possible to translate without a model of the heap: a shared borrow becomes the value, and a mutation becomes a functional update. A &mut argument becomes a value passed in plus a backward function that returns its new value to the caller. Loops become recursive functions. A panic becomes Result.fail.²⁶+

What MIR means is defined once, in Lean, starting from MiniRust, Ralf Jung's precise specification of a Rust core close to MIR. The translation for each kind of MIR statement is then checked against that model, so the Lean definition of a function is known to mean what its MIR means. Without the model, the translation would be one more thing to trust.⁷+

Obligations the compiler adds+

Some theorems are generated without a spec:+

• No panics where none are allowed. A function that says it cannot panic gets an obligation at each arithmetic operation that can overflow and each index that can be out of bounds.+

  No comments yet.

  Comments are not set up yet.

• Loop invariants. An invariant clause holds on entry and is preserved by each iteration.+

  No comments yet.

  Comments are not set up yet.

• Effect claims from RFC 0001. A function with no Alloc gets a theorem that no path reaches the allocator, which the translation can state because calls to it are explicit in MIR.+

  No comments yet.

  Comments are not set up yet.

The proof cache+

A proof is cached under the hash of the function's MIR plus the specs of the functions it calls, not their bodies. Changing a callee's body without changing its spec does not recheck its callers. This is the same unit as ra-jit's function cache, and it uses the same store.⁸+

Lean inside the compiler+

ra-jit embeds Lean from the start. Lean 4 is written in Lean and compiles to C, and its runtime is a C library with a C header, lean.h. ra-jit links Lean's runtime and elaborator into its own binary, the way a C program links any library.⁵+

At startup, ra-jit initializes the Lean runtime and the modules it needs, Lean's own and Mathlib's, once. The environment they build, every definition and theorem Mathlib has, then stays in memory for as long as ra-jit runs. Each obligation is a call into the elaborator and the kernel: no process boundary, no pipe and no JSON, and nothing to load again between edits.+

The community repl, which runs Lean as a subprocess and talks JSON on stdin, stays useful as a debugging fallback: an obligation can be written out and replayed there by hand. It is not how ra-jit checks proofs.⁹+

In the editor+

ra-jit's language server shows the proof state inline: the goal at the cursor inside a proof by lean block, which obligations were proved automatically and by which tactic, and which ones failed. A failed obligation is a diagnostic on the clause it came from.+

What a proof rests on+

unsafe functions and extern functions cannot be translated. They state an assumed ensures instead, which is trusted, like unsafe impl Send. For every proof, the compiler lists every assumption it rests on: assumed specs, axioms used by the Lean proof, and the MIR model itself. A reviewer reads that list, not the proof.+

Terms+

Lean here is the verification backend, not a code-generation backend. It checks claims and produces nothing that runs. Machine code still comes from ra-jit's normal backends, from the same MIR, and a function with a spec is compiled the same way as one without.+

What it buys+

• Claims about behaviour, checked on every build: sorted, in bounds, never overflows, never allocates.+

  No comments yet.

  Comments are not set up yet.

• Specs and proofs in the same file and the same diff as the code, so they cannot drift.+

  No comments yet.

  Comments are not set up yet.

• Mathlib's definitions and lemmas, usable in Rust specs, instead of writing a new library of facts.+

  No comments yet.

  Comments are not set up yet.

• Incremental proof checking: an edit rechecks the functions whose MIR or callee specs changed, and nothing else.+

  No comments yet.

  Comments are not set up yet.

• A loop language models are good at: write the proof, read the goal Lean shows, fix it. The compiler is the referee.+

  No comments yet.

  Comments are not set up yet.

• Review by assumptions: a diff that adds an assumed spec or an axiom shows up in the list a proof rests on.+

  No comments yet.

  Comments are not set up yet.

Prior art+

• Verus: specs and proofs in the Rust file, spec fn, requires and ensures, checked by an SMT solver. The surface syntax here follows it.+

  No comments yet.

  Comments are not set up yet.

• Aeneas and Charon: Rust to Lean from MIR, with backward functions for &mut. The translation here follows it.+

  No comments yet.

  Comments are not set up yet.

• Creusot: Rust specs in a Rust-like language, proved through Why3.+

  No comments yet.

  Comments are not set up yet.

• Prusti: Rust specs checked by the Viper verifier.+

  No comments yet.

  Comments are not set up yet.

• Kani: bounded model checking of Rust, used on std.+

  No comments yet.

  Comments are not set up yet.

• Flux: refinement types for Rust: the checkable claim lives in the type.+

  No comments yet.

  Comments are not set up yet.

• hax: Rust to F*, Lean and Rocq, for cryptographic code.+

  No comments yet.

  Comments are not set up yet.

• MiniRust: a precise specification of a Rust core close to MIR, the model the translation is checked against.+

  No comments yet.

  Comments are not set up yet.

• verify-rust-std: the AWS-led challenge to verify Rust's standard library, and the specs it has written so far.+

  No comments yet.

  Comments are not set up yet.

• Lean 4 reference: foreign function interface and Mathlib: the Lean side. leanprover-community/repl: Lean as a subprocess that answers JSON, the usual way tools drive Lean today.+

  No comments yet.

  Comments are not set up yet.

Open issues+

References

1. Verus Verified Rust: specs and proofs in the Rust file, checked by an SMT solver.
2. Aeneas Translates safe Rust to Lean as pure functions; &mut becomes a value and a backward function.
3. Creusot Deductive verification of Rust through Why3.
4. Mathlib Lean 4's library of mathematics.
5. Lean 4 reference: foreign function interface Calling C from Lean and Lean from C; marked unstable.
6. Charon Extracts a crate's MIR into a form other tools read; Aeneas's front end.
7. MiniRust Ralf Jung's precise specification of a Rust core close to MIR.
8. ra-jit: the function cache #[ra_jit::cache], and what makes a function ineligible.
9. leanprover-community/repl A JSON REPL for Lean 4 that reports goals, errors and sorries.
10. Prusti A static verifier for Rust, built on Viper.
11. Kani A bounded model checker for Rust.
12. Flux Refinement types for Rust.
13. hax Translates a subset of Rust to Lean, F* and Rocq.
14. verify-rust-std The challenge to verify Rust's standard library, announced by AWS in November 2024.