MiniRust: a spec written as an interpreter, for a Rust semantics nobody has pinned down

What the project is trying to settle

MiniRust is the cornerstone of a vision for a normative specification of Rust semantics, and it is described in the repository as a precise specification for Rust lite, MIR plus. It is an idealized MIR-like language with the purpose of serving as a core language of Rust.

The larger goal is stated precisely: to precisely specify the operational behavior of Rust, meaning the possible behaviors a Rust program might have when executed. The method is a two-step reduction. The behavior of a Rust program is defined by first translating it to MiniRust, a translation that is outside the scope of this repository, and then considering the possible behaviors of the MiniRust program as specified in the document.

The project is candid that the translation does a lot of work. Traits and pattern matching are basically gone at the MiniRust level. So the cost of the simplification is paid in the part that is not in the repository, and the benefit is that what remains can be specified exactly.

On the other side of that trade, MiniRust is concerned a lot with details such as the exact evaluation order, data representations, and precisely what is and is not Undefined Behavior.

That last phrase is the point of the whole project. Rust's undefined behaviour is a well known source of argument, and this is an attempt to draw the line formally rather than by convention.

The repository is not archived and the last push was on 2026-07-27, and there are no published GitHub releases. The licence is dual, with LICENSE-APACHE and LICENSE-MIT at the root. The author has also presented the work as video, at RustWeek 2025 and in an older, more in-depth presentation for the RFMIG, so the reasoning behind the design is available in spoken form as well as in the document.

The memory interface, defined but not implemented

The most unusual structural decision in the project is that memory is separated from the language by an interface, and that interface is left unimplemented.

The idea is to separate the complexities of memory from the semantics of MiniRust statements and expressions. The MiniRust memory interface treats memory as implementing some trait, and the MiniRust semantics is generic over the actual implementation of that trait. The interface between the MiniRust language, specified in lang, and its memory model, specified in mem, is untyped and byte-oriented, with the note that the bytes are a bit more complex than you might expect.

And then the key sentence: for now, only the memory interface is defined, but no implementation is given.

The claim that follows is the interesting one. Even without deciding what exactly the final memory model will look like, you can answer a surprising amount of interesting questions about Rust semantics. That is a strong claim, and it is the reason to look at the project even if you never intend to run it. If the language semantics can be specified in terms of an abstract memory, then a question like what is the effect of an out-of-bounds access can be answered as a property of the interface, and separately different implementations of the interface can be compared.

So the deliverable here is a specification with a deliberate hole in it, and the hole is the point rather than an oversight.

Values, types, and the deliberate absence of type safety

The most important concept to understand on the language side is that of a value and how it relates to types.

Values form a high-level, structural view of data, such as mathematical integers. Types serve to relate values with their low-level byte-oriented representation. And types are essentially just parameters attached to certain operations to define the de-serialization format.

That last framing is unusual and worth sitting with. A type in MiniRust is not primarily a safety guarantee, it is a description of how a value is laid out in bytes. The structural view of data and the byte view are related through the type, and the type is what says how to go between them.

Well-formedness of a MiniRust program ensures that expressions and statements satisfy some basic typing discipline, and then the sentence that catches people out: MiniRust is by design not type-safe.

So the typing discipline is there to make the program well formed, not to make it memory safe. A type-safe language rules out whole categories of misbehaviour by construction, and MiniRust deliberately does not, because the goal is to describe a language that has to admit the same programs real Rust admits. The memory model, not the type system, is where safety is supposed to come from.

That design is also why the memory interface is untyped and byte-oriented. If the types were the safety mechanism, the interface could be typed and the memory model could be high level. It is not, and so the interface has to work at the byte level.

specr lang, and why the spec is code

The most precise way to write down the MiniRust spec would be with mathematical notation, and the project explains why that was rejected: without LaTeX it is a pain, and it involves a lot of jargon which hurts accessibility of the spec.

So the MiniRust spec is written as an interpreter, so the spec itself is code. Which raises the question of what language that code is in, and the answer is specr lang, a kind of Rust-like pseudo-code.

The deviations from Rust are deliberate and each one has a reason. Imagine Rust without all the restrictions about sizedness and pointer indirections for recursive types, with the note that Arc could be implicitly inserted where needed. Generic type names like List, Map and Set rather than concrete implementations like Vec, HashMap and HashSet, since the implementation details do not matter. And some obvious language extensions, on the principle that it should always be clear what is meant to anyone with some Rust experience, even if this is not actually legal Rust.

There are more. All types except mutable references are Copy, with an implicit Clone where needed. The notation fn(T) -> U is used even for closures that can capture arbitrarily. And panic!, along with unwrap and slice indexing and similar standard Rust operations, indicates conditions that should always hold, so if execution ever panics that is a bug in the specification rather than a defined behaviour.

The functions are generally pure. They can write to mutable references, but that can be considered implemented via explicit state passing, and when other effects are needed they are made explicit in the return type.

So the spec is a program in a relaxed Rust, and the reader of the spec is reading code that describes what Rust does. That is the trade: less accessible than mathematics for some readers, more precise and more executable for everyone.

Failible operations, and two kinds of non-determinism

The effects used in the MiniRust interpreter are described in the next sections, and they are the parts of the language that have no direct Rust equivalent.

Fallible operations come first. Result is used to make operations fallible, where failure indicates UB or machine termination. A throw_ub! macro makes the current function return a UB error value, and throw_machine_stop! indicates that and how the machine has stopped. Inside Option-returning functions, throw!() returns None. And the function ret(t) wraps a value of type T as a Result<T>, an Option<T> or an NdResult<T>.

The second effect is non-determinism, which the project notes is a language feature Rust does not have direct support for. The return type Nondet<T> indicates that the function picks the returned T, and also its effect on the &mut it has access to, non-deterministically. It is only used in the memory model, because the expression language is perfectly deterministic, though it still has to propagate the memory model's non-determinism.

Within such a function, ? is used for monadic bind, which is more general than its usual role for short-circuiting, and the return value is implicitly wrapped in monadic return.

Then come two functions with opposite meanings, and the contrast is the point. pick<T>(impl Distribution<T>, fn(T) -> bool) -> Nondet<T> returns a value satisfying the closure, and its non-determinism is interpreted daemonically, meaning the program has to be correct for every possible choice. predict<T>(fn(T) -> bool) -> Nondet<T> also returns a value satisfying the closure, but interpreted angelically, meaning there has to exist a possible choice that makes the program behave as intended.

The consequences are sharp. For pick, a closure of |_| false or an uninhabited T means no behavior, which is described as the opposite of Undefined Behavior. For predict, the same situation is exactly like hint::unreachable_unchecked(), so ever reaching that operation is Undefined Behavior.

The Distribution argument to pick is a hint for the interpreter to sample suitable candidates, and it does not affect the set of possible program behaviors. The combined monad Nondet<Result<T>> is abbreviated NdResult<T>.

Editorial conclusion

MiniRust suits a compiler or tooling engineer who needs to reason precisely about what a Rust program is allowed to do, especially around evaluation order, data representation and the boundary of undefined behaviour, and it suits a reader who wants a spec they can execute. It is a poor fit for application work, since it is a specification and not a usable language, and it is a poor fit if you need a finished memory model, because the interface is defined but no implementation is given. Before relying on it, read the language and memory sections in spec/ and the mini directory, and treat the interpreter as a reference for the intended semantics rather than as a settled standard, since the project describes itself as one part of a larger story.

Frequently asked questions

Official sources

1. Issues
2. License: Apache-2.0
3. minirust/minirust on GitHub
4. README