diff --git a/library/core/src/iter/adapters/array_chunks.rs b/library/core/src/iter/adapters/array_chunks.rs
index 8f1744fc5fbb7..54e1b818fef7f 100644
--- a/library/core/src/iter/adapters/array_chunks.rs
+++ b/library/core/src/iter/adapters/array_chunks.rs
@@ -274,3 +274,65 @@ unsafe impl<I: InPlaceIterable + Iterator, const N: usize> InPlaceIterable for A
         }
     };
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+    use crate::kani;
+
+    fn any_slice<T>(orig: &[T]) -> &[T] {
+        if kani::any() {
+            let last = kani::any_where(|i: &usize| *i <= orig.len());
+            let first = kani::any_where(|i: &usize| *i <= last);
+            &orig[first..last]
+        } else {
+            let ptr = kani::any_where::<usize, _>(|v| *v != 0) as *const T;
+            kani::assume(ptr.is_aligned());
+            unsafe { crate::slice::from_raw_parts(ptr, 0) }
+        }
+    }
+
+    // `next_back_remainder` pulls the final `len % N` elements off the back via
+    // `rev().take(rem).next_chunk()`, then reverses them in place, relying on
+    // `unwrap_err_unchecked` (sound because `rem < N`).
+    macro_rules! check_next_back_remainder {
+        ($harness:ident, $elem_ty:ty, $n:expr, $max_len:expr) => {
+            #[kani::proof]
+            fn $harness() {
+                const N: usize = $n;
+                const MAX_LEN: usize = $max_len;
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let mut it: ArrayChunks<_, N> = ArrayChunks::new(any_slice(&array).iter());
+                it.next_back_remainder();
+                let _ = &it.remainder;
+            }
+        };
+    }
+    check_next_back_remainder!(check_array_chunks_next_back_remainder_unit, (), 2, 8);
+    check_next_back_remainder!(check_array_chunks_next_back_remainder_u8, u8, 2, 8);
+    check_next_back_remainder!(check_array_chunks_next_back_remainder_char, char, 3, 9);
+    check_next_back_remainder!(check_array_chunks_next_back_remainder_tup, (char, u8), 2, 8);
+
+    // `fold` on a `TrustedRandomAccessNoCoerce` source builds each chunk with
+    // `array::from_fn` calling `__iterator_get_unchecked(i + local)` under an
+    // `inner_len - i >= N` guard; this proves those indexes stay in bounds.
+    macro_rules! check_fold {
+        ($harness:ident, $elem_ty:ty, $n:expr, $max_len:expr, $unwind:literal) => {
+            #[kani::proof]
+            #[kani::unwind($unwind)]
+            fn $harness() {
+                const N: usize = $n;
+                const MAX_LEN: usize = $max_len;
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let it: ArrayChunks<_, N> = ArrayChunks::new(any_slice(&array).iter());
+                // Disambiguate from the in-scope internal `SpecFold::fold`.
+                let _ = crate::iter::Iterator::fold(it, 0usize, |acc, _chunk| acc.wrapping_add(1));
+            }
+        };
+    }
+    check_fold!(check_array_chunks_fold_unit, (), 2, 4, 5);
+    check_fold!(check_array_chunks_fold_u8, u8, 2, 4, 5);
+    check_fold!(check_array_chunks_fold_char, char, 3, 6, 7);
+    check_fold!(check_array_chunks_fold_tup, (char, u8), 2, 4, 5);
+}
diff --git a/library/core/src/iter/adapters/cloned.rs b/library/core/src/iter/adapters/cloned.rs
index 0f05260059880..79a900719dfe8 100644
--- a/library/core/src/iter/adapters/cloned.rs
+++ b/library/core/src/iter/adapters/cloned.rs
@@ -193,3 +193,62 @@ unsafe impl<I: InPlaceIterable> InPlaceIterable for Cloned<I> {
     const EXPAND_BY: Option<NonZero<usize>> = I::EXPAND_BY;
     const MERGE_BY: Option<NonZero<usize>> = I::MERGE_BY;
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+    use crate::kani;
+
+    fn any_slice<T>(orig_slice: &[T]) -> &[T] {
+        if kani::any() {
+            let last = kani::any_where(|idx: &usize| *idx <= orig_slice.len());
+            let first = kani::any_where(|idx: &usize| *idx <= last);
+            &orig_slice[first..last]
+        } else {
+            let ptr = kani::any_where::<usize, _>(|val| *val != 0) as *const T;
+            kani::assume(ptr.is_aligned());
+            unsafe { crate::slice::from_raw_parts(ptr, 0) }
+        }
+    }
+
+    fn any_cloned_iter<'a, T: Clone>(orig_slice: &'a [T]) -> Cloned<crate::slice::Iter<'a, T>> {
+        Cloned::new(any_slice(orig_slice).iter())
+    }
+
+    macro_rules! check_get_unchecked {
+        ($harness:ident, $elem_ty:ty, $max_len:expr) => {
+            #[kani::proof]
+            fn $harness() {
+                const MAX_LEN: usize = $max_len;
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let mut it = any_cloned_iter::<$elem_ty>(&array);
+                let idx = kani::any_where(|i: &usize| *i < it.it.size_hint().0);
+                let _ = unsafe { it.__iterator_get_unchecked(idx) };
+            }
+        };
+    }
+    check_get_unchecked!(check_cloned_get_unchecked_unit, (), isize::MAX as usize);
+    check_get_unchecked!(check_cloned_get_unchecked_u8, u8, u32::MAX as usize);
+    check_get_unchecked!(check_cloned_get_unchecked_char, char, 50);
+    check_get_unchecked!(check_cloned_get_unchecked_tup, (char, u8), 50);
+
+    // `next_unchecked` (UncheckedIterator): the precondition is that the iterator
+    // is non-empty; establish it by construction.
+    macro_rules! check_cloned_next_unchecked {
+        ($harness:ident, $elem_ty:ty, $max_len:expr) => {
+            #[kani::proof]
+            fn $harness() {
+                const MAX_LEN: usize = $max_len;
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let mut it = any_cloned_iter::<$elem_ty>(&array);
+                kani::assume(it.it.size_hint().0 > 0);
+                let _ = unsafe { it.next_unchecked() };
+            }
+        };
+    }
+    check_cloned_next_unchecked!(check_cloned_next_unchecked_unit, (), isize::MAX as usize);
+    check_cloned_next_unchecked!(check_cloned_next_unchecked_u8, u8, u32::MAX as usize);
+    check_cloned_next_unchecked!(check_cloned_next_unchecked_char, char, 50);
+    check_cloned_next_unchecked!(check_cloned_next_unchecked_tup, (char, u8), 50);
+}
diff --git a/library/core/src/iter/adapters/copied.rs b/library/core/src/iter/adapters/copied.rs
index 0b9da45acaa06..f9a131e756ba4 100644
--- a/library/core/src/iter/adapters/copied.rs
+++ b/library/core/src/iter/adapters/copied.rs
@@ -278,3 +278,66 @@ unsafe impl<I: InPlaceIterable> InPlaceIterable for Copied<I> {
     const EXPAND_BY: Option<NonZero<usize>> = I::EXPAND_BY;
     const MERGE_BY: Option<NonZero<usize>> = I::MERGE_BY;
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+    use crate::kani;
+
+    fn any_slice<T>(orig_slice: &[T]) -> &[T] {
+        if kani::any() {
+            let last = kani::any_where(|idx: &usize| *idx <= orig_slice.len());
+            let first = kani::any_where(|idx: &usize| *idx <= last);
+            &orig_slice[first..last]
+        } else {
+            let ptr = kani::any_where::<usize, _>(|val| *val != 0) as *const T;
+            kani::assume(ptr.is_aligned());
+            unsafe { crate::slice::from_raw_parts(ptr, 0) }
+        }
+    }
+
+    fn any_adapter_iter<'a, T>(orig_slice: &'a [T]) -> Copied<crate::slice::Iter<'a, T>> {
+        Copied::new(any_slice(orig_slice).iter())
+    }
+
+    macro_rules! check_get_unchecked {
+        ($harness:ident, $elem_ty:ty, $max_len:expr) => {
+            #[kani::proof]
+            fn $harness() {
+                const MAX_LEN: usize = $max_len;
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let mut it = any_adapter_iter::<$elem_ty>(&array);
+                let idx = kani::any_where(|i: &usize| *i < it.it.size_hint().0);
+                let _ = unsafe { it.__iterator_get_unchecked(idx) };
+            }
+        };
+    }
+    check_get_unchecked!(check_copied_get_unchecked_unit, (), isize::MAX as usize);
+    check_get_unchecked!(check_copied_get_unchecked_u8, u8, u32::MAX as usize);
+    check_get_unchecked!(check_copied_get_unchecked_char, char, 50);
+    check_get_unchecked!(check_copied_get_unchecked_tup, (char, u8), 50);
+
+    // `spec_next_chunk` on the `slice::Iter` specialization bulk-copies `N` (or
+    // `len`) elements into a `MaybeUninit<[T; N]>` and then either
+    // `array_assume_init`s the full array or returns a `0..len` `IntoIter`; this
+    // proves the `copy_nonoverlapping` lengths and the init range stay in bounds.
+    // `N` is a trait generic, so it is pinned via the result type annotation.
+    macro_rules! check_spec_next_chunk {
+        ($harness:ident, $elem_ty:ty, $n:expr) => {
+            #[kani::proof]
+            fn $harness() {
+                const N: usize = $n;
+                const MAX_LEN: usize = 16;
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let mut it = any_slice(&array).iter();
+                let _result: Result<[$elem_ty; N], crate::array::IntoIter<$elem_ty, N>> =
+                    it.spec_next_chunk();
+            }
+        };
+    }
+    check_spec_next_chunk!(check_copied_spec_next_chunk_unit, (), 2);
+    check_spec_next_chunk!(check_copied_spec_next_chunk_u8, u8, 3);
+    check_spec_next_chunk!(check_copied_spec_next_chunk_char, char, 2);
+    check_spec_next_chunk!(check_copied_spec_next_chunk_tup, (char, u8), 2);
+}
diff --git a/library/core/src/iter/adapters/enumerate.rs b/library/core/src/iter/adapters/enumerate.rs
index e7e18d178031f..553d1946bbdb3 100644
--- a/library/core/src/iter/adapters/enumerate.rs
+++ b/library/core/src/iter/adapters/enumerate.rs
@@ -321,3 +321,67 @@ impl<I: Default> Default for Enumerate<I> {
         Enumerate::new(Default::default())
     }
 }
