Verify Rust Std Lib

Tool Name

KMIR

Description

KMIR is a formal verification tool for Rust that defines the operational semantics of Rust’s Middle Intermediate Representation (MIR) in K (through Public / Stable MIR). By leveraging the K framework, KMIR provides a parser, interpreter, and symbolic execution engine for MIR programs. This tool enables direct execution of concrete and symbolic input, with step-by-step inspection of the internal state of the MIR program's execution, serving as a foundational step toward full formal verification of Rust programs. Through the dependency Stable MIR JSON, KMIR allows developers to extract serialized Stable MIR from Rust’s compilation process, execute it, and eventually prove critical properties of their code.

This diagram describes the extraction and verification workflow for KMIR:

The K Framework (kframework.org) is the basis of how KMIR operates to guarantee properties of Rust programs. K is a rewrite-based semantic framework based on matching logic in which programming languages, their operational semantics and type systems, and formal analysis tools can be defined through syntax, configurations, and rules. The syntax definitions in KMIR model the AST of Stable MIR (e.g., the statements and terminator of a basic block in a function body) and configuration data that exists at runtime (e.g., the stack frame structure of a function call). The configuration of a KMIR program organizes the state of an executed program in nested configuration units called cells (e.g., a stack frame is part of a stack stored in the configuration). K Framework transition rules of the KMIR semantics are rewriting steps that match patterns and transform the current continuation and state accordingly. They describe how program configuration and its contained data changes when particular program statements or terminators are executed (e.g., a returning function modifies the call stack and writes a return value into the caller's local variables).

Using the K semantics of Stable MIR, the KMIR execution of an entire Rust program represented as Stable MIR breaks down to a series of configuration rewrites that compute data held in local variables, and the program may either terminate normally or reach an exception or construct with undefined behaviour, which terminates the execution abnormally. KMIR is designed to provide sound assurances about undefined behavior (UB) for the MIR constructs it supports (see Known Limitations). Rather than statically over‑approximating or flagging UB at every unsafe block, KMIR models the MIR semantics, including UB transitions, using a refusal-to-execute strategy. This means that if symbolic execution reaches a MIR instruction and cannot prove that executing it would not result in UB (e.g., an out-of-bounds pointer dereference or an unchecked arithmetic overflow), execution halts in a UB DETECTED state. This state cannot be unified with a valid target state in the proof, so the proof fails. KMIR systematically explores all feasible paths under the user-supplied preconditions. Only when every path terminates without hitting UB and satisfies the target property does KMIR declare the program UB-free (and correct for the property). A “no UB” claim therefore holds under the assumptions that KMIR’s implementation is correct and that the program stays within the supported subset of MIR.

Programs modelled in K Framework can be executed symbolically, i.e., operating on abstract input which is not fully specified but characterized by path conditions (e.g., that an integer variable holds an unknown but non-negative value).

In practice, KMIR proof harnesses work similarly to property tests. Arguments to the entry function are automatically instantiated as fully symbolic values, so the proof covers all possible inputs. Post-conditions are expressed using assert! statements. Pre-conditions can be added using std::intrinsics::assume, which constrains the symbolic path condition to restrict the inputs under consideration. This design allows users to write verification harnesses in plain Rust without needing to write K (excepting advanced features).

#![feature(core_intrinsics)]
use std::intrinsics::assume;

fn abs_safe(x: i32) {
    unsafe { assume(x != i32::MIN); }
    let result = x.abs();
    assert!(result >= 0);
}

When KMIR is directed to prove abs_safe, x is instantiated symbolically. The assume adds x != i32::MIN as a path constraint, and KMIR proves the assertion holds for all values satisfying that constraint.

K (and thus KMIR) verifies program correctness by performing an all-path-reachability proof using the symbolic execution engine and verifier derived from the K encoding of the Public MIR operational semantics. The K semantics framework is based on reachability logic, which is a theory describing transition systems in matching logic. An all-path-reachability proof in this system verifies that a particular target end state is always reached from a given starting state. The rewrite rules branch on symbolic inputs, covering the feasible transitions of the program. For all-path reachability, every leaf state is required to unify with the target state. A one-path-reachability proof is similar to the above, but the proof requirement is that at least one leaf state unifies with the target state.

When performing a proof of a program that involves recursion or a loop construct, one of several possible techniques can be used:

1. K (and thus KMIR) are capable of unbounded verification via allowing the user to write loop invariants. However, these loop invariants would then need to be written in K's native language.
2. As potential future work, it would be possible to implement an annotation language to provide the required context for loop invariant directly in source code (as done in the past using natspec for Solidity code).
3. In general, K also supports bounded loop unrolling, by way of identifying loop heads and counting how many times the same loop head has been observed. This technique is managed by the all-path reachability prover library for K and works out of the box with suitable arguments, without requiring any special support from the back-end.

By default, KMIR will attempt to exhaustively unroll a loop. Loop invariants have been applied to the verification of the Solana P-Token / SPL-Token Equivalence (see Case Study 2) to summarise the behaviour of an iterator; see the P-Token loop and the P-Token lemma.

KMIR also prioritizes UI with interactive proof exploration available out-of-the-box through the terminal KCFG (K Control Flow Graph) viewer, allowing users to inspect intermediate states of the proof to get feedback on the successful path conditions and failing at unifying with the target state. An example of a KMIR proof being analyzed using the KCFG viewer can be seen below:

Tool Information

• Does the tool perform Rust verification? Yes – It performs verification at the MIR level, an intermediate representation of Rust programs in the Rust compiler rustc.
• Does the tool deal with unsafe Rust code? Yes – By operating on MIR, KMIR can analyze both safe and unsafe Rust code.
• Does the tool run independently in CI? Yes – KMIR can be integrated into CI workflows via our package manager and Nix-based build system or through a docker image provided.
• Is the tool open source? Yes – KMIR is open source and available on GitHub.
• Is the tool under development? Yes – KMIR is actively under development, with ongoing improvements to MIR syntax coverage and verification capabilities.
• Will you or your team be able to provide support for the tool? Yes – The Runtime Verification team is committed to supporting KMIR and will provide ongoing maintenance and community support.

Licenses

KMIR is released under an OSI-approved open source license. It is distributed under the BSD-3 clause license, which is compatible with the Rust standard library licenses. Please refer to the KMIR GitHub repository for full license details.

Comparison to Other Approved Tools

The other tools approved at the time of writing are Kani, Verifast, and Goto-transcoder (ESBMC).

• Verification Backend: KMIR primarily differs from all of these tools by utilizing a unique verification backend through the K framework and reachability logic (as explained in the description above). KMIR has little dependence on an SAT solver or SMT solver. Kani's CBMC backend and Goto-transcoder (ESBMC) encode the verification problem into an SAT / SMT verification condition to be discharged by the appropriate solver. Kani recently added a Lean backend through Aeneas, however Lean does not support matching or reachability logic currently. Verifast performs symbolic execution of the verification target like KMIR, however reasoning is performed by annotating functions with design-by-contract components in separation logic.
• Verification Input: KMIR takes input from Stable MIR JSON, an effort to serialize the internal MIR in a portable way that can be reusable by other projects.
• K Ecosystem: Since all tools in the K ecosystem share a common foundation of K, all projects benefit from development done by other K projects. This means that performance and user experience are projected to improve due to the continued development of other semantics.

Known Limitations

KMIR is under active development. The following summarises notable limitations at the time of writing:

Language features not yet supported:

• Floating point types (f16, f32, f64, f128)
• Heap allocating types: Strings and Vec
• Smart pointers (Box, Rc, Arc)
• Async/await
• Multi-threading and atomics
• Dynamic trait objects dyn T

Language feature partially supported:

• Iterators
• Casts
• unsafe code (Unions, raw pointers, etc.)
• usize/isize are modelled as fixed-width, not architecture-dependent

Steps to Use the Tool

Installation

3 methods to install KMIR are listed. Recommended is the Nix installation via kup.

Nix (via kup)

The recommended installation method uses kup, the K Framework package manager. This installs K Framework, kmir, and stable-mir-json on your system via Nix.

The following script installs Nix (if not already present) and kup:

bash <(curl https://kframework.org/install)

Then install kmir:

kup install kmir

kmir is now installed on the path:

kmir --help

Docker

KMIR is available as a Docker image on Docker Hub. The image contains K Framework, the kmir tool, and stable-mir-json.

The following commands may require sudo permissions.

docker run --rm \
  runtimeverificationinc/kmir:<LATEST-VERSION-FROM-DOCKERHUB> \
  kmir --help

To run a proof using Docker, mount your working directory into the container:

docker run --rm \
  -u $(id -u):$(id -g) \
  -v /path/to/your/files:/workspace \
  runtimeverificationinc/kmir:<LATEST-VERSION-FROM-DOCKERHUB> \
  kmir prove /workspace/program.rs --proof-dir /workspace/proofs --verbose

The -u flag ensures files created inside the container have the correct ownership on the host. The -v flag mounts a host directory so that input files are accessible and proof output persists after the container exits.

From source

The tools can be built from source as described in the mir-semantics repository. This requires Python >= 3.10, uv, K Framework, and Rust via rustup.

git clone --recurse-submodules https://github.com/runtimeverification/mir-semantics.git
cd mir-semantics
make build
make stable-mir-json

kmir can be invoked via uv (from repo root):

uv --project kmir/ -- kmir --help

Usage (Verification)

The kmir tool works with Stable MIR extracted from Rust programs via stable-mir-json, a custom driver for rustc that serializes a crate's Stable MIR to JSON.

To prove a program:

kmir prove <FILE>.rs --proof-dir <DIR> [--start-symbol <SYMBOL>] --verbose

Where <FILE> is the Rust source file to verify, <DIR> is the directory where proof artifacts are stored, and <SYMBOL> is the entry function to verify (defaults to main if omitted).

This invokes stable-mir-json internally, then performs an all-path reachability proof that the program reaches normal termination under all possible inputs. Any statements that would panic or cause undefined behaviour terminate execution, so successful completion proves their absence. Pre-conditions and post-conditions can be modelled using conditional execution and assertions.

To inspect proof results, the proof ID is <FILE>.<SYMBOL>, e.g., proving program.rs produces proof ID program.main:

kmir show <FILE>.<SYMBOL> --proof-dir <DIR> --leaves --statistics
kmir view <FILE>.<SYMBOL> --proof-dir <DIR>

Useful Prove Flags

Proof state is automatically written to disk at every branch point and leaf node. Additional state can be emitted with flags to kmir prove.

It is recommended to use --terminate-on-thunk, which stops the proof when an unevaluated symbolic value (thunk) is encountered. This does not affect soundness, but gives feedback of the proof failure from the earliest point a K rule could not apply.

If a --proof-dir <DIR> is supplied, proof progress is written to disk. If a proof is cancelled before completion, calling the same command with the same --proof-dir <DIR> will read the state from disk and continue the proof from there. Otherwise the --reload flag will start the proof overwriting the previous entry.

Furthermore, performance for a proof can be increased with parallelism. We recommend --max-workers 4 which empirical evidence suggests is an optimal number of workers for a proof.

KMIR Case Studies

Case Study 1: Verify Std Rust Challenge 11

Challenge 11 requires verifying the safety of public unsafe methods for numeric primitives in core::num. KMIR successfully verified the correctness of all scoped integer operations. Float operations remain future work. For details, please visit the proof suite.

For each unsafe method, two harness files are written:

PASSING ( unchecked_add.rs ): calls the unsafe method only when its safety precondition holds. KMIR proves all paths terminate without UB:

fn unchecked_add_u128(a: u128, b: u128) {
    if let Some(expected) = a.checked_add(b) {
        let result = unsafe { a.unchecked_add(b) };
        assert!(result == expected);
    }
}

FAILING ( unchecked_add-fail.rs ): calls the unsafe method on arbitrary symbolic inputs without a precondition. KMIR detects UB on overflow paths and the proof fails:

fn unchecked_add_u128(a: u128, b: u128) {
    let result = unsafe { a.unchecked_add(b) };
    assert!(result == a.wrapping_add(b)); // UB
}

Each failing test has an expected failure state recorded in the show directory.

The full set of verified methods covers all integer types (i8-i128, u8-u128):

Case Study 2: Solana P-Token / SPL-Token Equivalence Proofs

KMIR has been used to formally verify the equivalence of the Solana P-Token (a compute-optimized rewrite using Pinocchio) against the original Solana SPL-Token program.

The verification proves that the P-Token program simulates the SPL-Token program: for each SPL-Token state and instruction (a request to perform an operation such as Transfer or Burn), there is an equivalent P-Token state and instruction that produces the same result. Both programs must agree on state transitions and error behaviour.

Each instruction is verified twice (once for each implementation) against a shared specification harness that captures the initial account state, invokes the instruction processor with symbolic input, and verifies the same postcondition holds after execution. 41 proofs are required to demonstrate equivalence.

For more details, please see:

• Proof Status
• Multisig Proof Status
• Shared Specifications
• SPL-Token Implementation
• P-Token Implementation

A detailed report covering the Solana programming model, the formal equivalence methodology, and per-instruction verification conditions is available in the equivalence proofs report.

Background Reading

• Matching Logic Matching Logic is a foundational logic underpinning the K framework, providing a unified approach to specifying, verifying, and reasoning about programming languages and their properties in a correct-by-construction manner.

• K Framework The K Framework is a rewrite-based executable semantic framework designed for defining programming languages, type systems, and formal analysis tools. It automatically generates language analysis tools directly from their formal semantics.