lean-miri — A proofs.rs project

Proving Rust programs free of undefined behavior

lean-miri is a port of Miri, Rust’s undefined-behavior checker, to Lean 4. It lets you state and prove safety properties of Rust programs under Miri’s execution model.

Why lean-miri?

Prove claims over arbitrary inputs and executions. Miri checks concrete executions; Lean lets you quantify over inputs, caller states, and nondeterministic choices. You can state function-level safety properties without constructing an executable test harness, and prove them under explicit assumptions.
Bring Miri’s language coverage to theorem proving. Advanced traits and unsafe pointer operations already have implementations in Miri. Porting this mature interpreter offers a path to broad Rust support without designing a verifier around a restricted language subset.
Preserve Miri’s detailed model of undefined behavior. Safety depends on more than bounds checks: pointer provenance, aliasing, initialization, and concurrency also matter. The aim is to carry Miri’s execution rules and UB checks into Lean, including its Tree Borrows model.

Examples

empty_function

An empty function still initializes a call frame and returns to its caller. This example proves that call initialization and every finite execution prefix within the call report no undefined behavior, under the declared caller and execution-profile conditions.

pub fn empty_function() {}

Safe resource exhaustion is allowed; normal return is not promised for every resource supply.

Lean definition and theorem statement

EmptyFunction.ActualNoUBFinal · theorem statement

theorem noUB
    (s : Static)
    (metadata : Metadata s) (profile : Profile s)
    (p : Packet) (runtime : RuntimeProfile s p)
    (input : InputDraft.CurrentInputDraft s p) :
    CallLevelNoUB.NoUB s p

EmptyFunction.TotalCallGoal · definition

def Target (s : Static) : Prop :=
  CallLevelNoUB.Target s
    (Nonempty (Metadata s)) (Profile s)
    (fun p => RuntimeProfile s p ∧
      Nonempty (InputDraft.CurrentInputDraft s p))

duplicate_prefix

Copy the first n bytes of a slice into the following n bytes. The bounds check guards an unsafe raw-pointer operation.

pub fn duplicate_prefix(buf: &mut [u8], n: usize) -> bool {
    if n == 0 {
        return true;
    }
    if n > buf.len() / 2 {
        return false;
    }
    let p = buf.as_mut_ptr();
    unsafe {
        std::ptr::copy_nonoverlapping(p, p.add(n), n);
    }
    true
}

For every count and every input in the declared domain, the theorem establishes normal return, no interpreter errors, and no undefined behavior on any permitted finite prefix. Caller, resource, and metadata conditions are explicit.

Lean theorem statement

DuplicatePrefix.CurrentCallOrdinarySafety

theorem invoke
    {options limits remaining span before argument len place}
    (input : OrdinaryInput options limits remaining
      span before argument len place)
    (count : UInt64) :
    DuplicatePrefixArgumentCallResult.Result
      options limits remaining span before
      argument len count place

The result concerns interpreter safety under the declared conditions. It does not establish formation from every Rust calling history or an additional guarantee about the returned Boolean.

Architecture

Rust programs are imported as data. The lean-miri interpreter provides the execution semantics used in safety proofs.

Lean’s kernel checks the proofs. The compiler, exporter, and correspondence between the interpreter and Rust remain trusted boundaries.