+
+/// Verification harnesses for `Enumerate`'s `unsafe`/contract-bearing methods
+/// (verify-rust-std challenge #16).
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+    use crate::kani;
+
+    /// An arbitrary-length sub-slice of `orig_slice` (mirrors
+    /// `slice::iter::verify::any_slice`).  This is what makes the proof
+    /// *unbounded*: the backing array is a fixed Kani constant, but the slice
+    /// handed to the iterator has a symbolic length, so the proof covers every
+    /// shorter configuration at once.
+    fn any_slice<T>(orig_slice: &[T]) -> &[T] {
+        if kani::any() {
+            let last = kani::any_where(|idx: &usize| *idx <= orig_slice.len());
+            let first = kani::any_where(|idx: &usize| *idx <= last);
+            &orig_slice[first..last]
+        } else {
+            let ptr = kani::any_where::<usize, _>(|val| *val != 0) as *const T;
+            kani::assume(ptr.is_aligned());
+            // SAFETY: `ptr` is non-null and aligned; length 0 makes the slice trivially valid.
+            unsafe { crate::slice::from_raw_parts(ptr, 0) }
+        }
+    }
+
+    /// Wrap an arbitrary sub-slice in `Enumerate<slice::Iter<'_, T>>`.  We build
+    /// the inner `slice::Iter` via `(&[T]).iter()` because `slice::Iter::new` is
+    /// `pub(super)` to the `slice` module and unreachable from here.
+    fn any_enumerate_iter<'a, T>(orig_slice: &'a [T]) -> Enumerate<crate::slice::Iter<'a, T>> {
+        Enumerate::new(any_slice(orig_slice).iter())
+    }
+
+    /// One `proof_for_contract` harness per concrete element type; the contract
+    /// itself stays generic.  `slice::Iter<T>` is `TrustedRandomAccessNoCoerce`
+    /// for every `T`, satisfying the method's `Self: TrustedRandomAccessNoCoerce`.
+    // NOTE: `__iterator_get_unchecked` is a trait method on the *generic* impl
+    // `impl<I> Iterator for Enumerate<I>`, and Kani cannot attach a
+    // `proof_for_contract` to a generic trait method (kani#1997).  So instead of
+    // the contract machinery we use a plain `#[kani::proof]` that establishes the
+    // method's precondition by construction (`idx < self.iter.size_hint().0`) and
+    // lets Kani prove the body introduces no UB -- the same safety property the
+    // contract expresses.
+    macro_rules! check_enumerate_get_unchecked {
+        ($harness:ident, $elem_ty:ty, $max_len:expr) => {
+            #[kani::proof]
+            fn $harness() {
+                const MAX_LEN: usize = $max_len;
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let mut enumerate = any_enumerate_iter::<$elem_ty>(&array);
+                // The method's precondition: `idx < self.iter.size_hint().0`.
+                let idx = kani::any_where(|i: &usize| *i < enumerate.iter.size_hint().0);
+                let _ = unsafe { enumerate.__iterator_get_unchecked(idx) };
+            }
+        };
+    }
+
+    // Representative element types: ZST, byte, 4-byte-align niche type, composite.
+    check_enumerate_get_unchecked!(check_enumerate_get_unchecked_unit, (), isize::MAX as usize);
+    check_enumerate_get_unchecked!(check_enumerate_get_unchecked_u8, u8, u32::MAX as usize);
+    check_enumerate_get_unchecked!(check_enumerate_get_unchecked_char, char, 50);
+    check_enumerate_get_unchecked!(check_enumerate_get_unchecked_tup, (char, u8), 50);
+}
diff --git a/library/core/src/iter/adapters/filter.rs b/library/core/src/iter/adapters/filter.rs
index dd08cd6f61c4c..936dbe2bedb59 100644
--- a/library/core/src/iter/adapters/filter.rs
+++ b/library/core/src/iter/adapters/filter.rs
@@ -214,3 +214,52 @@ unsafe impl<I: InPlaceIterable, P> InPlaceIterable for Filter<I, P> {
     const EXPAND_BY: Option<NonZero<usize>> = I::EXPAND_BY;
     const MERGE_BY: Option<NonZero<usize>> = I::MERGE_BY;
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+    use crate::kani;
+
+    fn any_slice<T>(orig: &[T]) -> &[T] {
+        if kani::any() {
+            let last = kani::any_where(|i: &usize| *i <= orig.len());
+            let first = kani::any_where(|i: &usize| *i <= last);
+            &orig[first..last]
+        } else {
+            let ptr = kani::any_where::<usize, _>(|v| *v != 0) as *const T;
+            kani::assume(ptr.is_aligned());
+            unsafe { crate::slice::from_raw_parts(ptr, 0) }
+        }
+    }
+
+    // `Filter`'s predicate is `FnMut(&Self::Item)`; for `slice::Iter<T>` that is
+    // `FnMut(&&T)`. A nondeterministic predicate exercises both the kept and the
+    // filtered branch. A named fn pointer keeps the helper return type nameable.
+    fn maybe_keep<T>(_: &&T) -> bool {
+        kani::any()
+    }
+
+    // `next_chunk_dropless` writes every element (branchlessly) into a
+    // `MaybeUninit<[_; N]>` and bumps `initialized` only for kept elements,
+    // breaking once `initialized == N`; this proves the `get_unchecked_mut(idx)`
+    // writes and the final `array_assume_init` / `IntoIter` range stay in bounds.
+    macro_rules! check_next_chunk_dropless {
+        ($harness:ident, $elem_ty:ty) => {
+            #[kani::proof]
+            #[kani::unwind(7)]
+            fn $harness() {
+                const MAX_LEN: usize = 6;
+                const N: usize = 4;
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let mut it =
+                    Filter::new(any_slice(&array).iter(), maybe_keep::<$elem_ty> as fn(&&$elem_ty) -> bool);
+                let _ = it.next_chunk_dropless::<N>();
+            }
+        };
+    }
+    check_next_chunk_dropless!(check_filter_next_chunk_dropless_unit, ());
+    check_next_chunk_dropless!(check_filter_next_chunk_dropless_u8, u8);
+    check_next_chunk_dropless!(check_filter_next_chunk_dropless_char, char);
+    check_next_chunk_dropless!(check_filter_next_chunk_dropless_tup, (char, u8));
+}
diff --git a/library/core/src/iter/adapters/filter_map.rs b/library/core/src/iter/adapters/filter_map.rs
index 24ec6b1741ce1..f09cae914e6f5 100644
--- a/library/core/src/iter/adapters/filter_map.rs
+++ b/library/core/src/iter/adapters/filter_map.rs
@@ -211,3 +211,53 @@ unsafe impl<I: InPlaceIterable, F> InPlaceIterable for FilterMap<I, F> {
     const EXPAND_BY: Option<NonZero<usize>> = I::EXPAND_BY;
     const MERGE_BY: Option<NonZero<usize>> = I::MERGE_BY;
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+    use crate::kani;
+
+    fn any_slice<T>(orig: &[T]) -> &[T] {
+        if kani::any() {
+            let last = kani::any_where(|i: &usize| *i <= orig.len());
+            let first = kani::any_where(|i: &usize| *i <= last);
+            &orig[first..last]
+        } else {
+            let ptr = kani::any_where::<usize, _>(|v| *v != 0) as *const T;
+            kani::assume(ptr.is_aligned());
+            unsafe { crate::slice::from_raw_parts(ptr, 0) }
+        }
+    }
+
+    // Maps `&T -> Option<usize>` nondeterministically to exercise both the
+    // "element kept" and "element filtered" paths of the chunk-fill loop.
+    fn maybe_map<T>(_: &T) -> Option<usize> {
+        kani::any::<bool>().then_some(0)
+    }
+
+    // `next_chunk` fills a `MaybeUninit<[B; N]>` via a `Guard`-protected loop
+    // that byte-copies each mapped value's payload and bumps `initialized` only
+    // when the map yields `Some`; this proves the copies, the `array_assume_init`,
+    // and the partial-fill `IntoIter` range all stay in bounds.
+    macro_rules! check_next_chunk {
+        ($harness:ident, $elem_ty:ty) => {
+            #[kani::proof]
+            #[kani::unwind(6)]
+            fn $harness() {
+                const MAX_LEN: usize = 5;
+                const N: usize = 3;
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let mut it = FilterMap::new(
+                    any_slice(&array).iter(),
+                    maybe_map::<$elem_ty> as fn(&$elem_ty) -> Option<usize>,
+                );
+                let _ = it.next_chunk::<N>();
+            }
+        };
+    }
+    check_next_chunk!(check_filter_map_next_chunk_unit, ());
+    check_next_chunk!(check_filter_map_next_chunk_u8, u8);
+    check_next_chunk!(check_filter_map_next_chunk_char, char);
+    check_next_chunk!(check_filter_map_next_chunk_tup, (char, u8));
+}
diff --git a/library/core/src/iter/adapters/fuse.rs b/library/core/src/iter/adapters/fuse.rs
index fcad6168d85cd..11d607ba466fb 100644
--- a/library/core/src/iter/adapters/fuse.rs
+++ b/library/core/src/iter/adapters/fuse.rs
@@ -478,3 +478,43 @@ fn and_then_or_clear<T, U>(opt: &mut Option<T>, f: impl FnOnce(&mut T) -> Option
     }
     x
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+    use crate::kani;
+
+    fn any_slice<T>(orig_slice: &[T]) -> &[T] {
+        if kani::any() {
+            let last = kani::any_where(|idx: &usize| *idx <= orig_slice.len());
+            let first = kani::any_where(|idx: &usize| *idx <= last);
+            &orig_slice[first..last]
+        } else {
+            let ptr = kani::any_where::<usize, _>(|val| *val != 0) as *const T;
+            kani::assume(ptr.is_aligned());
+            unsafe { crate::slice::from_raw_parts(ptr, 0) }
+        }
+    }
+
+    fn any_fuse_iter<'a, T>(orig_slice: &'a [T]) -> Fuse<crate::slice::Iter<'a, T>> {
+        Fuse::new(any_slice(orig_slice).iter())
+    }
+
+    macro_rules! check_get_unchecked {
+        ($harness:ident, $elem_ty:ty, $max_len:expr) => {
+            #[kani::proof]
+            fn $harness() {
+                const MAX_LEN: usize = $max_len;
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let mut it = any_fuse_iter::<$elem_ty>(&array);
+                let idx = kani::any_where(|i: &usize| *i < it.iter.as_ref().unwrap().size_hint().0);
+                let _ = unsafe { it.__iterator_get_unchecked(idx) };
+            }
+        };
+    }
+    check_get_unchecked!(check_fuse_get_unchecked_unit, (), isize::MAX as usize);
+    check_get_unchecked!(check_fuse_get_unchecked_u8, u8, u32::MAX as usize);
+    check_get_unchecked!(check_fuse_get_unchecked_char, char, 50);
+    check_get_unchecked!(check_fuse_get_unchecked_tup, (char, u8), 50);
+}
diff --git a/library/core/src/iter/adapters/map.rs b/library/core/src/iter/adapters/map.rs
index bf9f0c48fec3b..eb77668fd620b 100644
--- a/library/core/src/iter/adapters/map.rs
+++ b/library/core/src/iter/adapters/map.rs
@@ -245,3 +245,69 @@ unsafe impl<I: InPlaceIterable, F> InPlaceIterable for Map<I, F> {
     const EXPAND_BY: Option<NonZero<usize>> = I::EXPAND_BY;
     const MERGE_BY: Option<NonZero<usize>> = I::MERGE_BY;
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+    use crate::kani;
+
+    fn any_slice<T>(orig_slice: &[T]) -> &[T] {
+        if kani::any() {
+            let last = kani::any_where(|idx: &usize| *idx <= orig_slice.len());
+            let first = kani::any_where(|idx: &usize| *idx <= last);
+            &orig_slice[first..last]
+        } else {
+            let ptr = kani::any_where::<usize, _>(|val| *val != 0) as *const T;
+            kani::assume(ptr.is_aligned());
+            unsafe { crate::slice::from_raw_parts(ptr, 0) }
+        }
+    }
+
+    // The mapping closure is irrelevant to buffer/UB safety; a simple
+    // `&T -> usize` fn pointer (nameable, unlike a closure) keeps the harness
+    // type concrete.  `slice::Iter<T>` yields `&T`, so `F: FnMut(&T) -> usize`.
+    fn map_fn<T>(_: &T) -> usize {
+        0
+    }
+
+    fn any_map_iter<'a, T>(orig_slice: &'a [T]) -> Map<crate::slice::Iter<'a, T>, fn(&T) -> usize> {
+        Map::new(any_slice(orig_slice).iter(), map_fn::<T> as fn(&T) -> usize)
+    }
+
+    macro_rules! check_map_get_unchecked {
+        ($harness:ident, $elem_ty:ty, $max_len:expr) => {
+            #[kani::proof]
+            fn $harness() {
+                const MAX_LEN: usize = $max_len;
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let mut it = any_map_iter::<$elem_ty>(&array);
+                let idx = kani::any_where(|i: &usize| *i < it.iter.size_hint().0);
+                let _ = unsafe { it.__iterator_get_unchecked(idx) };
+            }
+        };
+    }
+
+    macro_rules! check_map_next_unchecked {
+        ($harness:ident, $elem_ty:ty, $max_len:expr) => {
+            #[kani::proof]
+            fn $harness() {
+                const MAX_LEN: usize = $max_len;
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let mut it = any_map_iter::<$elem_ty>(&array);
+                kani::assume(it.iter.size_hint().0 > 0);
+                let _ = unsafe { it.next_unchecked() };
+            }
+        };
+    }
+
+    check_map_get_unchecked!(check_map_get_unchecked_unit, (), isize::MAX as usize);
+    check_map_get_unchecked!(check_map_get_unchecked_u8, u8, u32::MAX as usize);
+    check_map_get_unchecked!(check_map_get_unchecked_char, char, 50);
+    check_map_get_unchecked!(check_map_get_unchecked_tup, (char, u8), 50);
+
+    check_map_next_unchecked!(check_map_next_unchecked_unit, (), isize::MAX as usize);
+    check_map_next_unchecked!(check_map_next_unchecked_u8, u8, u32::MAX as usize);
+    check_map_next_unchecked!(check_map_next_unchecked_char, char, 50);
+    check_map_next_unchecked!(check_map_next_unchecked_tup, (char, u8), 50);
+}
diff --git a/library/core/src/iter/adapters/map_windows.rs b/library/core/src/iter/adapters/map_windows.rs
index 536251a137da0..6980784d55396 100644
--- a/library/core/src/iter/adapters/map_windows.rs
+++ b/library/core/src/iter/adapters/map_windows.rs
@@ -297,3 +297,73 @@ impl<T, const N: usize> Invariant for Buffer<T, N> {
         self.start + N <= 2 * N
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+    use crate::kani;
+
+    // Build a `Buffer<T, N>` in a valid state: `start` in `[0, N]` (the type
+    // invariant) and the live window `[start, start + N)` fully initialized with
+    // arbitrary values; the remaining `N` slots stay uninitialized, exactly as
+    // the real buffer maintains them.
+    fn any_buffer<T: kani::Arbitrary, const N: usize>() -> Buffer<T, N> {
+        let start = kani::any_where(|s: &usize| *s <= N);
+        let mut buffer = Buffer {
+            buffer: [[const { MaybeUninit::uninit() }; N], [const { MaybeUninit::uninit() }; N]],
+            start,
+        };
+        let items: [T; N] = kani::any();
+        let base = buffer.buffer_mut_ptr();
+        items.into_iter().enumerate().for_each(|(i, item)| {
+            // SAFETY: `start + i < start + N <= 2 * N`, in bounds of the `2 * N` buffer.
+            unsafe { (*base.add(start + i)).write(item) };
+        });
+        buffer
+    }
+
+    // `as_array_ref` / `as_uninit_array_mut` reinterpret the live window as an
+    // array reference; `push` rotates the window (and wraps + compacts when
+    // `start == N`); `drop` drops the live window. Each must respect the
+    // initialized-window invariant and stay in bounds of the `2 * N` storage.
+    macro_rules! check_buffer {
+        ($module:ident, $elem_ty:ty, $n:expr) => {
+            mod $module {
+                use super::*;
+                const N: usize = $n;
+
+                #[kani::proof]
+                fn check_as_array_ref() {
+                    let buf = any_buffer::<$elem_ty, N>();
+                    let _ = buf.as_array_ref();
+                    kani::assert(buf.is_safe(), "buffer invariant holds");
+                }
+
+                #[kani::proof]
+                fn check_as_uninit_array_mut() {
+                    let mut buf = any_buffer::<$elem_ty, N>();
+                    let _ = buf.as_uninit_array_mut();
+                    kani::assert(buf.is_safe(), "buffer invariant holds");
+                }
+
+                #[kani::proof]
+                fn check_push() {
+                    let mut buf = any_buffer::<$elem_ty, N>();
+                    buf.push(kani::any());
+                    kani::assert(buf.is_safe(), "buffer invariant holds after push");
+                }
+
+                #[kani::proof]
+                fn check_drop() {
+                    let buf = any_buffer::<$elem_ty, N>();
+                    drop(buf);
+                }
+            }
+        };
+    }
+    check_buffer!(verify_map_windows_unit, (), 3);
+    check_buffer!(verify_map_windows_u8, u8, 3);
+    check_buffer!(verify_map_windows_char, char, 2);
+    check_buffer!(verify_map_windows_tup, (char, u8), 2);
+}
diff --git a/library/core/src/iter/adapters/skip.rs b/library/core/src/iter/adapters/skip.rs
index ac3cc4c4f1152..499517c7e7678 100644
--- a/library/core/src/iter/adapters/skip.rs
+++ b/library/core/src/iter/adapters/skip.rs
@@ -293,3 +293,45 @@ where
 // I: TrustedLen would not.
 #[unstable(feature = "trusted_len", issue = "37572")]
 unsafe impl<I> TrustedLen for Skip<I> where I: Iterator + TrustedRandomAccess {}
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+    use crate::kani;
+
+    fn any_slice<T>(orig_slice: &[T]) -> &[T] {
+        if kani::any() {
+            let last = kani::any_where(|idx: &usize| *idx <= orig_slice.len());
+            let first = kani::any_where(|idx: &usize| *idx <= last);
+            &orig_slice[first..last]
+        } else {
+            let ptr = kani::any_where::<usize, _>(|val| *val != 0) as *const T;
+            kani::assume(ptr.is_aligned());
+            unsafe { crate::slice::from_raw_parts(ptr, 0) }
+        }
+    }
+
+    fn any_skip_iter<'a, T>(orig_slice: &'a [T]) -> Skip<crate::slice::Iter<'a, T>> {
+        let slice = any_slice(orig_slice);
+        let n = kani::any_where(|offset: &usize| *offset <= slice.len());
+        Skip::new(slice.iter(), n)
+    }
+
+    macro_rules! check_get_unchecked {
+        ($harness:ident, $elem_ty:ty, $max_len:expr) => {
+            #[kani::proof]
+            fn $harness() {
+                const MAX_LEN: usize = $max_len;
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let mut it = any_skip_iter::<$elem_ty>(&array);
+                let idx = kani::any_where(|i: &usize| *i < it.iter.size_hint().0 - it.n);
+                let _ = unsafe { it.__iterator_get_unchecked(idx) };
+            }
+        };
+    }
+    check_get_unchecked!(check_skip_get_unchecked_unit, (), isize::MAX as usize);
+    check_get_unchecked!(check_skip_get_unchecked_u8, u8, u32::MAX as usize);
+    check_get_unchecked!(check_skip_get_unchecked_char, char, 50);
+    check_get_unchecked!(check_skip_get_unchecked_tup, (char, u8), 50);
+}
diff --git a/library/core/src/iter/adapters/step_by.rs b/library/core/src/iter/adapters/step_by.rs
index 32604a07ca40c..1ac22d698a43e 100644
--- a/library/core/src/iter/adapters/step_by.rs
+++ b/library/core/src/iter/adapters/step_by.rs
@@ -589,3 +589,46 @@ spec_int_ranges_r!(u8 u16 u32 usize);
 spec_int_ranges!(u8 u16 usize);
 #[cfg(target_pointer_width = "16")]
 spec_int_ranges_r!(u8 u16 usize);
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+    use crate::kani;
+
+    fn any_slice<T>(orig: &[T]) -> &[T] {
+        if kani::any() {
+            let last = kani::any_where(|i: &usize| *i <= orig.len());
+            let first = kani::any_where(|i: &usize| *i <= last);
+            &orig[first..last]
+        } else {
+            let ptr = kani::any_where::<usize, _>(|v| *v != 0) as *const T;
+            kani::assume(ptr.is_aligned());
+            unsafe { crate::slice::from_raw_parts(ptr, 0) }
+        }
+    }
+
+    // `original_step` reconstructs the configured step as `step_minus_one + 1`
+    // via `unchecked_add` and `NonZero::new_unchecked`. The type invariant
+    // (`step_minus_one < usize::MAX`) makes both operations sound; a valid
+    // `StepBy` is established by construction (`StepBy::new` requires `step != 0`).
+    macro_rules! check_original_step {
+        ($harness:ident, $elem_ty:ty, $max_len:expr) => {
+            #[kani::proof]
+            fn $harness() {
+                const MAX_LEN: usize = $max_len;
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let step = kani::any_where(|s: &usize| *s != 0);
+                let it = StepBy::new(any_slice(&array).iter(), step);
+                let result = it.original_step();
+                kani::assert(result.get() == step, "original_step round-trips the configured step");
+            }
+        };
+    }
+    // `original_step` ignores the wrapped iterator, so a small backing array
+    // suffices; the proof is over the symbolic `step`, not the slice length.
+    check_original_step!(check_step_by_original_step_unit, (), 16);
+    check_original_step!(check_step_by_original_step_u8, u8, 16);
+    check_original_step!(check_step_by_original_step_char, char, 16);
+    check_original_step!(check_step_by_original_step_tup, (char, u8), 16);
+}
diff --git a/library/core/src/iter/adapters/take.rs b/library/core/src/iter/adapters/take.rs
index b96335f415257..7924ccdc8a5d7 100644
--- a/library/core/src/iter/adapters/take.rs
+++ b/library/core/src/iter/adapters/take.rs
@@ -374,3 +374,54 @@ impl<F: FnMut() -> A, A> ExactSizeIterator for Take<crate::iter::RepeatWith<F>>
         self.n
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+    use crate::kani;
+
+    fn any_slice<T>(orig: &[T]) -> &[T] {
+        if kani::any() {
+            let last = kani::any_where(|i: &usize| *i <= orig.len());
+            let first = kani::any_where(|i: &usize| *i <= last);
+            &orig[first..last]
+        } else {
+            let ptr = kani::any_where::<usize, _>(|v| *v != 0) as *const T;
+            kani::assume(ptr.is_aligned());
+            unsafe { crate::slice::from_raw_parts(ptr, 0) }
+        }
+    }
+
+    // On a `TrustedRandomAccess` source, `SpecTake::spec_fold` / `spec_for_each`
+    // drive a `0..end` loop calling `__iterator_get_unchecked(i)` where
+    // `end = self.n.min(self.iter.size())`; this proves those unchecked indexes
+    // stay in bounds. `MAX_LEN` is bounded because the methods iterate.
+    macro_rules! check_spec_take {
+        ($fold_harness:ident, $each_harness:ident, $elem_ty:ty) => {
+            #[kani::proof]
+            #[kani::unwind(6)]
+            fn $fold_harness() {
+                const MAX_LEN: usize = 5;
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let n = kani::any_where(|n: &usize| *n <= MAX_LEN);
+                let it = Take::new(any_slice(&array).iter(), n);
+                let _ = it.spec_fold(0usize, |acc, _| acc.wrapping_add(1));
+            }
+
+            #[kani::proof]
+            #[kani::unwind(6)]
+            fn $each_harness() {
+                const MAX_LEN: usize = 5;
+                let array: [$elem_ty; MAX_LEN] = kani::any();
+                let n = kani::any_where(|n: &usize| *n <= MAX_LEN);
+                let it = Take::new(any_slice(&array).iter(), n);
+                it.spec_for_each(|_| {});
+            }
+        };
+    }
+    check_spec_take!(check_take_spec_fold_unit, check_take_spec_for_each_unit, ());
+    check_spec_take!(check_take_spec_fold_u8, check_take_spec_for_each_u8, u8);
+    check_spec_take!(check_take_spec_fold_char, check_take_spec_for_each_char, char);
+    check_spec_take!(check_take_spec_fold_tup, check_take_spec_for_each_tup, (char, u8));
+}
diff --git a/library/core/src/iter/adapters/zip.rs b/library/core/src/iter/adapters/zip.rs
index e39f1535bd95d..85faeb442c753 100644
--- a/library/core/src/iter/adapters/zip.rs
+++ b/library/core/src/iter/adapters/zip.rs
@@ -692,3 +692,118 @@ impl<A: TrustedLen, B: TrustedLen> SpecFold for Zip<A, B> {
         accum
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+    use crate::kani;
+
+    fn any_slice<T>(orig_slice: &[T]) -> &[T] {
+        if kani::any() {
+            let last = kani::any_where(|idx: &usize| *idx <= orig_slice.len());
+            let first = kani::any_where(|idx: &usize| *idx <= last);
+            &orig_slice[first..last]
+        } else {
+            let ptr = kani::any_where::<usize, _>(|val| *val != 0) as *const T;
+            kani::assume(ptr.is_aligned());
+            unsafe { crate::slice::from_raw_parts(ptr, 0) }
+        }
+    }
+
+    fn any_zip_iter<'a, T, U>(
+        orig_slice_a: &'a [T],
+        orig_slice_b: &'a [U],
+    ) -> Zip<crate::slice::Iter<'a, T>, crate::slice::Iter<'a, U>> {
+        Zip::new(any_slice(orig_slice_a).iter(), any_slice(orig_slice_b).iter())
+    }
+
+    macro_rules! check_zip_get_unchecked {
+        ($harness:ident, $elem_ty_a:ty, $elem_ty_b:ty, $max_len:expr) => {
+            #[kani::proof]
+            fn $harness() {
+                const MAX_LEN: usize = $max_len;
+                let array_a: [$elem_ty_a; MAX_LEN] = kani::any();
+                let array_b: [$elem_ty_b; MAX_LEN] = kani::any();
+                let mut it = any_zip_iter::<$elem_ty_a, $elem_ty_b>(&array_a, &array_b);
+                let idx = kani::any_where(|i: &usize| *i < crate::iter::Iterator::size_hint(&it).0);
+                let _ = unsafe { it.__iterator_get_unchecked(idx) };
+            }
+        };
+    }
+
+    check_zip_get_unchecked!(check_zip_get_unchecked_unit_unit, (), (), 50);
+    check_zip_get_unchecked!(check_zip_get_unchecked_u8_u8, u8, u8, u32::MAX as usize);
+    check_zip_get_unchecked!(check_zip_get_unchecked_char_u8, char, u8, 50);
+    check_zip_get_unchecked!(check_zip_get_unchecked_u8_char, u8, char, 50);
+    check_zip_get_unchecked!(check_zip_get_unchecked_tup_tup, (char, u8), (u32, i16), 50);
+
+    // Safe `Zip` methods on `TrustedRandomAccess` sources drive the same
+    // `get_unchecked`-based machinery as `__iterator_get_unchecked`; these prove
+    // `next` / `nth` / `next_back` / `fold` / `spec_fold` keep their internal
+    // indexes in bounds. Bounded `MAX_LEN` because the methods iterate.
+    macro_rules! check_zip_safe {
+        ($a:ty, $b:ty, $next:ident, $nth:ident, $back:ident, $fold:ident, $spec:ident) => {
+            #[kani::proof]
+            fn $next() {
+                const MAX_LEN: usize = 16;
+                let array_a: [$a; MAX_LEN] = kani::any();
+                let array_b: [$b; MAX_LEN] = kani::any();
+                let mut it = any_zip_iter::<$a, $b>(&array_a, &array_b);
+                let _ = crate::iter::Iterator::next(&mut it);
+            }
+            #[kani::proof]
+            #[kani::unwind(6)]
+            fn $nth() {
+                const MAX_LEN: usize = 5;
+                let array_a: [$a; MAX_LEN] = kani::any();
+                let array_b: [$b; MAX_LEN] = kani::any();
+                let mut it = any_zip_iter::<$a, $b>(&array_a, &array_b);
+                let n = kani::any_where(|x: &usize| *x <= MAX_LEN);
+                let _ = crate::iter::Iterator::nth(&mut it, n);
+            }
+            #[kani::proof]
+            fn $back() {
+                const MAX_LEN: usize = 16;
+                let array_a: [$a; MAX_LEN] = kani::any();
+                let array_b: [$b; MAX_LEN] = kani::any();
+                let mut it = any_zip_iter::<$a, $b>(&array_a, &array_b);
+                let _ = crate::iter::DoubleEndedIterator::next_back(&mut it);
+            }
+            #[kani::proof]
+            #[kani::unwind(6)]
+            fn $fold() {
+                const MAX_LEN: usize = 5;
+                let array_a: [$a; MAX_LEN] = kani::any();
+                let array_b: [$b; MAX_LEN] = kani::any();
+                let it = any_zip_iter::<$a, $b>(&array_a, &array_b);
+                let _ = crate::iter::Iterator::fold(it, 0usize, |acc, _| acc.wrapping_add(1));
+            }
+            #[kani::proof]
+            #[kani::unwind(6)]
+            fn $spec() {
+                const MAX_LEN: usize = 5;
+                let array_a: [$a; MAX_LEN] = kani::any();
+                let array_b: [$b; MAX_LEN] = kani::any();
+                let it = any_zip_iter::<$a, $b>(&array_a, &array_b);
+                let _ = SpecFold::spec_fold(it, 0usize, |acc, _| acc.wrapping_add(1));
+            }
+        };
+    }
+    check_zip_safe!(
+        (), (), check_zip_next_unit, check_zip_nth_unit, check_zip_next_back_unit,
+        check_zip_fold_unit, check_zip_spec_fold_unit
+    );
+    check_zip_safe!(
+        u8, u8, check_zip_next_u8, check_zip_nth_u8, check_zip_next_back_u8,
+        check_zip_fold_u8, check_zip_spec_fold_u8
+    );
+    check_zip_safe!(
+        char, u8, check_zip_next_char_u8, check_zip_nth_char_u8, check_zip_next_back_char_u8,
+        check_zip_fold_char_u8, check_zip_spec_fold_char_u8
+    );
+    check_zip_safe!(
+        (char, u8), (u32, i16), check_zip_next_tup, check_zip_nth_tup, check_zip_next_back_tup,
+        check_zip_fold_tup, check_zip_spec_fold_tup
+    );
+}