Verify the Safety of the Rust Standard Library

Rust is one of the fastest growing languages around the world. The Rust community has grown into millions of developers, with more products and services relying on Rust. The ergonomics and strong compiler guarantees make Rust an ideal choice for developers. With this growth though, the Rust community has also recognized the unsafety of Rust (if used incorrectly). Specifically, when developers leave the walled garden of the compiler to implement their solutions, the Rust compiler places the onus of safety on the developer. The core libraries of Rust make use of this unsafe feature significantly, which is unverified. We believe that providing formal guarantees for these libraries will improve the Rust ecosystem for everyone.

In this post, we are pleased to announce a community wide effort to verify the Rust standard libraries for safety. The effort is structured as a challenge-based contest where each challenge describes a verification goal for a subset of the Rust libraries. Each challenge is created with a financial reward, which is awarded upon successful completion of the challenge. The Rust Foundation has reviewed our plans and agreed to host this endeavor.

How is Rust unsafe?

Rust aims at being a safe and performant language. Its type system and ownership model provide strong safety guarantees; however, this model can be too restrictive (for efficiency, hardware access, legacy etc.). To overcome that, Rust provides a mechanism to perform unsafe operations that escape the guarantees of the compiler. Developers can create and use safe abstractions over unsafe code by delimiting the specific code that requires extra functionality. The Rust standard library, composed of a few crates such as core, alloc, and std, provides efficient implementations and safe abstractions for the most common general purpose programming data structures and operations. By doing so, they perform unsafe operations internally, which have not been formally verified or proven safe. The onus is placed on the developer to understand and evaluate the usage of unsafe operations. If done incorrectly, this can result in undefined behavior (UB).

Today, the Rust standard library comprises roughly 35K functions, with approximately 7.5K unsafe functions, and 3K safe abstractions. The core library has 21K functions, with 7K unsafe functions and 1.7K safe abstractions.

In the last 3 years, 57 soundness issues have been filed in the Rust standard library and 20 CVEs have been reported. Of these soundness issues, 28% of them were discovered in 2024, telling us that the rate of change of the standard libraries is faster and more unsound. Over 90% of Rust based products/services depend on the Rust standard library with virtually every Rust application depending on the core library.

Verification Landscape

Recently, there have been significant efforts to create tools and techniques that enable verification of safe and unsafe Rust code. Here we list some of the tools (alphabetically):

• Aeneas translates Rust’s intermediate representation to Coq, Lean, F* and HOL4. This enables interactive theorem proving of Rust programs.
• Creusot is a Rust verifier that also employs deductive-style verification for safe Rust code. Creusot also introduces Pearlite – a specification language for specifying function and loop contracts. Creusot today requires manually writing specifications, which can be time consuming and add to code maintenance.
• Gillian-Rust is a separation logic-based hybrid verification tool for Rust programs. The approach combines automated verification of safe Rust with targeted semi-automated verification of unsafe Rust.
• Kani uses bounded model checking to verify generic memory safety properties, a subset of Rust undefined behaviors, and user specified assertions. Kani supports both unsafe and safe code, but cannot guarantee unbounded verification in all cases.
• Miri is a Rust interpreter with built-in checks for undefined behavior. As an interpreter it is under-approximating, but can be effective with good test coverage. Miri is used by the Rust project itself.
• Prusti employs deductive verification to prove functional correctness of safe Rust code. Specifically, it targets certain type of panics and allows users to specify properties of interest.
• Verus is an SMT-based tool used to verify Rust code and can support unsafe in certain situations such as the use of raw pointers and ref cells.
• There are other related tools, but we do not list them here due to the scope of this article.

Verifying the Rust libraries is difficult because: 1/ lack of a specification, 2/ lack of an existing verification mechanism in the Rust ecosystem, 3/ the large size of the verification problem, and 4/ the unknowns of scalable verification. Given the magnitude and scope of the effort, we believe that a single team would be unable to make significant inroads. Our approach is to create a community owned effort.

Crowd-sourcing the verification

To overcome such challenges, we have started a crowd-sourced verification effort, wherein verifying the Rust standard library is specified as a set of challenges. Each challenge describes the goal and the success criteria. Currently, we are focusing on doing verification for memory-safety and a subset of undefined behaviors. The challenges are open to anyone. This effort aims to be tool agnostic to facilitate the introduction of verification solutions into the Rust language repositories. Our vision is to have multiple tools can be used for verification as a continuous process rather than discreet one-off events. We have been working with the Rust language team to introduce function and loop contracts into the Rust mainline and have created a fork of the Rust standard library repository wherein all solutions to challenges and verification artifacts are stored.

Challenges can come in various flavors: 1/ specifying contracts for a part of the Rust standard library, 2/ specifying and verifying a part of the Rust standard library, and 3/ introducing new tools or techniques to verify parts of the Rust standard library. The repository provides templates for introducing new challenges, new tools, and instructions on how to submit solutions to challenges. To date, over 20 students, academics, and researchers have been involved in the challenge. As part of this effort, we are also creating more challenges.

For example, we have created a challenge to verify the String library in the standard library [6]. In this challenge, the goal is to verify the memory safety of std::string::String and prove the absence of undefined behavior (UB). Even though the majority of String methods are safe, many of them are safe abstractions over unsafe code. For instance, the insert method is implemented as follows :

1 pub fn insert(&mut self, idx: usize, ch: char) {
2   assert!(self.is_char_boundary(idx));
3   let mut bits = [0; 4];
4   let bits = ch.encode_utf8(&mut bits).as_bytes();
5
6   unsafe {
7     self.insert_bytes(idx, bits);
8   }
9 }

The challenge also specifies the success criteria that must be met for the solution to be reviewed and merged into the forked repository CI pipeline. Today, several challenges already exist, and are being actively worked on. You can view part of a solution to a challenge in the verify-rust-std repository.

This effort is tool agnostic and encourages the usage of multiple tools, as long as they can be used in CI. For example, this request is for introducing a new tool in the repository and verification ecosystem. ESBMC is a tool that is being modified to accept Rust code for verification. All issues, solutions, pull requests etc. are reviewed by a technical review committee. The technical review committee is open to anyone in the community and requires a simple pull request to add oneself. The rewards committee is responsible for reviewing and disbursing this.

Finally, our call to action for you is to join this effort in any capacity (reviews, proofs, tools etc.). To learn more and engage, you can visit our GitHub repository.