From 9e29edf8c6cf6b1b91f2af1ba89a0ece44aa0daf Mon Sep 17 00:00:00 2001
From: "Felipe R. Monteiro" <felisous@amazon.com>
Date: Tue, 4 Aug 2026 14:33:29 -0400
Subject: [PATCH 1/5] Remove end dates from challenges

Challenges no longer have a fixed end date. Contributors are welcome to
tackle any open challenge regardless of the dates that were previously
listed, many of which had already passed.

Drops the "End date" field from all 29 existing challenge documents and
from the challenge template so that new challenges are not created with
one.

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>
---
 doc/src/challenge_template.md                  | 1 -
 doc/src/challenges/0001-core-transmutation.md  | 1 -
 doc/src/challenges/0002-intrinsics-memory.md   | 1 -
 doc/src/challenges/0003-pointer-arithmentic.md | 1 -
 doc/src/challenges/0004-btree-node.md          | 1 -
 doc/src/challenges/0005-linked-list.md         | 1 -
 doc/src/challenges/0006-nonnull.md             | 1 -
 doc/src/challenges/0007-atomic-types.md        | 1 -
 doc/src/challenges/0008-smallsort.md           | 1 -
 doc/src/challenges/0009-duration.md            | 1 -
 doc/src/challenges/0010-string.md              | 1 -
 doc/src/challenges/0011-floats-ints.md         | 1 -
 doc/src/challenges/0012-nonzero.md             | 1 -
 doc/src/challenges/0013-cstr.md                | 1 -
 doc/src/challenges/0014-convert-num.md         | 1 -
 doc/src/challenges/0015-intrinsics-simd.md     | 1 -
 doc/src/challenges/0016-iter.md                | 1 -
 doc/src/challenges/0017-slice.md               | 1 -
 doc/src/challenges/0018-slice-iter.md          | 1 -
 doc/src/challenges/0019-rawvec.md              | 1 -
 doc/src/challenges/0020-str-pattern-pt1.md     | 1 -
 doc/src/challenges/0021-str-pattern-pt2.md     | 1 -
 doc/src/challenges/0022-str-iter.md            | 1 -
 doc/src/challenges/0023-vec-pt1.md             | 1 -
 doc/src/challenges/0024-vec-pt2.md             | 1 -
 doc/src/challenges/0025-vecdeque.md            | 1 -
 doc/src/challenges/0026-rc.md                  | 1 -
 doc/src/challenges/0027-arc.md                 | 1 -
 doc/src/challenges/0028-flt2dec.md             | 1 -
 doc/src/challenges/0029-boxed.md               | 1 -
 30 files changed, 30 deletions(-)

diff --git a/doc/src/challenge_template.md b/doc/src/challenge_template.md
index a39fad01050f1..0c59a6b0af0be 100644
--- a/doc/src/challenge_template.md
+++ b/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]
 
 -------------------
diff --git a/doc/src/challenges/0001-core-transmutation.md b/doc/src/challenges/0001-core-transmutation.md
index 029a627f06289..b384aa5f5fbbb 100644
--- a/doc/src/challenges/0001-core-transmutation.md
+++ b/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)
 
diff --git a/doc/src/challenges/0002-intrinsics-memory.md b/doc/src/challenges/0002-intrinsics-memory.md
index 021c52d1ac018..2b1dd4d1f5930 100644
--- a/doc/src/challenges/0002-intrinsics-memory.md
+++ b/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*
 
 -------------------
diff --git a/doc/src/challenges/0003-pointer-arithmentic.md b/doc/src/challenges/0003-pointer-arithmentic.md
index 65fb3074cf487..c8ede475aab44 100644
--- a/doc/src/challenges/0003-pointer-arithmentic.md
+++ b/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)
 
diff --git a/doc/src/challenges/0004-btree-node.md b/doc/src/challenges/0004-btree-node.md
index 838d9199b400b..907afbe71c22d 100644
--- a/doc/src/challenges/0004-btree-node.md
+++ b/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*
 
 -------------------
diff --git a/doc/src/challenges/0005-linked-list.md b/doc/src/challenges/0005-linked-list.md
index 1f635b72accf7..4a5debc25308b 100644
--- a/doc/src/challenges/0005-linked-list.md
+++ b/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)
 
diff --git a/doc/src/challenges/0006-nonnull.md b/doc/src/challenges/0006-nonnull.md
index 4b1b73b75ccf5..0218aaeb9199d 100644
--- a/doc/src/challenges/0006-nonnull.md
+++ b/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)
 -------------------
