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, 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	N/A	Resolved	Kani
2: Verify the memory safety of core intrinsics using raw pointers	N/A	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	5,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	N/A	Open
11: Safety of Methods for Numeric Primitive Types	N/A	Resolved	Kani
12: Safety of NonZero	N/A	Open
13: Safety of CStr	N/A	Open
14: Safety of Primitive Conversions	TBD	Resolved	Kani
15: Contracts and Tests for SIMD Intrinsics		Open
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

See our book for more details on the challenge rules.

We welcome everyone to participate!

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.

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.