diff --git a/library/core/src/slice/iter.rs b/library/core/src/slice/iter.rs
index b6de37033cc47..903f91398ea79 100644
--- a/library/core/src/slice/iter.rs
+++ b/library/core/src/slice/iter.rs
@@ -3121,7 +3121,11 @@ where
             let mut len = 1;
             let mut iter = self.slice.windows(2);
             while let Some([l, r]) = iter.next() {
-                if (self.predicate)(l, r) { len += 1 } else { break }
+                if (self.predicate)(l, r) {
+                    len += 1
+                } else {
+                    break;
+                }
             }
             let (head, tail) = self.slice.split_at(len);
             self.slice = tail;
@@ -3153,7 +3157,11 @@ where
             let mut len = 1;
             let mut iter = self.slice.windows(2);
             while let Some([l, r]) = iter.next_back() {
-                if (self.predicate)(l, r) { len += 1 } else { break }
+                if (self.predicate)(l, r) {
+                    len += 1
+                } else {
+                    break;
+                }
             }
             let (head, tail) = self.slice.split_at(self.slice.len() - len);
             self.slice = head;
@@ -3215,7 +3223,11 @@ where
             let mut len = 1;
             let mut iter = self.slice.windows(2);
             while let Some([l, r]) = iter.next() {
-                if (self.predicate)(l, r) { len += 1 } else { break }
+                if (self.predicate)(l, r) {
+                    len += 1
+                } else {
+                    break;
+                }
             }
             let slice = mem::take(&mut self.slice);
             let (head, tail) = slice.split_at_mut(len);
@@ -3248,7 +3260,11 @@ where
             let mut len = 1;
             let mut iter = self.slice.windows(2);
             while let Some([l, r]) = iter.next_back() {
-                if (self.predicate)(l, r) { len += 1 } else { break }
+                if (self.predicate)(l, r) {
+                    len += 1
+                } else {
+                    break;
+                }
             }
             let slice = mem::take(&mut self.slice);
             let (head, tail) = slice.split_at_mut(slice.len() - len);
@@ -3399,6 +3415,42 @@ mod verify {
                 check_safe_abstraction!(check_clone, $ty, |iter: &mut Iter<'_, $ty>| {
                     kani::assert(iter.clone().is_safe(), "Clone is safe");
                 });
+
+                // Part 1 macro functions: last, fold, for_each, position, rposition
+                #[kani::proof]
+                fn check_last() {
+                    let array: [$ty; MAX_LEN] = kani::any();
+                    let iter = any_iter::<$ty>(&array);
+                    let _ = iter.last();
+                }
+
+                #[kani::proof]
+                fn check_fold() {
+                    let array: [$ty; MAX_LEN] = kani::any();
+                    let iter = any_iter::<$ty>(&array);
+                    let _ = iter.fold(0usize, |acc, _| acc.wrapping_add(1));
+                }
+
+                #[kani::proof]
+                fn check_for_each() {
+                    let array: [$ty; MAX_LEN] = kani::any();
+                    let iter = any_iter::<$ty>(&array);
+                    iter.for_each(|_| {});
+                }
+
+                #[kani::proof]
+                fn check_position() {
+                    let array: [$ty; MAX_LEN] = kani::any();
+                    let mut iter = any_iter::<$ty>(&array);
+                    let _ = iter.position(|_| kani::any());
+                }
+
+                #[kani::proof]
+                fn check_rposition() {
+                    let array: [$ty; MAX_LEN] = kani::any();
+                    let mut iter = any_iter::<$ty>(&array);
+                    let _ = iter.rposition(|_| kani::any());
+                }
             }
         };
     }