diff --git a/doc/src/challenges/0007-atomic-types.md b/doc/src/challenges/0007-atomic-types.md
index 43a19f805a382..64c247ed31d08 100644
--- a/doc/src/challenges/0007-atomic-types.md
+++ b/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*
 
 -------------------
diff --git a/doc/src/challenges/0008-smallsort.md b/doc/src/challenges/0008-smallsort.md
index ea4e90caa94dc..55f0552c6762b 100644
--- a/doc/src/challenges/0008-smallsort.md
+++ b/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*
 
 -------------------
diff --git a/doc/src/challenges/0009-duration.md b/doc/src/challenges/0009-duration.md
index 4d44f20376cc4..b30742ada4363 100644
--- a/doc/src/challenges/0009-duration.md
+++ b/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)
 -------------------
diff --git a/doc/src/challenges/0010-string.md b/doc/src/challenges/0010-string.md
index 7c392b59ec7d2..26e493f8dfb8c 100644
--- a/doc/src/challenges/0010-string.md
+++ b/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*
 
 -------------------
diff --git a/doc/src/challenges/0011-floats-ints.md b/doc/src/challenges/0011-floats-ints.md
index 2d80453e25c3c..95760e976c43a 100644
--- a/doc/src/challenges/0011-floats-ints.md
+++ b/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)
 
diff --git a/doc/src/challenges/0012-nonzero.md b/doc/src/challenges/0012-nonzero.md
index 2c48386dfdb3c..85326244572cb 100644
--- a/doc/src/challenges/0012-nonzero.md
+++ b/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*
 
 -------------------
diff --git a/doc/src/challenges/0013-cstr.md b/doc/src/challenges/0013-cstr.md
index eb6e28d59b724..1a112713ef315 100644
--- a/doc/src/challenges/0013-cstr.md
+++ b/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*
 
 -------------------
diff --git a/doc/src/challenges/0014-convert-num.md b/doc/src/challenges/0014-convert-num.md
index ec784d09dadd1..6c398bb74fc8e 100644
--- a/doc/src/challenges/0014-convert-num.md
+++ b/doc/src/challenges/0014-convert-num.md
@@ -3,7 +3,6 @@
 - **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*
 - **Contributors**: [Shoyu Vanilla](https://github.com/ShoyuVanilla)
 -------------------
diff --git a/doc/src/challenges/0015-intrinsics-simd.md b/doc/src/challenges/0015-intrinsics-simd.md
index 32ea982e08070..a927b1a0bc045 100644
--- a/doc/src/challenges/0015-intrinsics-simd.md
+++ b/doc/src/challenges/0015-intrinsics-simd.md
@@ -4,7 +4,6 @@
 - **Solution:** 
 - **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*
 
 -------------------
diff --git a/doc/src/challenges/0016-iter.md b/doc/src/challenges/0016-iter.md
index b85b9badc70a4..89f55669c35b0 100644
--- a/doc/src/challenges/0016-iter.md
+++ b/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*
 
 -------------------
diff --git a/doc/src/challenges/0017-slice.md b/doc/src/challenges/0017-slice.md
index 4ecda06a3ec47..76f4dd8b02039 100644
--- a/doc/src/challenges/0017-slice.md
+++ b/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*
 
 -------------------
diff --git a/doc/src/challenges/0018-slice-iter.md b/doc/src/challenges/0018-slice-iter.md
index 6b59bae162c53..74c02df42d9b9 100644
--- a/doc/src/challenges/0018-slice-iter.md
+++ b/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*
 
 -------------------
diff --git a/doc/src/challenges/0019-rawvec.md b/doc/src/challenges/0019-rawvec.md
index 133339ebe899c..08bd4afa9de27 100644
--- a/doc/src/challenges/0019-rawvec.md
+++ b/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)
 
diff --git a/doc/src/challenges/0020-str-pattern-pt1.md b/doc/src/challenges/0020-str-pattern-pt1.md
index 12d6066fe77b6..a551ef74bcf90 100644
--- a/doc/src/challenges/0020-str-pattern-pt1.md
+++ b/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*
 
 -------------------
diff --git a/doc/src/challenges/0021-str-pattern-pt2.md b/doc/src/challenges/0021-str-pattern-pt2.md
index e8a6bb6ed7bf0..bd209eb072a9c 100644
--- a/doc/src/challenges/0021-str-pattern-pt2.md
+++ b/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*
 
 -------------------
