Surveying the Rust Verification Landscape

TL;DR

The paper surveys the Rust verification landscape, focusing on how to verify Rust code in the presence of Unsafe Rust with an emphasis on the standard library. It analyzes which properties to verify (safety and domain-specific correctness), how to verify them (MIR- and LLVM-based IRs, bounded model checking vs deductive approaches), and what to verify (standard library first, then crates and client code). It discusses challenges in specifying unsafe behavior, encapsulation of unsafety, and the need for machine-readable specifications, while proposing Kani as a practical starting tool and outlining human factors and community engagement. The work aims to inform the verification community about practical strategies, tooling gaps, and procedural considerations for robustly verifying Rust code and fostering safer Rust ecosystems with broad impact.

Abstract

Rust aims to be a safe programming language applicable to systems programming applications. In particular, its type system has strong guardrails to prevent a variety of issues, such as memory safety bugs and data races. However, these guardrails can be sidestepped via the unsafe keyword. unsafe allows certain otherwise-prohibited operations, but shifts the onus of preventing undefined behaviour from the Rust language's compile-time checks to the developer. We believe that tools have a role to play in ensuring the absence of undefined behaviour in the presence of unsafe code. Moreover, safety aside, programs would also benefit from being verified for functional correctness, ensuring that they meet their specifications. In this research proposal, we explore what it means to do Rust verification. Specifically, we explore which properties are worth verifying for Rust; what techniques exist to verify them; and which code is worth verifying. In doing so, we motivate an effort to verify safety properties of the Rust standard library, presenting the relevant challenges along with ideas to address them.