Miri and Undefined-Behavior Detection

Miri is an official Mid-level Intermediate Representation (MIR) interpreter for Rust that executes programs and test suites in a virtual abstract machine to deterministically detect undefined behavior (UB), memory leaks, and aliasing violations that normal CPU execution silently ignores.

Why Normal Hardware Tests Miss Undefined Behavior

When compiled to native x86_64 or AArch64 machine code, memory is just a flat array of bytes: reading an uninitialized byte returns whatever bits happened to sit in RAM, and having two aliasing &mut i32 references executes normal CPU instructions until a future compiler version reorders them.

Miri does not compile code to native machine instructions. Instead, it interprets the compiler's MIR directly while tracking rich shadow metadata for every single byte and pointer:

Physical CPU Memory (Flat Bytes)       Miri Abstract Machine Memory
+------+------+------+------+          +-------------------+-------------------+
| 0x2A | 0x00 | 0xFF | 0x10 |          | Byte 0: Init(0x2A)| Byte 1: Uninit    |
+------+------+------+------+          | Prov: AllocId(14) | (Reading = Error!)|
  (Cannot distinguish uninitialized    | Borrow Stack:     |                   |
   bytes or invalidated pointer tags)  |  [Unique(#41),    |                   |
                                       |   SharedRW(#42)]  |                   |
                                       +-------------------+-------------------+

What Miri Detects

Defect Category	Detected by Miri?	Mechanism Used by Miri
Out-of-bounds reads, writes, and ptr.add()	Yes	Tracks exact allocation bounds (AllocId + byte length)
Use-after-free and dangling pointers	Yes	Marks AllocId as freed on deallocation or stack frame exit
Reading uninitialized memory or padding bytes	Yes	Tracks per-byte initialization state (Init vs. Uninit)
Aliasing violations (&mut overlap, mutating &T)	Yes	Enforces Stacked Borrows (default) or Tree Borrows (-Zmiri-tree-borrows)
Invalid bit patterns (invalid bool, char, enum tag, null &T)	Yes	Checks type validity invariants on every load, store, and cast
Unaligned pointer accesses and Layout mismatches on dealloc	Yes	Verifies address alignment and checks dealloc layout against alloc layout
Data races in multi-threaded code	Yes	Vector-clock race detector across emulated threads
Memory leaks (Box::leak, reference cycles, mem::forget)	Yes	Reports allocations still live when main exits

Installing and Running Miri

Miri runs on the nightly toolchain via rustup:

rustup +nightly component add miri
cargo +nightly miri run
cargo +nightly miri test

Example of Miri Catching a Stacked Borrows Aliasing Violation

The following code compiles without warnings and prints 20 when run normally with cargo run, but contains undefined behavior because creating and using r_mut invalidates the earlier raw pointer raw:

// Contains Undefined Behavior detected by `cargo +nightly miri run`!
fn main() {
    let mut x = 10;
    let raw: *mut i32 = &mut x;
    let r_mut: &mut i32 = &mut x;
    *r_mut = 15;

    // UB: `raw` was invalidated when `r_mut` was created from `x`!
    unsafe {
        *raw = 20;
    }
    println!("{}", x);
}

Running cargo +nightly miri run immediately pinpoints the exact aliasing violation:

error: Undefined Behavior: attempting a write access using <tag> at alloc123[0x0], but that tag does not exist in the borrow stack for this location
 --> src/main.rs:10:9
  |
10 |         *raw = 20;
  |         ^^^^^^^^^ this error occurs as part of an access at alloc123[0x0..0x4]
  |
help: <tag> was created by a SharedReadWrite retag at offsets [0x0..0x4]
 --> src/main.rs:4:25
  |
4 |     let raw: *mut i32 = &mut x;
  |                         ^^^^^^
help: <tag> was later invalidated at offsets [0x0..0x4] by a Unique retag
 --> src/main.rs:5:27
  |
5 |     let r_mut: &mut i32 = &mut x;
  |                           ^^^^^^

Useful MIRIFLAGS Options

Flag in MIRIFLAGS="..."	Effect
-Zmiri-tree-borrows	Uses the experimental Tree Borrows aliasing model instead of Stacked Borrows
-Zmiri-ignore-leaks	Disables the exit-time memory leak checker (useful when testing code that intentionally uses Box::leak or OnceLock)
-Zmiri-disable-isolation	Allows the interpreted program to access host environment variables, filesystem, and system clock
-Zmiri-symbolic-alignment-check	Enforces strict symbolic alignment checks instead of relying on lucky accidental numeric addresses