Instrument the Rust standard library with safety contracts

[nikomatsakis]

Metadata
Point of contact	@celinval
Team(s)	compiler, libs
Goal document	2025h1/std-contracts

Summary

Finish the implementation of the contract attributes proposed in the compiler [MCP-759],
and port safety contracts from the [verify-rust-std] fork to the Rust standard library.

Tasks and status

• Discussion and moral support (libs )

Experimental Contract attributes

• Author MCP
• Implementation (@celinval)
• Standard reviews (compiler )
• Design meeting (compiler )

Standard Library Contracts

• Standard Library Contracts (@celinval, @tautschnig)
• Writing new contracts ()
• Standard reviews (libs )

[nikomatsakis]

This issue is intended for status updates only.

For general questions or comments, please contact the owner(s) directly.

[celinval]

Update: So far we have integrated Kani into our repository and we have successfully instrumented and verified 22 functions in the standard library. We have also published 11 challenges.

We are currently investigating the integration of other tools, such as Gillian Rust and Verus.

[celinval]

Key developments: We have welcome the help of students from the CMU Practicum Project. They have started writing functions contracts that include the safety conditions for some unsafe functions in the core library, as well as verifying that safe abstractions respect those pre-conditions and are indeed safe.
Help wanted: Contracts and verification harnesses are being added to our existing fork: https://github.com/model-checking/verify-rust-std. Help needed to write more contracts, to integrate new tools, to review pull requests or to participate in the repository discussions.

[celinval]

Key developments: A new partnership between the Rust Foundation and AWS will help fund this effort [ref]. The verification challenges in the verify-rust-std fork now have financial rewards for those completing them.
Help wanted: Help needed to write more contracts, to integrate new tools, to review pull requests or to participate in the repository discussions.

[celinval]

Key developments: We have written and verified around 220 safety contracts in the verify-rust-std fork. 3 out of 14 challenges have been solved. We have successfully integrated Kani in the repository CI, and we are working on the integration of 2 other verification tools: VeriFast and Goto-transcoder (ESBMC)

[nikomatsakis]

This is a continuing project goal, and the updates below this comment will be for the new period 2025h1

[celinval]

We have been able to merge the initial support for contracts in the Rust compiler under the contracts unstable feature. @tautschnig has created the first PR to incorporate contracts in the standard library and uncovered a few limitations that we've been working on.

[celinval]

We fixed issue rust-lang/rust#136925 that was blocking contract annotations on constant functions, which unblocks the initial PR to add some contract annotations in the standard library (rust-lang/rust#136578). The PR currently triggers a CI failure which we are investigating.