@@ -3408,4 +3460,631 @@ mod verify {
     check_iter_with_ty!(verify_u8, u8, u32::MAX as usize);
     check_iter_with_ty!(verify_char, char, 50);
     check_iter_with_ty!(verify_tup, (char, u8), 50);
+
+    // --- IterMut harnesses ---
+
+    fn any_mut_slice<T>(orig_slice: &mut [T]) -> &mut [T] {
+        if kani::any() {
+            let last = kani::any_where(|idx: &usize| *idx <= orig_slice.len());
+            let first = kani::any_where(|idx: &usize| *idx <= last);
+            &mut orig_slice[first..last]
+        } else {
+            let ptr = kani::any_where::<usize, _>(|val| *val != 0) as *mut T;
+            kani::assume(ptr.is_aligned());
+            unsafe { crate::slice::from_raw_parts_mut(ptr, 0) }
+        }
+    }
+
+    fn any_iter_mut<'a, T>(orig_slice: &'a mut [T]) -> IterMut<'a, T> {
+        let slice = any_mut_slice(orig_slice);
+        IterMut::new(slice)
+    }
+
+    macro_rules! check_iter_mut_with_ty {
+        ($module:ident, $ty:ty, $max:expr) => {
+            mod $module {
+                use super::*;
+                const MAX_LEN: usize = $max;
+
+                #[kani::proof]
+                fn check_new_iter_mut() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_mut_slice::<$ty>(&mut array);
+                    let iter = IterMut::new(slice);
+                    kani::assert(iter.is_safe(), "IterMut is safe");
+                }
+
+                #[kani::proof]
+                fn check_into_slice() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let iter = any_iter_mut::<$ty>(&mut array);
+                    let _ = iter.into_slice();
+                }
+
+                #[kani::proof]
+                fn check_as_mut_slice() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let mut iter = any_iter_mut::<$ty>(&mut array);
+                    let _ = iter.as_mut_slice();
+                    kani::assert(iter.is_safe(), "IterMut is safe");
+                }
+
+                #[kani::proof]
+                fn check_next() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let mut iter = any_iter_mut::<$ty>(&mut array);
+                    let _ = iter.next();
+                    kani::assert(iter.is_safe(), "IterMut is safe");
+                }
+
+                #[kani::proof]
+                fn check_next_back() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let mut iter = any_iter_mut::<$ty>(&mut array);
+                    let _ = iter.next_back();
+                    kani::assert(iter.is_safe(), "IterMut is safe");
+                }
+
+                #[kani::proof]
+                fn check_nth() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let mut iter = any_iter_mut::<$ty>(&mut array);
+                    let _ = iter.nth(kani::any());
+                    kani::assert(iter.is_safe(), "IterMut is safe");
+                }
+
+                #[kani::proof]
+                fn check_nth_back() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let mut iter = any_iter_mut::<$ty>(&mut array);
+                    let _ = iter.nth_back(kani::any());
+                    kani::assert(iter.is_safe(), "IterMut is safe");
+                }
+
+                #[kani::proof]
+                fn check_advance_by() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let mut iter = any_iter_mut::<$ty>(&mut array);
+                    let _ = iter.advance_by(kani::any());
+                    kani::assert(iter.is_safe(), "IterMut is safe");
+                }
+
+                #[kani::proof]
+                fn check_advance_back_by() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let mut iter = any_iter_mut::<$ty>(&mut array);
+                    let _ = iter.advance_back_by(kani::any());
+                    kani::assert(iter.is_safe(), "IterMut is safe");
+                }
+
+                #[kani::proof]
+                fn check_len() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let iter = any_iter_mut::<$ty>(&mut array);
+                    let _ = iter.len();
+                }
+
+                #[kani::proof]
+                fn check_is_empty() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let iter = any_iter_mut::<$ty>(&mut array);
+                    let _ = iter.is_empty();
+                }
+
+                #[kani::proof]
+                fn check_size_hint() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let iter = any_iter_mut::<$ty>(&mut array);
+                    let _ = iter.size_hint();
+                }
+
+                #[kani::proof]
+                fn check_count() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let iter = any_iter_mut::<$ty>(&mut array);
+                    iter.count();
+                }
+
+                #[kani::proof]
+                fn check_last() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let iter = any_iter_mut::<$ty>(&mut array);
+                    let _ = iter.last();
+                }
+
+                #[kani::proof]
+                fn check_fold() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let iter = any_iter_mut::<$ty>(&mut array);
+                    let _ = iter.fold(0usize, |acc, _| acc.wrapping_add(1));
+                }
+
+                #[kani::proof]
+                fn check_for_each() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let iter = any_iter_mut::<$ty>(&mut array);
+                    iter.for_each(|_| {});
+                }
+
+                #[kani::proof]
+                fn check_position() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let mut iter = any_iter_mut::<$ty>(&mut array);
+                    let _ = iter.position(|_| kani::any());
+                }
+
+                #[kani::proof]
+                fn check_rposition() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let mut iter = any_iter_mut::<$ty>(&mut array);
+                    let _ = iter.rposition(|_| kani::any());
+                }
+            }
+        };
+    }
+
+    check_iter_mut_with_ty!(verify_iter_mut_unit, (), isize::MAX as usize);
+    check_iter_mut_with_ty!(verify_iter_mut_u8, u8, u32::MAX as usize);
+    check_iter_mut_with_ty!(verify_iter_mut_char, char, 50);
+    check_iter_mut_with_ty!(verify_iter_mut_tup, (char, u8), 50);
+
+    // --- Part 2: Chunk/Window iterator harnesses ---
+
+    /// Helper to create an arbitrary slice for chunk-type iterators.
+    fn any_chunk_slice<T>(orig_slice: &[T]) -> &[T] {
+        any_slice(orig_slice)
+    }
+
+    fn any_chunk_mut_slice<T>(orig_slice: &mut [T]) -> &mut [T] {
+        any_mut_slice(orig_slice)
+    }
+
+    macro_rules! check_chunks_with_ty {
+        ($module:ident, $ty:ty, $max:expr) => {
+            mod $module {
+                use super::*;
+                const MAX_LEN: usize = $max;
+
+                // --- Windows ---
+
+                #[kani::proof]
+                fn check_windows_next() {
+                    let array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_slice::<$ty>(&array);
+                    let size: usize = kani::any();
+                    kani::assume(size > 0);
+                    let mut iter = slice.windows(size);
+                    let _ = iter.next();
+                }
+
+                #[kani::proof]
+                fn check_windows_next_back() {
+                    let array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_slice::<$ty>(&array);
+                    let size: usize = kani::any();
+                    kani::assume(size > 0);
+                    let mut iter = slice.windows(size);
+                    let _ = iter.next_back();
+                }
+
+                #[kani::proof]
+                fn check_windows_get_unchecked() {
+                    let array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_slice::<$ty>(&array);
+                    let size: usize = kani::any();
+                    kani::assume(size > 0);
+                    let mut iter = slice.windows(size);
+                    let idx: usize = kani::any();
+                    kani::assume(idx < iter.len());
+                    let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+                }
+
+                // --- Chunks ---
+
+                #[kani::proof]
+                fn check_chunks_next_back() {
+                    let array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_slice::<$ty>(&array);
+                    let size: usize = kani::any();
+                    kani::assume(size > 0);
+                    let mut iter = slice.chunks(size);
+                    let _ = iter.next_back();
+                }
+
+                #[kani::proof]
+                fn check_chunks_get_unchecked() {
+                    let array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_slice::<$ty>(&array);
+                    let size: usize = kani::any();
+                    kani::assume(size > 0);
+                    let mut iter = slice.chunks(size);
+                    let idx: usize = kani::any();
+                    kani::assume(idx < iter.len());
+                    let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+                }
+
+                // --- ChunksMut ---
+
+                #[kani::proof]
+                fn check_chunks_mut_next() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_mut_slice::<$ty>(&mut array);
+                    let size: usize = kani::any();
+                    kani::assume(size > 0);
+                    let mut iter = slice.chunks_mut(size);
+                    let _ = iter.next();
+                }
+
+                #[kani::proof]
+                fn check_chunks_mut_nth() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_mut_slice::<$ty>(&mut array);
+                    let size: usize = kani::any();
+                    kani::assume(size > 0);
+                    let mut iter = slice.chunks_mut(size);
+                    let _ = iter.nth(kani::any());
+                }
+
+                #[kani::proof]
+                fn check_chunks_mut_next_back() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_mut_slice::<$ty>(&mut array);
+                    let size: usize = kani::any();
+                    kani::assume(size > 0);
+                    let mut iter = slice.chunks_mut(size);
+                    let _ = iter.next_back();
+                }
+
+                #[kani::proof]
+                fn check_chunks_mut_nth_back() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_mut_slice::<$ty>(&mut array);
+                    let size: usize = kani::any();
+                    kani::assume(size > 0);
+                    let mut iter = slice.chunks_mut(size);
+                    let _ = iter.nth_back(kani::any());
+                }
+
+                #[kani::proof]
+                fn check_chunks_mut_get_unchecked() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_mut_slice::<$ty>(&mut array);
+                    let size: usize = kani::any();
+                    kani::assume(size > 0);
+                    let mut iter = slice.chunks_mut(size);
+                    let idx: usize = kani::any();
+                    kani::assume(idx < iter.len());
+                    let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+                }
+
+                // --- ChunksExact ---
+
+                #[kani::proof]
+                fn check_chunks_exact_new() {
+                    let array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_slice::<$ty>(&array);
+                    let size: usize = kani::any();
+                    kani::assume(size > 0);
+                    let _ = slice.chunks_exact(size);
+                }
+
+                #[kani::proof]
+                fn check_chunks_exact_get_unchecked() {
+                    let array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_slice::<$ty>(&array);
+                    let size: usize = kani::any();
+                    kani::assume(size > 0);
+                    let mut iter = slice.chunks_exact(size);
+                    let idx: usize = kani::any();
+                    kani::assume(idx < iter.len());
+                    let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+                }
+
+                // --- ChunksExactMut ---
+
+                #[kani::proof]
+                fn check_chunks_exact_mut_new() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_mut_slice::<$ty>(&mut array);
+                    let size: usize = kani::any();
+                    kani::assume(size > 0);
+                    let _ = slice.chunks_exact_mut(size);
+                }
+
+                #[kani::proof]
+                fn check_chunks_exact_mut_next() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_mut_slice::<$ty>(&mut array);
+                    let size: usize = kani::any();
+                    kani::assume(size > 0);
+                    let mut iter = slice.chunks_exact_mut(size);
+                    let _ = iter.next();
+                }
+
+                #[kani::proof]
+                fn check_chunks_exact_mut_nth() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_mut_slice::<$ty>(&mut array);
+                    let size: usize = kani::any();
+                    kani::assume(size > 0);
+                    let mut iter = slice.chunks_exact_mut(size);
+                    let _ = iter.nth(kani::any());
+                }
+
+                #[kani::proof]
+                fn check_chunks_exact_mut_next_back() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_mut_slice::<$ty>(&mut array);
+                    let size: usize = kani::any();
+                    kani::assume(size > 0);
+                    let mut iter = slice.chunks_exact_mut(size);
+                    let _ = iter.next_back();
+                }
+
+                #[kani::proof]
+                fn check_chunks_exact_mut_nth_back() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_mut_slice::<$ty>(&mut array);
+                    let size: usize = kani::any();
+                    kani::assume(size > 0);
+                    let mut iter = slice.chunks_exact_mut(size);
+                    let _ = iter.nth_back(kani::any());
+                }
+
+                #[kani::proof]
+                fn check_chunks_exact_mut_get_unchecked() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_mut_slice::<$ty>(&mut array);
+                    let size: usize = kani::any();
+                    kani::assume(size > 0);
+                    let mut iter = slice.chunks_exact_mut(size);
+                    let idx: usize = kani::any();
+                    kani::assume(idx < iter.len());
+                    let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+                }
+
+                // --- RChunks ---
+
+                #[kani::proof]
+                fn check_rchunks_next() {
+                    let array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_slice::<$ty>(&array);
+                    let size: usize = kani::any();
+                    kani::assume(size > 0);
+                    let mut iter = slice.rchunks(size);
+                    let _ = iter.next();
+                }
+
+                #[kani::proof]
+                fn check_rchunks_next_back() {
+                    let array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_slice::<$ty>(&array);
+                    let size: usize = kani::any();
+                    kani::assume(size > 0);
+                    let mut iter = slice.rchunks(size);
+                    let _ = iter.next_back();
+                }
+
+                #[kani::proof]
+                fn check_rchunks_get_unchecked() {
+                    let array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_slice::<$ty>(&array);
+                    let size: usize = kani::any();
+                    kani::assume(size > 0);
+                    let mut iter = slice.rchunks(size);
+                    let idx: usize = kani::any();
+                    kani::assume(idx < iter.len());
+                    let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+                }
+
+                // --- RChunksMut ---
+
+                #[kani::proof]
+                fn check_rchunks_mut_next() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_mut_slice::<$ty>(&mut array);
+                    let size: usize = kani::any();
+                    kani::assume(size > 0);
+                    let mut iter = slice.rchunks_mut(size);
+                    let _ = iter.next();
+                }
+
+                #[kani::proof]
+                fn check_rchunks_mut_nth() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_mut_slice::<$ty>(&mut array);
+                    let size: usize = kani::any();
+                    kani::assume(size > 0);
+                    let mut iter = slice.rchunks_mut(size);
+                    let _ = iter.nth(kani::any());
+                }
+
+                #[kani::proof]
+                fn check_rchunks_mut_last() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_mut_slice::<$ty>(&mut array);
+                    let size: usize = kani::any();
+                    kani::assume(size > 0);
+                    let mut iter = slice.rchunks_mut(size);
+                    let _ = iter.last();
+                }
+
+                #[kani::proof]
+                fn check_rchunks_mut_next_back() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_mut_slice::<$ty>(&mut array);
+                    let size: usize = kani::any();
+                    kani::assume(size > 0);
+                    let mut iter = slice.rchunks_mut(size);
+                    let _ = iter.next_back();
+                }
+
+                #[kani::proof]
+                fn check_rchunks_mut_nth_back() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_mut_slice::<$ty>(&mut array);
+                    let size: usize = kani::any();
+                    kani::assume(size > 0);
+                    let mut iter = slice.rchunks_mut(size);
+                    let _ = iter.nth_back(kani::any());
+                }
+
+                #[kani::proof]
+                fn check_rchunks_mut_get_unchecked() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_mut_slice::<$ty>(&mut array);
+                    let size: usize = kani::any();
+                    kani::assume(size > 0);
+                    let mut iter = slice.rchunks_mut(size);
+                    let idx: usize = kani::any();
+                    kani::assume(idx < iter.len());
+                    let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+                }
+
+                // --- RChunksExact ---
+
+                #[kani::proof]
+                fn check_rchunks_exact_new() {
+                    let array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_slice::<$ty>(&array);
+                    let size: usize = kani::any();
+                    kani::assume(size > 0);
+                    let _ = slice.rchunks_exact(size);
+                }
+
+                #[kani::proof]
+                fn check_rchunks_exact_get_unchecked() {
+                    let array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_slice::<$ty>(&array);
+                    let size: usize = kani::any();
+                    kani::assume(size > 0);
+                    let mut iter = slice.rchunks_exact(size);
+                    let idx: usize = kani::any();
+                    kani::assume(idx < iter.len());
+                    let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+                }
+
+                // --- RChunksExactMut ---
+
+                #[kani::proof]
+                fn check_rchunks_exact_mut_new() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_mut_slice::<$ty>(&mut array);
+                    let size: usize = kani::any();
+                    kani::assume(size > 0);
+                    let _ = slice.rchunks_exact_mut(size);
+                }
+
+                #[kani::proof]
+                fn check_rchunks_exact_mut_next() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_mut_slice::<$ty>(&mut array);
+                    let size: usize = kani::any();
+                    kani::assume(size > 0);
+                    let mut iter = slice.rchunks_exact_mut(size);
+                    let _ = iter.next();
+                }
+
+                #[kani::proof]
+                fn check_rchunks_exact_mut_nth() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_mut_slice::<$ty>(&mut array);
+                    let size: usize = kani::any();
+                    kani::assume(size > 0);
+                    let mut iter = slice.rchunks_exact_mut(size);
+                    let _ = iter.nth(kani::any());
+                }
+
+                #[kani::proof]
+                fn check_rchunks_exact_mut_next_back() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_mut_slice::<$ty>(&mut array);
+                    let size: usize = kani::any();
+                    kani::assume(size > 0);
+                    let mut iter = slice.rchunks_exact_mut(size);
+                    let _ = iter.next_back();
+                }
+
+                #[kani::proof]
+                fn check_rchunks_exact_mut_nth_back() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_mut_slice::<$ty>(&mut array);
+                    let size: usize = kani::any();
+                    kani::assume(size > 0);
+                    let mut iter = slice.rchunks_exact_mut(size);
+                    let _ = iter.nth_back(kani::any());
+                }
+
+                #[kani::proof]
+                fn check_rchunks_exact_mut_get_unchecked() {
+                    let mut array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_mut_slice::<$ty>(&mut array);
+                    let size: usize = kani::any();
+                    kani::assume(size > 0);
+                    let mut iter = slice.rchunks_exact_mut(size);
+                    let idx: usize = kani::any();
+                    kani::assume(idx < iter.len());
+                    let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+                }
+
+                // --- Split ---
+
+                #[kani::proof]
+                fn check_split_next() {
+                    let array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_slice::<$ty>(&array);
+                    let mut iter = slice.split(|_| kani::any());
+                    let _ = iter.next();
+                }
+
+                #[kani::proof]
+                fn check_split_next_back() {
+                    let array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_slice::<$ty>(&array);
+                    let mut iter = slice.split(|_| kani::any());
+                    let _ = iter.next_back();
+                }
+
+                // --- ArrayWindows ---
+
+                #[kani::proof]
+                fn check_array_windows_next() {
+                    let array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_slice::<$ty>(&array);
+                    // ArrayWindows requires const generic N, use a small fixed size.
+                    let mut iter = slice.array_windows::<1>();
+                    let _ = iter.next();
+                }
+
+                #[kani::proof]
+                fn check_array_windows_nth() {
+                    let array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_slice::<$ty>(&array);
+                    let mut iter = slice.array_windows::<1>();
+                    let _ = iter.nth(kani::any());
+                }
+
+                #[kani::proof]
+                fn check_array_windows_next_back() {
+                    let array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_slice::<$ty>(&array);
+                    let mut iter = slice.array_windows::<1>();
+                    let _ = iter.next_back();
+                }
+
+                #[kani::proof]
+                fn check_array_windows_nth_back() {
+                    let array: [$ty; MAX_LEN] = kani::any();
+                    let slice = any_chunk_slice::<$ty>(&array);
+                    let mut iter = slice.array_windows::<1>();
+                    let _ = iter.nth_back(kani::any());
+                }
+            }
+        };
+    }
+
+    check_chunks_with_ty!(verify_chunks_u8, u8, 128);
+    check_chunks_with_ty!(verify_chunks_unit, (), 128);
+    check_chunks_with_ty!(verify_chunks_char, char, 50);
+    check_chunks_with_ty!(verify_chunks_tup, (char, u8), 50);
 }