diff --git a/doc/src/challenges/0022-str-iter.md b/doc/src/challenges/0022-str-iter.md
index 808bfe97ca453..8b01d82b6e60e 100644
--- a/doc/src/challenges/0022-str-iter.md
+++ b/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*
 
 -------------------
diff --git a/doc/src/challenges/0023-vec-pt1.md b/doc/src/challenges/0023-vec-pt1.md
index 08259fefbf9de..88bace6ed4e36 100644
--- a/doc/src/challenges/0023-vec-pt1.md
+++ b/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*
 
 -------------------
diff --git a/doc/src/challenges/0024-vec-pt2.md b/doc/src/challenges/0024-vec-pt2.md
index c3b1ac84cf9cf..ddb49a6ff851c 100644
--- a/doc/src/challenges/0024-vec-pt2.md
+++ b/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*
 
 -------------------
diff --git a/doc/src/challenges/0025-vecdeque.md b/doc/src/challenges/0025-vecdeque.md
index 5185dcc031bbf..79d6fc517c6f7 100644
--- a/doc/src/challenges/0025-vecdeque.md
+++ b/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*
 
 -------------------
diff --git a/doc/src/challenges/0026-rc.md b/doc/src/challenges/0026-rc.md
index b5fc0a329243e..08a1f83f7511b 100644
--- a/doc/src/challenges/0026-rc.md
+++ b/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*
 
 -------------------
