MiniRust is a formal specification of an idealized subset of Rust, known as MiniRust, with an executable model defined in a custom specification language (specr). The repository provides tooling that translates real Rust MIR (via rustc) into MiniRust and runs it through a reference interpreter. It includes a comprehensive test suite (minitest) covering pass, panic, and undefined behavior scenarios, along with utilities for program construction and pretty-printing. The work is squarely a formal-semantics research project, not a production application. It models pointer provenance, aliasing (Tree Borrows), concurrency, and data-race detection, and is primarily used to validate the Rust memory model. The codebase is well-structured with clean abstractions (pluggable memory model, builder API) but depends heavily on unstable rustc internals and has many incomplete features (e.g., floats, operators, casts).