From 5adfe4a83284d8e66ede00aaa417662898cd09d9 Mon Sep 17 00:00:00 2001 From: Stefan Zetzsche Date: Fri, 28 Aug 2026 14:12:14 +0000 Subject: [PATCH 1/2] docs: mark NonZero challenge as resolved --- doc/src/challenges/0012-nonzero.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/doc/src/challenges/0012-nonzero.md b/doc/src/challenges/0012-nonzero.md index 2c48386dfdb3c..bd81632bf875a 100644 --- a/doc/src/challenges/0012-nonzero.md +++ b/doc/src/challenges/0012-nonzero.md @@ -1,6 +1,7 @@ # Challenge 12: Safety of `NonZero` -- **Status:** Open +- **Status:** Resolved +- **Winning Solution:** [#637](https://github.com/model-checking/verify-rust-std/pull/637) - **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71) - **Start date:** *2024/08/23* - **End date:** *2025/04/10* From 7706e4614b5a76089c733daa177609b25c3cf787 Mon Sep 17 00:00:00 2001 From: Stefan Zetzsche Date: Sun, 30 Aug 2026 09:51:52 +0000 Subject: [PATCH 2/2] docs: address Challenge 12 follow-up feedback --- README.md | 2 +- doc/src/challenges/0012-nonzero.md | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/README.md b/README.md index 5bdeac61207db..d167fb1854a64 100644 --- a/README.md +++ b/README.md @@ -36,7 +36,7 @@ These are the challenges: | [9: Safe abstractions for `core::time::Duration`](https://model-checking.github.io/verify-rust-std/challenges/0009-duration.html) | N/A | [Resolved](https://github.com/model-checking/verify-rust-std/pull/136) | [Kani](https://github.com/model-checking/verify-rust-std/blob/main/library/core/src/time.rs) | | [10: Memory safety of String](https://model-checking.github.io/verify-rust-std/challenges/0010-string.html) | 10,000 USD | Open | | | [11: Safety of Methods for Numeric Primitive Types](https://model-checking.github.io/verify-rust-std/challenges/0011-floats-ints.html) | N/A | [Resolved](https://github.com/model-checking/verify-rust-std/issues/59) | [Kani](https://github.com/model-checking/verify-rust-std/tree/main/library/core/src/num) | -| [12: Safety of `NonZero`](https://model-checking.github.io/verify-rust-std/challenges/0012-nonzero.html) | 10,000 USD | Open | | +| [12: Safety of `NonZero`](https://model-checking.github.io/verify-rust-std/challenges/0012-nonzero.html) | 10,000 USD | [Resolved](https://github.com/model-checking/verify-rust-std/pull/637) | [Kani](https://github.com/model-checking/verify-rust-std/blob/main/library/core/src/num/nonzero.rs) | | [13: Safety of `CStr`](https://model-checking.github.io/verify-rust-std/challenges/0013-cstr.html) | 10,000 USD | Open | | | [14: Safety of Primitive Conversions](https://model-checking.github.io/verify-rust-std/challenges/0014-convert-num.html) | TBD | [Resolved](https://github.com/model-checking/verify-rust-std/pull/247) | [Kani](https://github.com/model-checking/verify-rust-std/blob/main/library/core/src/convert/num.rs) | | [15: Contracts and Tests for SIMD Intrinsics](https://model-checking.github.io/verify-rust-std/challenges/0015-intrinsics-simd.html) | 20,000 USD | Open | | diff --git a/doc/src/challenges/0012-nonzero.md b/doc/src/challenges/0012-nonzero.md index bd81632bf875a..afab984ef0cba 100644 --- a/doc/src/challenges/0012-nonzero.md +++ b/doc/src/challenges/0012-nonzero.md @@ -4,8 +4,8 @@ - **Winning Solution:** [#637](https://github.com/model-checking/verify-rust-std/pull/637) - **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71) - **Start date:** *2024/08/23* -- **End date:** *2025/04/10* - **Reward:** *10000 USD* +- **Contributors**: [Stefan Zetzsche](https://github.com/stefanzetzsche) -------------------