diff --git a/doc/src/challenges/0027-arc.md b/doc/src/challenges/0027-arc.md
index 4081356ef9e8a..9edb3f55a13fd 100644
--- a/doc/src/challenges/0027-arc.md
+++ b/doc/src/challenges/0027-arc.md
@@ -4,7 +4,6 @@
 - **Solution:** *Option field to point to the PR that solved this challenge.*
 - **Tracking Issue:** [#383](https://github.com/model-checking/verify-rust-std/issues/383)
 - **Start date:** *2025/06/01*
-- **End date:** *2025/12/31*
 - **Reward:** *10,000 USD*
 
 -------------------
diff --git a/doc/src/challenges/0028-flt2dec.md b/doc/src/challenges/0028-flt2dec.md
index a5a52a25b503d..730d18a854898 100644
--- a/doc/src/challenges/0028-flt2dec.md
+++ b/doc/src/challenges/0028-flt2dec.md
@@ -4,7 +4,6 @@
 - **Solution:** *Option field to point to the PR that solved this challenge.*
 - **Tracking Issue:** [#524](https://github.com/model-checking/verify-rust-std/issues/524)
 - **Start date:** *2026/01/01*
-- **End date:** *2026/08/31*
 - **Reward:** *5,000 USD*
 
 -------------------
diff --git a/doc/src/challenges/0029-boxed.md b/doc/src/challenges/0029-boxed.md
index 6e4dcf0531127..7559e49008069 100644
--- a/doc/src/challenges/0029-boxed.md
+++ b/doc/src/challenges/0029-boxed.md
@@ -4,7 +4,6 @@
 - **Solution:** *Option field to point to the PR that solved this challenge.*
 - **Tracking Issue:** [#526](https://github.com/model-checking/verify-rust-std/issues/526)
 - **Start date:** *2026/01/01*
-- **End date:** *2026/12/31*
 - **Reward:** *15,000 USD*
 
 -------------------

From 74e6ae26f70ebf18d3fbfb273946708203b31a5c Mon Sep 17 00:00:00 2001
From: Felipe Monteiro <felisous@amazon.com>
Date: Fri, 21 Aug 2026 20:17:25 +0000
Subject: [PATCH 2/5] Mark challenge 15 resolved; update README licenses,
 citation, and challenge 14 reward

- Mark Challenge 15 (SIMD intrinsics) as Resolved, solved by #423
- README: challenge 14 reward TBD -> N/A; challenge 15 Open -> Resolved
- Add license info for GOTO Transcoder (ESBMC), Flux, and VeriFast
- Add NFM 2026 paper citation section and CITATION.cff
---
 CITATION.cff                               | 73 ++++++++++++++++++++++
 README.md                                  | 52 ++++++++++++++-
 doc/src/challenges/0015-intrinsics-simd.md |  5 +-
 3 files changed, 126 insertions(+), 4 deletions(-)
 create mode 100644 CITATION.cff

diff --git a/CITATION.cff b/CITATION.cff
new file mode 100644
index 0000000000000..7bc59c98d2b78
--- /dev/null
+++ b/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
diff --git a/README.md b/README.md
index 5bdeac61207db..1638cccc0ee74 100644
--- a/README.md
+++ b/README.md
@@ -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 | |
@@ -57,6 +57,39 @@ See [our book](https://model-checking.github.io/verify-rust-std/intro.html) for
 
 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 +104,21 @@ 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 based on CBMC: CBMC is distributed under the terms of the BSD 4-clause license, and the ESBMC modifications are 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.
+
 ### 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.
 
diff --git a/doc/src/challenges/0015-intrinsics-simd.md b/doc/src/challenges/0015-intrinsics-simd.md
index a927b1a0bc045..0b7781b814a15 100644
--- a/doc/src/challenges/0015-intrinsics-simd.md
+++ b/doc/src/challenges/0015-intrinsics-simd.md
@@ -1,10 +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
 - **Reward:** *20000 USD*
+- **Contributors:** [Karthik Bhargavan](https://github.com/karthikbhargavan), [Maxime Buyse](https://github.com/maximebuyse)
 
 -------------------
 

From af7ded8a92b977d4abda3d1e615ba61fddec4132 Mon Sep 17 00:00:00 2001
From: Felipe Monteiro <felisous@amazon.com>
Date: Fri, 21 Aug 2026 20:19:59 +0000
Subject: [PATCH 3/5] Fix doc inconsistencies: list challenges 28/29, align
 challenge 14 reward

- Add challenges 28 (flt2dec) and 29 (boxed) to README table and book SUMMARY;
  their docs existed but were not linked anywhere (also absent on main)
- Challenge 14 doc: Prize TBD -> N/A to match README
---
 README.md                              | 2 ++
 doc/src/SUMMARY.md                     | 2 ++
 doc/src/challenges/0014-convert-num.md | 2 +-
 3 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 1638cccc0ee74..583bec82c3404 100644
--- a/README.md
+++ b/README.md
@@ -52,6 +52,8 @@ 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.
 
diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md
index cb6d9337dd32d..ab51c03ccf1f6 100644
--- a/doc/src/SUMMARY.md
+++ b/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)
diff --git a/doc/src/challenges/0014-convert-num.md b/doc/src/challenges/0014-convert-num.md
index 6c398bb74fc8e..6e5a1ee880d25 100644
--- a/doc/src/challenges/0014-convert-num.md
+++ b/doc/src/challenges/0014-convert-num.md
@@ -3,7 +3,7 @@
 - **Status:** Resolved
 - **Tracking Issue:** [#220](https://github.com/model-checking/verify-rust-std/issues/220)
 - **Start date:** 2024/12/15
-- **Prize:** *TBD*
+- **Prize:** *N/A*
 - **Contributors**: [Shoyu Vanilla](https://github.com/ShoyuVanilla)
 -------------------
 

From 1f2bad8841bc3b40c2b0fe0dc6d88b1aec2d7ef3 Mon Sep 17 00:00:00 2001
From: Felipe Monteiro <felisous@amazon.com>
Date: Fri, 21 Aug 2026 20:31:24 +0000
Subject: [PATCH 4/5] Simplify ESBMC license note; drop CBMC lineage reference

Signed-off-by: Felipe Monteiro <felisous@amazon.com>
---
 README.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 583bec82c3404..7845051b7b1e6 100644
--- a/README.md
+++ b/README.md
@@ -110,7 +110,7 @@ See [LICENSE-APACHE](https://github.com/model-checking/kani/blob/main/LICENSE-AP
 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 based on CBMC: CBMC is distributed under the terms of the BSD 4-clause license, and the ESBMC modifications are distributed under the terms of the Apache License (Version 2.0).
+[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

From f0d409dde5f2ce1b9a0414702543bc2a8ec01a23 Mon Sep 17 00:00:00 2001
From: Felipe Monteiro <felisous@amazon.com>
Date: Fri, 21 Aug 2026 20:37:20 +0000
Subject: [PATCH 5/5] Add KMIR to accepted tools list and license section

Signed-off-by: Felipe Monteiro <felisous@amazon.com>
---
 README.md | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 7845051b7b1e6..47d5dafbc1485 100644
--- a/README.md
+++ b/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
@@ -121,6 +121,10 @@ See [LICENSE](https://github.com/flux-rs/flux/blob/main/LICENSE) for details.
 [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.