Rust is most well-known for it strong type system, guaranteeing memory safety and thread safety despite a low-level programming paradigm that does not require a garbage collector. However, not all code can be written in the confines of a safe type system: sometimes, the programmer has to be more clever than the compiler permits. This is where unsafe Rust comes in, a set of additional operations that come with great power and great responsibility. They give programmers the power to program directly against the underlying machine model, side-stepping all the limitations of the type system. However, it is the programmer’s responsibility to ensure that the preconditions of these unsafe operations are maintained, or else runtime behavior is entirely unconstrained – the infamous Undefined Behavior.

Miri is a tool that helps programmers deal with this responsibility. Specifically, Miri can execute Rust code in a way that detects (almost) all Undefined Behavior. It is trivial to deploy, requiring no annotations and being distributed with the Rust nightly toolchain. Miri has found numerous bugs in real-world code and has become a standard tool for unsafe Rust programmers. That makes it the first practical tool for reliably detecting Undefined Behavior – in any language.

In this talk, I will give an overview of what kinds of bugs Miri is able to find, how Miri works, and how it helps in the ongoing effort of formally specifying the Rust language.