diff --git a/library/core/src/slice/iter/macros.rs b/library/core/src/slice/iter/macros.rs
index a5bdbdf556f7e..347c36ad72536 100644
--- a/library/core/src/slice/iter/macros.rs
+++ b/library/core/src/slice/iter/macros.rs
@@ -245,32 +245,51 @@ macro_rules! iterator {
                 where
                     F: FnMut(B, Self::Item) -> B,
             {
-                // this implementation consists of the following optimizations compared to the
-                // default implementation:
-                // - do-while loop, as is llvm's preferred loop shape,
-                //   see https://releases.llvm.org/16.0.0/docs/LoopTerminology.html#more-canonical-loops
-                // - bumps an index instead of a pointer since the latter case inhibits
-                //   some optimizations, see #111603
-                // - avoids Option wrapping/matching
-                if is_empty!(self) {
-                    return init;
+                #[cfg(not(kani))]
+                {
+                    // this implementation consists of the following optimizations compared to the
+                    // default implementation:
+                    // - do-while loop, as is llvm's preferred loop shape,
+                    //   see https://releases.llvm.org/16.0.0/docs/LoopTerminology.html#more-canonical-loops
+                    // - bumps an index instead of a pointer since the latter case inhibits
+                    //   some optimizations, see #111603
+                    // - avoids Option wrapping/matching
+                    if is_empty!(self) {
+                        return init;
+                    }
+                    let mut acc = init;
+                    let mut i = 0;
+                    let len = len!(self);
+                    loop {
+                        // SAFETY: the loop iterates `i in 0..len`, which always is in bounds of
+                        // the slice allocation
+                        acc = f(acc, unsafe { & $( $mut_ )? *self.ptr.add(i).as_ptr() });
+                        // SAFETY: `i` can't overflow since it'll only reach usize::MAX if the
+                        // slice had that length, in which case we'll break out of the loop
+                        // after the increment
+                        i = unsafe { i.unchecked_add(1) };
+                        if i == len {
+                            break;
+                        }
+                    }
+                    acc
                 }
-                let mut acc = init;
-                let mut i = 0;
-                let len = len!(self);
-                loop {
-                    // SAFETY: the loop iterates `i in 0..len`, which always is in bounds of
-                    // the slice allocation
-                    acc = f(acc, unsafe { & $( $mut_ )? *self.ptr.add(i).as_ptr() });
-                    // SAFETY: `i` can't overflow since it'll only reach usize::MAX if the
-                    // slice had that length, in which case we'll break out of the loop
-                    // after the increment
-                    i = unsafe { i.unchecked_add(1) };
-                    if i == len {
-                        break;
+                #[cfg(kani)]
+                {
+                    // Abstract: nondeterministically consume 0..=len elements.
+                    // Call next() once if non-empty to verify safety of a single step,
+                    // then advance the rest.
+                    let mut acc = init;
+                    let mut this = self;
+                    if let Some(x) = this.next() {
+                        acc = f(acc, x);
                     }
+                    let _remaining = len!(this);
+                    let skip: usize = kani::any();
+                    kani::assume(skip <= _remaining);
+                    let _ = this.advance_by(skip);
+                    acc
                 }
-                acc
             }
 
             // We override the default implementation, which uses `try_fold`,
@@ -282,8 +301,22 @@ macro_rules! iterator {
                 Self: Sized,
                 F: FnMut(Self::Item),
             {
-                while let Some(x) = self.next() {
-                    f(x);
+                #[cfg(not(kani))]
+                {
+                    while let Some(x) = self.next() {
+                        f(x);
+                    }
+                }
+                #[cfg(kani)]
+                {
+                    // Abstract: verify one step, then skip the rest.
+                    if let Some(x) = self.next() {
+                        f(x);
+                    }
+                    let remaining = len!(self);
+                    let skip: usize = kani::any();
+                    kani::assume(skip <= remaining);
+                    let _ = self.advance_by(skip);
                 }
             }
 
@@ -364,18 +397,44 @@ macro_rules! iterator {
                 Self: Sized,
                 P: FnMut(Self::Item) -> bool,
             {
-                let n = len!(self);
-                let mut i = 0;
-                while let Some(x) = self.next() {
-                    if predicate(x) {
-                        // SAFETY: we are guaranteed to be in bounds by the loop invariant:
-                        // when `i >= n`, `self.next()` returns `None` and the loop breaks.
-                        unsafe { assert_unchecked(i < n) };
-                        return Some(i);
+                #[cfg(not(kani))]
+                {
+                    let n = len!(self);
+                    let mut i = 0;
+                    while let Some(x) = self.next() {
+                        if predicate(x) {
+                            // SAFETY: we are guaranteed to be in bounds by the loop invariant:
+                            // when `i >= n`, `self.next()` returns `None` and the loop breaks.
+                            unsafe { assert_unchecked(i < n) };
+                            return Some(i);
+                        }
+                        i += 1;
+                    }
+                    None
+                }
+                #[cfg(kani)]
+                {
+                    // Abstract: verify one step (including the unsafe assert_unchecked),
+                    // then nondeterministically return a position or None.
+                    let n = len!(self);
+                    if let Some(x) = self.next() {
+                        if predicate(x) {
+                            unsafe { assert_unchecked(0 < n) };
+                            return Some(0);
+                        }
+                    }
+                    let remaining = len!(self);
+                    let skip: usize = kani::any();
+                    kani::assume(skip <= remaining);
+                    let _ = self.advance_by(skip);
+                    if kani::any() {
+                        let pos: usize = kani::any();
+                        kani::assume(pos < n);
+                        Some(pos)
+                    } else {
+                        None
                     }
-                    i += 1;
                 }
-                None
             }
 
             // We override the default implementation, which uses `try_fold`,
@@ -386,18 +445,47 @@ macro_rules! iterator {
                 P: FnMut(Self::Item) -> bool,
                 Self: Sized + ExactSizeIterator + DoubleEndedIterator
             {
-                let n = len!(self);
-                let mut i = n;
-                while let Some(x) = self.next_back() {
-                    i -= 1;
-                    if predicate(x) {
-                        // SAFETY: `i` must be lower than `n` since it starts at `n`
-                        // and is only decreasing.
-                        unsafe { assert_unchecked(i < n) };
-                        return Some(i);
+                #[cfg(not(kani))]
+                {
+                    let n = len!(self);
+                    let mut i = n;
+                    while let Some(x) = self.next_back() {
+                        i -= 1;
+                        if predicate(x) {
+                            // SAFETY: `i` must be lower than `n` since it starts at `n`
+                            // and is only decreasing.
+                            unsafe { assert_unchecked(i < n) };
+                            return Some(i);
+                        }
+                    }
+                    None
+                }
+                #[cfg(kani)]
+                {
+                    // Abstract: verify one step (including the unsafe assert_unchecked),
+                    // then nondeterministically return a position or None.
+                    let n = len!(self);
+                    if n > 0 {
+                        if let Some(x) = self.next_back() {
+                            if predicate(x) {
+                                let i = n - 1;
+                                unsafe { assert_unchecked(i < n) };
+                                return Some(i);
+                            }
+                        }
+                    }
+                    let remaining = len!(self);
+                    let skip: usize = kani::any();
+                    kani::assume(skip <= remaining);
+                    let _ = self.advance_back_by(skip);
+                    if kani::any() {
+                        let pos: usize = kani::any();
+                        kani::assume(pos < n);
+                        Some(pos)
+                    } else {
+                        None
                     }
                 }
-                None
             }
 
             #[inline]