Docs: remove challenge end dates and fix README/challenge inconsistencies

CITATION.cff

@@ -0,0 +1,73 @@
+cff-version: 1.2.0
+title: Verifying the Rust Standard Library
+message: >-
+  If you use this project in your research, please cite the NFM 2026 paper
+  listed under `preferred-citation`.
+type: software
+authors:
+  - name: The verify-rust-std Contributors
+abstract: >-
+  A fork of the Rust standard library created solely to formally verify the Rust
+  standard library. The repository is tool-agnostic and integrates complementary
+  verification tools into its continuous integration to prove the absence of a
+  subset of undefined behaviors (e.g., out-of-bounds access, null and dangling
+  pointer dereferences, and use of uninitialized memory) in the standard
+  library.
+repository-code: https://github.com/model-checking/verify-rust-std
+url: https://model-checking.github.io/verify-rust-std/
+keywords:
+  - rust
+  - formal verification
+  - model checking
+  - program analysis
+  - undefined behavior
+  - standard library
+preferred-citation:
+  type: conference-paper
+  title: Verifying the Rust Standard Library
+  authors:
+    - given-names: Byron
+      family-names: Cook
+    - given-names: Remi
+      family-names: Delmas
+    - given-names: Zyad
+      family-names: Hassan
+    - given-names: Bart
+      family-names: Jacobs
+    - given-names: Ranjit
+      family-names: Jhala
+    - given-names: Rahul
+      family-names: Kumar
+    - given-names: Felipe R.
+      family-names: Monteiro
+    - given-names: Thanh
+      family-names: Nguyen
+    - given-names: Rebecca
+      family-names: Rumbul
+    - given-names: Michael
+      family-names: Tautschnig
+    - given-names: Celina
+      family-names: Val
+    - given-names: Carolyn
+      family-names: Zech
+  collection-title: >-
+    NASA Formal Methods: 18th International Symposium, NFM 2026, Los Angeles, CA,
+    USA, May 5–7, 2026, Proceedings
+  collection-type: proceedings
+  conference:
+    name: 18th International Symposium on NASA Formal Methods (NFM 2026)
+    city: Los Angeles
+    region: CA
+    country: US
+    date-start: '2026-05-05'
+    date-end: '2026-05-07'
+  publisher:
+    name: Springer-Verlag
+    city: Berlin
+    country: DE
+  isbn: 978-3-032-28078-7
+  year: 2026
+  start: 415
+  end: 435
+  doi: 10.1007/978-3-032-28079-4_19
+  url: https://doi.org/10.1007/978-3-032-28079-4_19

README.md

