<<<<<<< HEAD

tag-std

This project aims to provide an annotation-based approach to managing safety-related comments in unsafe Rust code. It has three main objectives:

• The annotation system should be user-friendly and compatible with existing developer workflows.
• The annotations should be syntactically checkable by the compiler, thereby enabling standardized usage.
• If sufficiently precise, the annotations could also support formal verification, for example by being extended into contracts. However, this is not required for general projects.

See this pre-RFC for more details.

The project is named tag-std because it was originally intended to standardize safety property annotations for unsafe code within the Rust core and standard libraries through a simple yet precise tag-based approach. We have already defined a set of primitive safety properties to describe the safety concerns associated with unsafe APIs in the standard library, and we have labeled these unsafe APIs with tags accordingly. In addition, we have developed a systematic method to detect annotation discrepancies through program analysis, demonstrating the effectiveness of safety tags. For more details, please refer to our paper:

• "Annotating and Auditing the Safety Properties of Unsafe Rust", Zihao Rao, Hongliang Tian, Xin Wang, Hui Xu, arXiv:2504.21312, 2025.

While we are formulating the annotation method and developing the corresponding tools, we are also exploring the application of this approach to Rust projects beyond the standard library, including Rust-for-Linux and Asterinas

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	Open
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.

398ff24d1e50b98cb38e3b9f1c180ffddcc454de