Rust standard library verification

This repository is a fork of the official Rust programming language repository, created solely to verify the Rust standard library. It should not be used as an alternative to the official Rust releases. The repository is tool agnostic and welcomes the addition of new tools. The currently accepted tools are Flux, GOTO Transcoder (ESBMC), Kani, KMIR, and VeriFast.

The goal is to have a verified Rust standard library and prove that it is safe.

1. Contributing to the core mechanism of verifying the rust standard library
2. Creating new techniques to perform scalable verification
3. Apply techniques to verify previously unverified parts of the standard library.

For that we are launching a contest supported by the Rust Foundation that includes a series of challenges that focus on verifying memory safety and a subset of undefined behaviors in the Rust standard library. Each challenge describes the goal, the success criteria, and whether it has a financial award to be awarded upon its successful completion.

These are the challenges:

Challenge	Reward	Status	Proof
1: Verify core transmuting methods	10,000 USD	Resolved	Kani
2: Verify the memory safety of core intrinsics using raw pointers	10,000 USD	Open
3: Verifying Raw Pointer Arithmetic Operations	N/A	Resolved	Kani
4: Memory safety of BTreeMap's btree::node module	10,000 USD	Open
5: Verify functions iterating over inductive data type: linked_list	20,000 USD	Resolved	VeriFast
6: Safety of NonNull	N/A	Resolved	Kani
7: Safety of Methods for Atomic Types & Atomic Intrinsics	10,000 USD	Open
8: Contracts for SmallSort	10,000 USD	Open
9: Safe abstractions for core::time::Duration	N/A	Resolved	Kani
10: Memory safety of String	10,000 USD	Open
11: Safety of Methods for Numeric Primitive Types	N/A	Resolved	Kani
12: Safety of NonZero	10,000 USD	Open
13: Safety of CStr	10,000 USD	Open
14: Safety of Primitive Conversions	N/A	Resolved	Kani
15: Contracts and Tests for SIMD Intrinsics	20,000 USD	Resolved	Testable Models
16: Verify the safety of Iterator functions	10,000 USD	Open
17: Verify the safety of slice functions	10,000 USD	Open
18: Verify the safety of slice iter functions	10,000 USD	Open
19: Safety of RawVec	10,000 USD	Resolved	VeriFast
20: Verify the safety of char-related functions in str::pattern	25,000 USD	Open
21: Verify the safety of substring-related functions in str::pattern	25,000 USD	Open
22: Verify the safety of str iter functions	10,000 USD	Open
23: Verify the safety of Vec functions part 1	15,000 USD	Open
24: Verify the safety of Vec functions part 2	15,000 USD	Open
25: Verify the safety of VecDeque functions	10,000 USD	Open
26: Verify reference-counted Cell implementation	10,000 USD	Open
27: Verify atomically reference-counted Cell implementation	10,000 USD	Open
28: Verify float to decimal conversion module	5,000 USD	Open
29: Safety of boxed	15,000 USD	Open

See our book for more details on the challenge rules.

We welcome everyone to participate!

Citing this project

If you use this project in your research, please cite our NFM 2026 paper.

ACM Reference Format:

Byron Cook, Remi Delmas, Zyad Hassan, Bart Jacobs, Ranjit Jhala, Rahul Kumar, Felipe R. Monteiro, Thanh Nguyen, Rebecca Rumbul, Michael Tautschnig, Celina Val, and Carolyn Zech. 2026. Verifying the Rust Standard Library. In NASA Formal Methods: 18th International Symposium, NFM 2026, Los Angeles, CA, USA, May 5–7, 2026, Proceedings. Springer-Verlag, Berlin, Heidelberg, 415–435. https://doi.org/10.1007/978-3-032-28079-4_19

BibTeX:

@inproceedings{10.1007/978-3-032-28079-4_19,
  author    = {Cook, Byron and Delmas, Remi and Hassan, Zyad and Jacobs, Bart and
               Jhala, Ranjit and Kumar, Rahul and Monteiro, Felipe R. and
               Nguyen, Thanh and Rumbul, Rebecca and Tautschnig, Michael and
               Val, Celina and Zech, Carolyn},
  title     = {Verifying the Rust Standard Library},
  year      = {2026},
  isbn      = {978-3-032-28078-7},
  publisher = {Springer-Verlag},
  address   = {Berlin, Heidelberg},
  url       = {https://doi.org/10.1007/978-3-032-28079-4_19},
  doi       = {10.1007/978-3-032-28079-4_19},
  booktitle = {NASA Formal Methods: 18th International Symposium, NFM 2026, Los Angeles, CA, USA, May 5–7, 2026, Proceedings},
  pages     = {415–435},
  numpages  = {21},
  location  = {Los Angeles, CA, USA}
}

The same citation is available in machine-readable form in CITATION.cff, which powers GitHub's Cite this repository button.

Contact

For questions, suggestions or feedback, feel free to open an issue here.

Security

See SECURITY for more information.

License

Kani

Kani is distributed under the terms of both the MIT license and the Apache License (Version 2.0). See LICENSE-APACHE and LICENSE-MIT for details.

GOTO Transcoder (ESBMC)

The goto-transcoder is distributed under the terms of the MIT license. See LICENSE for details.

ESBMC is distributed under the terms of the Apache License (Version 2.0). See COPYING for details.

Flux

Flux is distributed under the terms of the MIT license. See LICENSE for details.

VeriFast

VeriFast is distributed under the terms of the MIT license. See LICENSE.md for details.

KMIR

KMIR is distributed under the terms of the BSD-3-Clause license. See LICENSE for details.

Rust

Rust is primarily distributed under the terms of both the MIT license and the Apache License (Version 2.0), with portions covered by various BSD-like licenses.

See the Rust repository for details.

Introducing a New Tool

Please use the template available in this repository to introduce a new verification tool.