@@ -8,7 +8,7 @@ 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](https://model-checking.github.io/verify-rust-std/tools/flux.html), [GOTO Transcoder (ESBMC)](https://model-checking.github.io/verify-rust-std/tools/goto-transcoder.html), [Kani](https://model-checking.github.io/verify-rust-std/tools/kani.html), and [VeriFast](https://model-checking.github.io/verify-rust-std/tools/verifast.html).
+new tools. The currently accepted tools are [Flux](https://model-checking.github.io/verify-rust-std/tools/flux.html), [GOTO Transcoder (ESBMC)](https://model-checking.github.io/verify-rust-std/tools/goto-transcoder.html), [Kani](https://model-checking.github.io/verify-rust-std/tools/kani.html), [KMIR](https://model-checking.github.io/verify-rust-std/tools/kmir.html), and [VeriFast](https://model-checking.github.io/verify-rust-std/tools/verifast.html).
 
 The goal is to have a verified [Rust standard library](https://doc.rust-lang.org/std/) and prove that it is safe.
 1. Contributing to the core mechanism of verifying the rust standard library
@@ -38,8 +38,8 @@ These are the challenges:
 | [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 | |
 | [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 | |
+| [14: Safety of Primitive Conversions](https://model-checking.github.io/verify-rust-std/challenges/0014-convert-num.html) | N/A | [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 | [Resolved](https://github.com/model-checking/verify-rust-std/pull/423) | [Testable Models](https://github.com/model-checking/verify-rust-std/tree/main/testable-simd-models) |
 | [16: Verify the safety of Iterator functions](https://model-checking.github.io/verify-rust-std/challenges/0016-iter.html) | 10,000 USD | Open | |
 | [17: Verify the safety of slice functions](https://model-checking.github.io/verify-rust-std/challenges/0017-slice.html) | 10,000 USD | Open | |
 | [18: Verify the safety of slice iter functions](https://model-checking.github.io/verify-rust-std/challenges/0018-slice-iter.html) | 10,000 USD | Open | |
@@ -52,11 +52,46 @@ These are the challenges:
 | [25: Verify the safety of `VecDeque` functions](https://model-checking.github.io/verify-rust-std/challenges/0025-vecdeque.html) | 10,000 USD | Open | |
 | [26: Verify reference-counted Cell implementation](https://model-checking.github.io/verify-rust-std/challenges/0026-rc.html) | 10,000 USD | Open | |
 | [27: Verify atomically reference-counted Cell implementation](https://model-checking.github.io/verify-rust-std/challenges/0027-arc.html) | 10,000 USD | Open | |
+| [28: Verify float to decimal conversion module](https://model-checking.github.io/verify-rust-std/challenges/0028-flt2dec.html) | 5,000 USD | Open | |
+| [29: Safety of `boxed`](https://model-checking.github.io/verify-rust-std/challenges/0029-boxed.html) | 15,000 USD | Open | |
 
 See [our book](https://model-checking.github.io/verify-rust-std/intro.html) for more details on the challenge rules.
 
 We welcome everyone to participate!
 
+## Citing this project
+
+If you use this project in your research, please cite our NFM 2026 paper.
+
+ACM Reference Format:
+
+> Byron Cook, Remi Delmas, Zyad Hassan, Bart Jacobs, Ranjit Jhala, Rahul Kumar, Felipe R. Monteiro, Thanh Nguyen, Rebecca Rumbul, Michael Tautschnig, Celina Val, and Carolyn Zech. 2026. Verifying the Rust Standard Library. In *NASA Formal Methods: 18th International Symposium, NFM 2026, Los Angeles, CA, USA, May 5–7, 2026, Proceedings*. Springer-Verlag, Berlin, Heidelberg, 415–435. <https://doi.org/10.1007/978-3-032-28079-4_19>
+
+BibTeX:
+
+```bibtex
+@inproceedings{10.1007/978-3-032-28079-4_19,
+  author    = {Cook, Byron and Delmas, Remi and Hassan, Zyad and Jacobs, Bart and
+               Jhala, Ranjit and Kumar, Rahul and Monteiro, Felipe R. and
+               Nguyen, Thanh and Rumbul, Rebecca and Tautschnig, Michael and
+               Val, Celina and Zech, Carolyn},
+  title     = {Verifying the Rust Standard Library},
+  year      = {2026},
+  isbn      = {978-3-032-28078-7},
+  publisher = {Springer-Verlag},
+  address   = {Berlin, Heidelberg},
+  url       = {https://doi.org/10.1007/978-3-032-28079-4_19},
+  doi       = {10.1007/978-3-032-28079-4_19},
+  booktitle = {NASA Formal Methods: 18th International Symposium, NFM 2026, Los Angeles, CA, USA, May 5–7, 2026, Proceedings},
+  pages     = {415–435},
+  numpages  = {21},
+  location  = {Los Angeles, CA, USA}
+}
+```
+
+The same citation is available in machine-readable form in [CITATION.cff](CITATION.cff),
+which powers GitHub's *Cite this repository* button.
+
 ## Contact
 
 For questions, suggestions or feedback, feel free to open an [issue here](https://github.com/model-checking/verify-rust-std/issues).
@@ -71,6 +106,25 @@ 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](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.
 
+### GOTO Transcoder (ESBMC)
+The [goto-transcoder](https://github.com/rafaelsamenezes/goto-transcoder) is distributed under the terms of the MIT license.
+See [LICENSE](https://github.com/rafaelsamenezes/goto-transcoder/blob/main/LICENSE) for details.
+
+[ESBMC](https://github.com/esbmc/esbmc) is distributed under the terms of the Apache License (Version 2.0).
+See [COPYING](https://github.com/esbmc/esbmc/blob/master/COPYING) for details.
+
+### Flux
+[Flux](https://github.com/flux-rs/flux) is distributed under the terms of the MIT license.
+See [LICENSE](https://github.com/flux-rs/flux/blob/main/LICENSE) for details.
+
+### VeriFast
+[VeriFast](https://github.com/verifast/verifast) is distributed under the terms of the MIT license.
+See [LICENSE.md](https://github.com/verifast/verifast/blob/master/LICENSE.md) for details.
+
+### KMIR
+[KMIR](https://github.com/runtimeverification/mir-semantics) is distributed under the terms of the BSD-3-Clause license.
+See [LICENSE](https://github.com/runtimeverification/mir-semantics/blob/master/LICENSE) 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.
 

doc/src/SUMMARY.md

@@ -42,3 +42,5 @@
   - [25: Verify the safety of `VecDeque` functions](./challenges/0025-vecdeque.md)
   - [26: Verify reference-counted Cell implementation](./challenges/0026-rc.md)
   - [27: Verify atomically reference-counted Cell implementation](./challenges/0027-arc.md)
+  - [28: Verify float to decimal conversion module](./challenges/0028-flt2dec.md)
+  - [29: Safety of `boxed`](./challenges/0029-boxed.md)

doc/src/challenge_template.md

@@ -4,7 +4,6 @@
 - **Solution:** *Option field to point to the PR that solved this challenge.*
 - **Tracking Issue:** *Link to issue*
 - **Start date:** *YYYY/MM/DD*
-- **End date:** *YYYY/MM/DD*
 - **Reward:** *TBD*[^reward]
 
 -------------------

doc/src/challenges/0001-core-transmutation.md

@@ -3,7 +3,6 @@
 - **Status:** Resolved
 - **Tracking Issue:** [#19](https://github.com/model-checking/verify-rust-std/issues/19)
 - **Start date:** *2024/06/12*
-- **End date:** *2025/04/10*
 - **Reward:** *10000 USD*
 - **Contributors**: [Alex Le Blanc](https://github.com/AlexLB99), [Patrick Lam](https://github.com/patricklam)
 

doc/src/challenges/0002-intrinsics-memory.md

@@ -3,7 +3,6 @@
 - **Status:** Open
 - **Tracking Issue:** [#16](https://github.com/model-checking/verify-rust-std/issues/16)
 - **Start date:** *2024/06/12*
-- **End date:** *2025/04/10*
 - **Reward:** *10000 USD*
 
 -------------------

doc/src/challenges/0003-pointer-arithmentic.md

@@ -3,7 +3,6 @@
 - **Status:** Resolved
 - **Tracking Issue:** [#76](https://github.com/model-checking/verify-rust-std/issues/76)
 - **Start date:** *2024/06/24*
-- **End date:** *2024/12/11*
 - **Reward:** *N/A*
 - **Contributors:** [Surya Togaru](https://github.com/stogaru), [Yifei Wang](https://github.com/xsxszab), [Szu-Yu Lee](https://github.com/szlee118), [Mayuresh Joshi](https://github.com/MayureshJoshi25)
 

doc/src/challenges/0004-btree-node.md

@@ -3,7 +3,6 @@
 - **Status:** Open
 - **Tracking Issue:** [#77](https://github.com/model-checking/verify-rust-std/issues/77)
 - **Start date:** *2024/07/01*
-- **End date:** *2025/04/10*
 - **Reward:** *10,000 USD*
 
 -------------------

doc/src/challenges/0005-linked-list.md

@@ -3,7 +3,6 @@
 - **Status:** Resolved
 - **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29)
 - **Start date:** *2024/07/01*
-- **End date:** *2025/08/12*
 - **Reward:** *20000 USD*
 - **Contributors:** [Bart Jacobs](https://github.com/btj)
 

doc/src/challenges/0006-nonnull.md

@@ -3,7 +3,6 @@
 - **Status:** Resolved
 - **Tracking Issue:** [#53](https://github.com/model-checking/verify-rust-std/issues/53)
 - **Start date:** *2024/08/16*
-- **End date:** *2025/04/10*
 - **Reward:** *N/A*
 - **Contributors**: [Quinyuan Wu](https://github.com/QinyuanWu), [Daniel Tu](https://github.com/danielhumanmod), [Dhvani Kapadia](https://github.com/Dhvani-Kapadia) and [Jiun Chi Yang](https://github.com/Jimmycreative)
 -------------------

doc/src/challenges/0007-atomic-types.md

@@ -3,7 +3,6 @@
 - **Status:** Open
 - **Tracking Issue:** [#83](https://github.com/model-checking/verify-rust-std/issues/83)
 - **Start date:** *2024/10/30*
-- **End date:** *2025/04/10*
 - **Reward:** *10,000 USD*
 
 -------------------

doc/src/challenges/0008-smallsort.md

@@ -3,7 +3,6 @@
 - **Status:** Open
 - **Tracking Issue:** [#56](https://github.com/model-checking/verify-rust-std/issues/56)
 - **Start date:** *2024/08/17*
-- **End date:** *2025/04/10*
 - **Reward:** *10,000 USD*
 
 -------------------

doc/src/challenges/0009-duration.md

@@ -3,7 +3,6 @@
 - **Status:** Resolved
 - **Tracking Issue:** [#72](https://github.com/model-checking/verify-rust-std/issues/72)
 - **Start date:** *2024/08/20*
-- **End date:** *2024/12/10*
 - **Reward:** *N/A*
 - **Contributors**: [Samuel Thomas](https://github.com/sgpthomas) and [Cole Vick](https://github.com/cvick32)
 -------------------

doc/src/challenges/0010-string.md

@@ -3,7 +3,6 @@
 - **Status:** Open
 - **Tracking Issue:** [#61](https://github.com/model-checking/verify-rust-std/issues/61)
 - **Start date:** *2024/08/19*
-- **End date:** *2025/04/10*
 - **Reward:** *10000 USD*
 
 -------------------

doc/src/challenges/0011-floats-ints.md

@@ -4,7 +4,6 @@
 - **Status:** Resolved
 - **Tracking Issue:** [#59](https://github.com/model-checking/verify-rust-std/issues/59)
 - **Start date:** *2024/08/20*
-- **End date:** *2024/12/04*
 - **Reward:** *N/A*
 - **Contributors**: [Rajath M Kotyal](https://github.com/rajathkotyal), [Yen-Yun Wu](https://github.com/Yenyun035), [Lanfei Ma](https://github.com/lanfeima), [Junfeng Jin](https://github.com/MWDZ)
 

doc/src/challenges/0012-nonzero.md

@@ -3,7 +3,6 @@
 - **Status:** Open
 - **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*
 
 -------------------

doc/src/challenges/0013-cstr.md

@@ -4,7 +4,6 @@
 - **Solution:**
 - **Tracking Issue:** [#150](https://github.com/model-checking/verify-rust-std/issues/150)
 - **Start date:** *2024/11/04*
-- **End date:** *2025/04/10*
 - **Reward:** *10000 USD*
 
 -------------------

doc/src/challenges/0014-convert-num.md

@@ -3,8 +3,7 @@
 - **Status:** Resolved
 - **Tracking Issue:** [#220](https://github.com/model-checking/verify-rust-std/issues/220)
 - **Start date:** 2024/12/15
-- **End date:** 2025/2/28
-- **Prize:** *TBD*
+- **Prize:** *N/A*
 - **Contributors**: [Shoyu Vanilla](https://github.com/ShoyuVanilla)
 -------------------
 

doc/src/challenges/0015-intrinsics-simd.md

@@ -1,11 +1,11 @@
 # Challenge 15: Contracts and Tests for SIMD Intrinsics
 
-- **Status:** Open
-- **Solution:** 
+- **Status:** Resolved
+- **Solution:** [#423](https://github.com/model-checking/verify-rust-std/pull/423)
 - **Tracking Issue:** [#173](https://github.com/model-checking/verify-rust-std/issues/173)
 - **Start date:** 2025/02/01
-- **End date:** 2025/08/01
 - **Reward:** *20000 USD*
+- **Contributors:** [Karthik Bhargavan](https://github.com/karthikbhargavan), [Maxime Buyse](https://github.com/maximebuyse)
 
 -------------------
 

doc/src/challenges/0016-iter.md

@@ -3,7 +3,6 @@
 - **Status:** Open
 - **Tracking Issue:** [#280](https://github.com/model-checking/verify-rust-std/issues/280)
 - **Start date:** *2025-03-07*
-- **End date:** *2025-10-17*
 - **Reward:** *10,000 USD*
 
 -------------------

doc/src/challenges/0017-slice.md

@@ -3,7 +3,6 @@
 - **Status:** Open
 - **Tracking Issue:** [#281](https://github.com/model-checking/verify-rust-std/issues/281)
 - **Start date:** *2025-03-07*
-- **End date:** *2025-10-17*
 - **Reward:** *10000 USD*
 
 -------------------

doc/src/challenges/0018-slice-iter.md

@@ -3,7 +3,6 @@
 - **Status:** Open
 - **Tracking Issue:** [#282](https://github.com/model-checking/verify-rust-std/issues/282)
 - **Start date:** *2025-03-07*
-- **End date:** *2025-10-17*
 - **Reward:** *10000 USD*
 
 -------------------

doc/src/challenges/0019-rawvec.md

@@ -3,7 +3,6 @@
 - **Status:** Resolved
 - **Tracking Issue:** [#283](https://github.com/model-checking/verify-rust-std/issues/283)
 - **Start date:** *2025-03-07*
-- **End date:** *2025-08-12*
 - **Reward:** *10000 USD*
 - **Contributors:** [Bart Jacobs](https://github.com/btj)
 

doc/src/challenges/0020-str-pattern-pt1.md

@@ -3,7 +3,6 @@
 - **Status:** Open
 - **Tracking Issue:** [#277](https://github.com/model-checking/verify-rust-std/issues/277)
 - **Start date:** *2025-03-07*
-- **End date:** *2025-10-17*
 - **Reward:** *25000 USD*
 
 -------------------

doc/src/challenges/0021-str-pattern-pt2.md

@@ -3,7 +3,6 @@
 - **Status:** Open
 - **Tracking Issue:** [#278](https://github.com/model-checking/verify-rust-std/issues/278)
 - **Start date:** *2025-03-07*
-- **End date:** *2025-10-17*
 - **Reward:** *25000 USD*
 
 -------------------

doc/src/challenges/0022-str-iter.md

@@ -3,7 +3,6 @@
 - **Status:** Open
 - **Tracking Issue:** [#279](https://github.com/model-checking/verify-rust-std/issues/279)
 - **Start date:** *2025-03-07*
-- **End date:** *2025-10-17*
 - **Reward:** *10000 USD*
 
 -------------------

doc/src/challenges/0023-vec-pt1.md

@@ -3,7 +3,6 @@
 - **Status:** Open
 - **Tracking Issue:** [#284](https://github.com/model-checking/verify-rust-std/issues/284)
 - **Start date:** *2025-03-07*
-- **End date:** *2025-10-17*
 - **Reward:** *15000 USD*
 
 -------------------

doc/src/challenges/0024-vec-pt2.md

@@ -3,7 +3,6 @@
 - **Status:** Open
 - **Tracking Issue:** [#285](https://github.com/model-checking/verify-rust-std/issues/285)
 - **Start date:** *2025/03/07*
-- **End date:** *2025/10/17*
 - **Reward:** *15000 USD*
 
 -------------------

doc/src/challenges/0025-vecdeque.md

@@ -3,7 +3,6 @@
 - **Status:** Open
 - **Tracking Issue:** [#286](https://github.com/model-checking/verify-rust-std/issues/286)
 - **Start date:** *2025-03-07*
-- **End date:** *2025-10-17*
 - **Reward:** *10000 USD*
 
 -------------------

doc/src/challenges/0026-rc.md

@@ -4,7 +4,6 @@
 - **Solution:** *Option field to point to the PR that solved this challenge.*
 - **Tracking Issue:** [#382](https://github.com/model-checking/verify-rust-std/issues/382)
 - **Start date:** *2025/06/01*
-- **End date:** *2025/12/31*
 - **Reward:** *10,000 USD*
 
 -------------------