diff --git a/README.md b/README.md index b54f56aebf0e8..54d3758a44485 100644 --- a/README.md +++ b/README.md @@ -11,20 +11,22 @@ The goal is to have a contest to help verify the [Rust standard library](https:/ To help you get started in the contest, Amazon’s [Kani-rust-verifier team](https://github.com/model-checking/kani) has created mechanisms and tools to help participants verify the standard library. The Kani team has also created some initial contracts and proofs (To be filled and linked here later) to help you get started as a participant. + +NOTE: This work is not official, affiliated, or endorsed by the Rust project or Rust Foundation. * * * ## Contest Details Here are some details for the contest -1. This repository will contain templates for [Issues](http://Insert link to Issues page), [pull requests](http://Link to PR page here) etc. that will be used to create new challenges for verifying the Rust standard library. +1. This repository will contain templates for [Issues](https://github.com/model-checking/verify-rust-std/issues), and [pull requests](https://github.com/model-checking/verify-rust-std/pulls), that will be used to create new challenges for verifying the Rust standard library. 2. This repository will contain the initial contracts and proofs that AWS creates using Kani as a tool to verify the standard library. 3. Verification of the functions will be enabled using CI pipelines and Kani tool initially. 4. Any new tool that participants want to enable will require an application using an Issue template. This tool will be analyzed by an independent committee consisting of members from the Rust open-source developers and AWS 1. A new tool application should clearly specify the differences to existing techniques and provide sufficient background of why this is needed. 2. Once the tool is approved, it needs to be enabled using CI pipelines. 5. Each contribution or attempt should be submitted via a pull request that will be analyzed by the committee. -6. Each contribution will be reviewed on a first come first serve basis. Acceptance will be based on a unanimous affirmative vote from the review committee. +6. Each contribution will be reviewed on a first come first serve basis. Acceptance will be based on a unanimous affirmative vote from the review committee. 7. The contribution must be automated and should work in CI. 8. Once approved by the review committee, the change will be merged into the repository. @@ -53,7 +55,7 @@ You can find out more about Kani from the [Kani book](https://model-checking.git ## Contact -For questions, suggestions or feedback, feel free to open an issue on the Kani page with the tag `stdlib-contest` or contact us directly at [kani-developers@amazon.com](mailto:kani-developers@amazon.com). +For questions, suggestions or feedback, feel free to open an [issue here](https://github.com/model-checking/verify-rust-std/issues). ## Security @@ -65,7 +67,7 @@ See [SECURITY](https://github.com/model-checking/kani/security/policy) for more Kani is distributed under the terms of both the MIT license and the Apache License (Version 2.0). -See [LICENSE-APACHE](link to LICENSE-APACHE) and [LICENSE-MIT](link to LICENSE-MIT) for details. +See [LICENSE-APACHE](https://github.com/model-checking/kani/blob/main/LICENSE-APACHE) and [LICENSE-MIT](https://github.com/model-checking/kani/blob/main/LICENSE-MIT) for details. ## Rust @@ -73,5 +75,3 @@ See [LICENSE-APACHE](link to LICENSE-APACHE) and [LICENSE-MIT](link to LICENSE-M 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](https://github.com/rust-lang/rust) for details. - -