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:

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.