diff --git a/library/core/src/iter/adapters/array_chunks.rs b/library/core/src/iter/adapters/array_chunks.rs
index 967136288865c..e56c2df945569 100644
--- a/library/core/src/iter/adapters/array_chunks.rs
+++ b/library/core/src/iter/adapters/array_chunks.rs
@@ -3,6 +3,8 @@ use crate::iter::adapters::SourceIter;
 use crate::iter::{
     ByRefSized, FusedIterator, InPlaceIterable, TrustedFused, TrustedRandomAccessNoCoerce,
 };
+#[cfg(kani)]
+use crate::kani;
 use crate::num::NonZero;
 use crate::ops::{ControlFlow, NeverShortCircuit, Try};
 
@@ -230,6 +232,15 @@ where
         let inner_len = self.iter.size();
         let mut i = 0;
         // Use a while loop because (0..len).step_by(N) doesn't optimize well.
+        #[cfg_attr(
+            kani,
+            kani::loop_invariant(
+                N != 0
+                    && self.iter.size() == inner_len
+                    && i <= inner_len
+                    && i % N == 0
+            )
+        )]
         while inner_len - i >= N {
             let chunk = crate::array::from_fn(|local| {
                 // SAFETY: The method consumes the iterator and the loop condition ensures that
@@ -274,3 +285,83 @@ unsafe impl<I: InPlaceIterable + Iterator, const N: usize> InPlaceIterable for A
         }
     };
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+
+    // Harnesses for `next_back_remainder` for ArrayChunks
+    macro_rules! generate_next_back_remainder_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                // Generate an unbounded symbolic length and payload.
+                let end: usize = kani::any();
+                let value: $ty = kani::any();
+
+                // Construct a valid unbounded exact-size, double-ended iterator.
+                let source = (0..end).map(move |position| (position, value));
+
+                // The safe constructor establishes N != 0.
+                let mut chunks = ArrayChunks::<_, 4>::new(source);
+
+                // Exercise the main path, including unwrap_err_unchecked.
+                chunks.next_back_remainder();
+
+                // Exercise the existing-remainder early-return path.
+                chunks.next_back_remainder();
+            }
+        };
+    }
+
+    generate_next_back_remainder_harness!(harness_next_back_remainder_i8, i8);
+    generate_next_back_remainder_harness!(harness_next_back_remainder_i16, i16);
+    generate_next_back_remainder_harness!(harness_next_back_remainder_i32, i32);
+    generate_next_back_remainder_harness!(harness_next_back_remainder_i64, i64);
+    generate_next_back_remainder_harness!(harness_next_back_remainder_i128, i128);
+    generate_next_back_remainder_harness!(harness_next_back_remainder_u8, u8);
+    generate_next_back_remainder_harness!(harness_next_back_remainder_u16, u16);
+    generate_next_back_remainder_harness!(harness_next_back_remainder_u32, u32);
+    generate_next_back_remainder_harness!(harness_next_back_remainder_u64, u64);
+    generate_next_back_remainder_harness!(harness_next_back_remainder_u128, u128);
+    generate_next_back_remainder_harness!(harness_next_back_remainder_array, [u8; 4]);
+    generate_next_back_remainder_harness!(harness_next_back_remainder_bool, bool);
+    generate_next_back_remainder_harness!(harness_next_back_remainder_unit, ());
+
+    // Harnesses for `fold` for ArrayChunks
+    macro_rules! generate_array_chunks_fold_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                // Generate an unbounded symbolic length, payload, and accumulator.
+                let end: usize = kani::any();
+                let value: $ty = kani::any();
+                let init: $ty = kani::any();
+
+                // Map preserves random access while attaching the symbolic payload.
+                let source = (0..end).map(move |position| (position, value));
+
+                // The safe constructor establishes the N != 0 invariant.
+                let chunks = ArrayChunks::<_, 4>::new(source);
+
+                // Directly call the specialized safe function under test.
+                let _ = SpecFold::fold(chunks, init, |accum, _chunk| accum);
+            }
+        };
+    }
+
+    generate_array_chunks_fold_harness!(harness_array_chunks_fold_i8, i8);
+    generate_array_chunks_fold_harness!(harness_array_chunks_fold_i16, i16);
+    generate_array_chunks_fold_harness!(harness_array_chunks_fold_i32, i32);
+    generate_array_chunks_fold_harness!(harness_array_chunks_fold_i64, i64);
+    generate_array_chunks_fold_harness!(harness_array_chunks_fold_i128, i128);
+    generate_array_chunks_fold_harness!(harness_array_chunks_fold_u8, u8);
+    generate_array_chunks_fold_harness!(harness_array_chunks_fold_u16, u16);
+    generate_array_chunks_fold_harness!(harness_array_chunks_fold_u32, u32);
+    generate_array_chunks_fold_harness!(harness_array_chunks_fold_u64, u64);
+    generate_array_chunks_fold_harness!(harness_array_chunks_fold_u128, u128);
+    generate_array_chunks_fold_harness!(harness_array_chunks_fold_array, [u8; 4]);
+    generate_array_chunks_fold_harness!(harness_array_chunks_fold_bool, bool);
+    generate_array_chunks_fold_harness!(harness_array_chunks_fold_unit, ());
+}
diff --git a/library/core/src/iter/adapters/cloned.rs b/library/core/src/iter/adapters/cloned.rs
index 0f05260059880..7b298ffc465ed 100644
--- a/library/core/src/iter/adapters/cloned.rs
+++ b/library/core/src/iter/adapters/cloned.rs
@@ -152,6 +152,8 @@ where
     I: UncheckedIterator<Item = &'a T>,
     T: Clone,
 {
+    #[cfg_attr(kani, kani::requires(self.size_hint().0 != 0))]
+    #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn next_unchecked(&mut self) -> T {
         // SAFETY: `Cloned` is 1:1 with the inner iterator, so if the caller promised
         // that there's an element left, the inner iterator has one too.
@@ -193,3 +195,109 @@ 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::*;
+
+    // Harnesses for `__iterator_get_unchecked` for Cloned.
+    // Use a regular proof because `proof_for_contract` cannot resolve this trait method path.
+    macro_rules! generate_cloned_get_unchecked_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                // Generate a symbolic logical length with no explicit upper bound.
+                let len: usize = kani::any();
+                // Generate a symbolic access index.
+                let idx: usize = kani::any();
+                // Generate an arbitrary element to clone.
+                let value: $ty = kani::any();
+                // Record the index actually received by the inner iterator.
+                let observed_idx = crate::cell::Cell::new(usize::MAX);
+
+                // Build a lazy iterator of length `len` without allocating `len` elements.
+                let source = (0..len).map(|i| {
+                    // Save the index forwarded by the random-access operation.
+                    observed_idx.set(i);
+                    // Make the inner iterator's item type `&T`.
+                    &value
+                });
+                // Construct the target `Cloned<I>` from the inner iterator.
+                let mut iter = Cloned::new(source);
+                // Express the target's `idx < self.size()` precondition.
+                kani::assume(idx < iter.size_hint().0);
+                // Save the iterator size before the call.
+                let size_before = iter.size_hint();
+
+                // Call the target `Cloned<I>` implementation through the trait path.
+                let result =
+                    unsafe { crate::iter::Iterator::__iterator_get_unchecked(&mut iter, idx) };
+
+                // Check that the target forwarded `idx` exactly.
+                assert_eq!(observed_idx.get(), idx);
+                // Check that the returned value is the correct clone of the inner `&T`.
+                assert_eq!(result, value);
+                // Check that random access did not consume the iterator.
+                assert_eq!(iter.size_hint(), size_before);
+            }
+        };
+    }
+
+    generate_cloned_get_unchecked_harness!(harness_cloned_iterator_get_unchecked_i8, i8);
+    generate_cloned_get_unchecked_harness!(harness_cloned_iterator_get_unchecked_i16, i16);
+    generate_cloned_get_unchecked_harness!(harness_cloned_iterator_get_unchecked_i32, i32);
+    generate_cloned_get_unchecked_harness!(harness_cloned_iterator_get_unchecked_i64, i64);
+    generate_cloned_get_unchecked_harness!(harness_cloned_iterator_get_unchecked_i128, i128);
+    generate_cloned_get_unchecked_harness!(harness_cloned_iterator_get_unchecked_u8, u8);
+    generate_cloned_get_unchecked_harness!(harness_cloned_iterator_get_unchecked_u16, u16);
+    generate_cloned_get_unchecked_harness!(harness_cloned_iterator_get_unchecked_u32, u32);
+    generate_cloned_get_unchecked_harness!(harness_cloned_iterator_get_unchecked_u64, u64);
+    generate_cloned_get_unchecked_harness!(harness_cloned_iterator_get_unchecked_u128, u128);
+    generate_cloned_get_unchecked_harness!(harness_cloned_iterator_get_unchecked_array, [u8; 4]);
+    generate_cloned_get_unchecked_harness!(harness_cloned_iterator_get_unchecked_bool, bool);
+    generate_cloned_get_unchecked_harness!(harness_cloned_iterator_get_unchecked_unit, ());
+
+    // Harnesses for `next_unchecked` for Cloned.
+    // Use a regular proof because `proof_for_contract` cannot resolve this trait method path.
+    macro_rules! generate_cloned_next_unchecked_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                // Generate an arbitrary element to clone.
+                let value: $ty = kani::any();
+                // Generate a symbolic logical length with no explicit upper bound.
+                let len: usize = kani::any();
+                // Build an exact-length iterator without allocating `len` elements.
+                let source = crate::iter::repeat_n(&value, len);
+                // Construct the target `Cloned<I>` from the inner iterator.
+                let mut iter = Cloned::new(source);
+
+                // Express the target's `self.size_hint().0 != 0` precondition.
+                kani::assume(iter.size_hint().0 != 0);
+
+                // Call the target `Cloned<I>` implementation through the trait path.
+                let result = unsafe { UncheckedIterator::next_unchecked(&mut iter) };
+
+                // Check that the returned value is the correct clone of the inner `&T`.
+                assert_eq!(result, value);
+                // Check that the call consumed exactly one element.
+                assert_eq!(iter.size_hint(), (len - 1, Some(len - 1)));
+            }
+        };
+    }
+
+    generate_cloned_next_unchecked_harness!(harness_cloned_next_unchecked_i8, i8);
+    generate_cloned_next_unchecked_harness!(harness_cloned_next_unchecked_i16, i16);
+    generate_cloned_next_unchecked_harness!(harness_cloned_next_unchecked_i32, i32);
+    generate_cloned_next_unchecked_harness!(harness_cloned_next_unchecked_i64, i64);
+    generate_cloned_next_unchecked_harness!(harness_cloned_next_unchecked_i128, i128);
+    generate_cloned_next_unchecked_harness!(harness_cloned_next_unchecked_u8, u8);
+    generate_cloned_next_unchecked_harness!(harness_cloned_next_unchecked_u16, u16);
+    generate_cloned_next_unchecked_harness!(harness_cloned_next_unchecked_u32, u32);
+    generate_cloned_next_unchecked_harness!(harness_cloned_next_unchecked_u64, u64);
+    generate_cloned_next_unchecked_harness!(harness_cloned_next_unchecked_u128, u128);
+    generate_cloned_next_unchecked_harness!(harness_cloned_next_unchecked_array, [u8; 4]);
+    generate_cloned_next_unchecked_harness!(harness_cloned_next_unchecked_bool, bool);
+    generate_cloned_next_unchecked_harness!(harness_cloned_next_unchecked_unit, ());
+}
diff --git a/library/core/src/iter/adapters/copied.rs b/library/core/src/iter/adapters/copied.rs
index 3db6c5dafd400..fd4cdd8f27317 100644
--- a/library/core/src/iter/adapters/copied.rs
+++ b/library/core/src/iter/adapters/copied.rs
@@ -284,3 +284,108 @@ 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::*;
+
+    // Harnesses for `__iterator_get_unchecked` for Copied
+    // Use a regular proof because `proof_for_contract` cannot resolve this trait method path.
+    macro_rules! generate_copied_get_unchecked_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                // Generate symbolic inputs with no explicit length bound.
+                let len: usize = kani::any();
+                let idx: usize = kani::any();
+                let value: $ty = kani::any();
+
+                // Record the index received by the inner iterator.
+                let observed_idx = crate::cell::Cell::new(usize::MAX);
+
+                // Build a lazy trusted-random-access iterator yielding `&T`.
+                let source = (0..len).map(|i| {
+                    observed_idx.set(i);
+                    &value
+                });
+                let mut iter = Copied::new(source);
+
+                // Express `idx < self.size()`.
+                kani::assume(idx < iter.size_hint().0);
+                let size_before = iter.size_hint();
+
+                // Call the target `Copied<I>` implementation.
+                let result =
+                    unsafe { crate::iter::Iterator::__iterator_get_unchecked(&mut iter, idx) };
+
+                // Check exact index forwarding.
+                assert_eq!(observed_idx.get(), idx);
+                // Check the copied result.
+                assert_eq!(result, value);
+                // Check that random access did not consume the iterator.
+                assert_eq!(iter.size_hint(), size_before);
+            }
+        };
+    }
+
+    generate_copied_get_unchecked_harness!(harness_copied_iterator_get_unchecked_i8, i8);
+    generate_copied_get_unchecked_harness!(harness_copied_iterator_get_unchecked_i16, i16);
+    generate_copied_get_unchecked_harness!(harness_copied_iterator_get_unchecked_i32, i32);
+    generate_copied_get_unchecked_harness!(harness_copied_iterator_get_unchecked_i64, i64);
+    generate_copied_get_unchecked_harness!(harness_copied_iterator_get_unchecked_i128, i128);
+    generate_copied_get_unchecked_harness!(harness_copied_iterator_get_unchecked_u8, u8);
+    generate_copied_get_unchecked_harness!(harness_copied_iterator_get_unchecked_u16, u16);
+    generate_copied_get_unchecked_harness!(harness_copied_iterator_get_unchecked_u32, u32);
+    generate_copied_get_unchecked_harness!(harness_copied_iterator_get_unchecked_u64, u64);
+    generate_copied_get_unchecked_harness!(harness_copied_iterator_get_unchecked_u128, u128);
+    generate_copied_get_unchecked_harness!(harness_copied_iterator_get_unchecked_array, [u8; 4]);
+    generate_copied_get_unchecked_harness!(harness_copied_iterator_get_unchecked_bool, bool);
+    generate_copied_get_unchecked_harness!(harness_copied_iterator_get_unchecked_unit, ());
+
+    // Harnesses for `spec_next_chunk` for Copied
+    macro_rules! generate_copied_spec_next_chunk_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                // Provide valid symbolic storage for every relevant length around N = 4.
+                let values: [$ty; 5] = kani::any();
+                let slice = kani::slice::any_slice_of_array(&values);
+                let mut iter = slice.iter();
+
+                // Directly call the specialized safe function under test.
+                let _ = <crate::slice::Iter<'_, $ty> as SpecNextChunk<'_, 4, $ty>>::spec_next_chunk(
+                    &mut iter,
+                );
+            }
+        };
+    }
+
+    generate_copied_spec_next_chunk_harness!(harness_copied_spec_next_chunk_i8, i8);
+    generate_copied_spec_next_chunk_harness!(harness_copied_spec_next_chunk_i16, i16);
+    generate_copied_spec_next_chunk_harness!(harness_copied_spec_next_chunk_i32, i32);
+    generate_copied_spec_next_chunk_harness!(harness_copied_spec_next_chunk_i64, i64);
+    generate_copied_spec_next_chunk_harness!(harness_copied_spec_next_chunk_i128, i128);
+    generate_copied_spec_next_chunk_harness!(harness_copied_spec_next_chunk_u8, u8);
+    generate_copied_spec_next_chunk_harness!(harness_copied_spec_next_chunk_u16, u16);
+    generate_copied_spec_next_chunk_harness!(harness_copied_spec_next_chunk_u32, u32);
+    generate_copied_spec_next_chunk_harness!(harness_copied_spec_next_chunk_u64, u64);
+    generate_copied_spec_next_chunk_harness!(harness_copied_spec_next_chunk_u128, u128);
+    generate_copied_spec_next_chunk_harness!(harness_copied_spec_next_chunk_array, [u8; 4]);
+    generate_copied_spec_next_chunk_harness!(harness_copied_spec_next_chunk_bool, bool);
+
+    #[kani::proof]
+    pub fn harness_copied_spec_next_chunk_unit() {
+        // Generate a truly unbounded symbolic length for the zero-sized type.
+        let len: usize = kani::any();
+        let data = crate::ptr::NonNull::<()>::dangling().as_ptr();
+
+        // SAFETY: the pointer is non-null and aligned, and `()` occupies zero bytes.
+        let slice = unsafe { crate::slice::from_raw_parts(data, len) };
+        let mut iter = slice.iter();
+
+        // Directly call the ZST branch of the specialized safe function.
+        let _ =
+            <crate::slice::Iter<'_, ()> as SpecNextChunk<'_, 4, ()>>::spec_next_chunk(&mut iter);
+    }
+}
diff --git a/library/core/src/iter/adapters/enumerate.rs b/library/core/src/iter/adapters/enumerate.rs
index e7e18d178031f..f9a01555e180e 100644
--- a/library/core/src/iter/adapters/enumerate.rs
+++ b/library/core/src/iter/adapters/enumerate.rs
@@ -321,3 +321,71 @@ impl<I: Default> Default for Enumerate<I> {
         Enumerate::new(Default::default())
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+
+    // Harnesses for `__iterator_get_unchecked` for enumerate
+    // Use a regular proof because `proof_for_contract` cannot resolve this trait method path.
+    macro_rules! generate_enumerate_get_unchecked_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                // Generate a symbolic enumeration offset.
+                let count: usize = kani::any();
+                // Generate a symbolic relative access index.
+                let idx: usize = kani::any();
+                // Generate an arbitrary inner item.
+                let value: $ty = kani::any();
+                // Record the absolute position reached by the inner iterator.
+                let observed_position = crate::cell::Cell::new(usize::MAX);
+
+                // Model the remaining range after `count` items without allocating elements.
+                let source = (count..usize::MAX).map(|position| {
+                    // Record which inner element the target actually requested.
+                    observed_position.set(position);
+                    value
+                });
+                // Build a valid `Enumerate` state with a symbolic offset.
+                let mut iter = Enumerate { iter: source, count };
+
+                // Express the target's `idx < self.size()` precondition.
+                kani::assume(idx < iter.size_hint().0);
+                // Save observable iterator state before random access.
+                let count_before = iter.next_index();
+                let size_before = iter.size_hint();
+
+                // Call the target `Enumerate<I>` implementation through the trait path.
+                let result =
+                    unsafe { crate::iter::Iterator::__iterator_get_unchecked(&mut iter, idx) };
+
+                // Check that the relative `idx` reached the correct absolute position.
+                assert_eq!(observed_position.get(), count_before + idx);
+                // Check the enumeration index added by the target.
+                assert_eq!(result.0, count_before + idx);
+                // Check that the inner item was forwarded unchanged.
+                assert_eq!(result.1, value);
+                // Check that random access did not advance the enumeration count.
+                assert_eq!(iter.next_index(), count_before);
+                // Check that random access did not consume the iterator.
+                assert_eq!(iter.size_hint(), size_before);
+            }
+        };
+    }
+
+    generate_enumerate_get_unchecked_harness!(harness_enumerate_get_unchecked_i8, i8);
+    generate_enumerate_get_unchecked_harness!(harness_enumerate_get_unchecked_i16, i16);
+    generate_enumerate_get_unchecked_harness!(harness_enumerate_get_unchecked_i32, i32);
+    generate_enumerate_get_unchecked_harness!(harness_enumerate_get_unchecked_i64, i64);
+    generate_enumerate_get_unchecked_harness!(harness_enumerate_get_unchecked_i128, i128);
+    generate_enumerate_get_unchecked_harness!(harness_enumerate_get_unchecked_u8, u8);
+    generate_enumerate_get_unchecked_harness!(harness_enumerate_get_unchecked_u16, u16);
+    generate_enumerate_get_unchecked_harness!(harness_enumerate_get_unchecked_u32, u32);
+    generate_enumerate_get_unchecked_harness!(harness_enumerate_get_unchecked_u64, u64);
+    generate_enumerate_get_unchecked_harness!(harness_enumerate_get_unchecked_u128, u128);
+    generate_enumerate_get_unchecked_harness!(harness_enumerate_get_unchecked_array, [u8; 4]);
+    generate_enumerate_get_unchecked_harness!(harness_enumerate_get_unchecked_bool, bool);
+    generate_enumerate_get_unchecked_harness!(harness_enumerate_get_unchecked_unit, ());
+}
diff --git a/library/core/src/iter/adapters/filter.rs b/library/core/src/iter/adapters/filter.rs
index dd08cd6f61c4c..c0b502dcdcf1b 100644
--- a/library/core/src/iter/adapters/filter.rs
+++ b/library/core/src/iter/adapters/filter.rs
@@ -5,6 +5,8 @@ use core::ops::ControlFlow;
 use crate::fmt;
 use crate::iter::adapters::SourceIter;
 use crate::iter::{FusedIterator, InPlaceIterable, TrustedFused};
+#[cfg(kani)]
+use crate::kani;
 use crate::num::NonZero;
 use crate::ops::Try;
 
@@ -214,3 +216,41 @@ 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::*;
+
+    // Harnesses for `next_chunk_dropless` for Filter
+    macro_rules! generate_next_chunk_dropless_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            fn $name() {
+                // Use a fixed-size source so the underlying iterator loop is bounded.
+                let values: [$ty; 4] = kani::any();
+                let source: crate::array::IntoIter<$ty, 4> = values.into_iter();
+
+                // Choose each filtering decision nondeterministically.
+                let mut filter = Filter::new(source, |_: &$ty| kani::any());
+
+                // Exercise both the full-chunk and partial-chunk result paths.
+                let _ = filter.next_chunk_dropless::<4>();
+            }
+        };
+    }
+
+    generate_next_chunk_dropless_harness!(harness_next_chunk_dropless_i8, i8);
+    generate_next_chunk_dropless_harness!(harness_next_chunk_dropless_i16, i16);
+    generate_next_chunk_dropless_harness!(harness_next_chunk_dropless_i32, i32);
+    generate_next_chunk_dropless_harness!(harness_next_chunk_dropless_i64, i64);
+    generate_next_chunk_dropless_harness!(harness_next_chunk_dropless_i128, i128);
+    generate_next_chunk_dropless_harness!(harness_next_chunk_dropless_u8, u8);
+    generate_next_chunk_dropless_harness!(harness_next_chunk_dropless_u16, u16);
+    generate_next_chunk_dropless_harness!(harness_next_chunk_dropless_u32, u32);
+    generate_next_chunk_dropless_harness!(harness_next_chunk_dropless_u64, u64);
+    generate_next_chunk_dropless_harness!(harness_next_chunk_dropless_u128, u128);
+    generate_next_chunk_dropless_harness!(harness_next_chunk_dropless_array, [u8; 4]);
+    generate_next_chunk_dropless_harness!(harness_next_chunk_dropless_bool, bool);
+    generate_next_chunk_dropless_harness!(harness_next_chunk_dropless_unit, ());
+}
diff --git a/library/core/src/iter/adapters/filter_map.rs b/library/core/src/iter/adapters/filter_map.rs
index 24ec6b1741ce1..5dfd7b3977a1f 100644
--- a/library/core/src/iter/adapters/filter_map.rs
+++ b/library/core/src/iter/adapters/filter_map.rs
@@ -1,5 +1,7 @@
 use crate::iter::adapters::SourceIter;
 use crate::iter::{FusedIterator, InPlaceIterable, TrustedFused};
+#[cfg(kani)]
+use crate::kani;
 use crate::mem::{ManuallyDrop, MaybeUninit};
 use crate::num::NonZero;
 use crate::ops::{ControlFlow, Try};
@@ -211,3 +213,47 @@ 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::*;
+
+    // Harnesses for `next_chunk` for FilterMap
+    macro_rules! generate_next_chunk_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            fn $name() {
+                // Use a fixed-size source so the underlying iterator loop is bounded.
+                let values: [$ty; 4] = kani::any();
+                let source: crate::array::IntoIter<$ty, 4> = values.into_iter();
+
+                // Choose whether each input is mapped to Some or filtered out as None.
+                let mut filter_map =
+                    FilterMap::new(
+                        source,
+                        |element: $ty| {
+                            if kani::any::<bool>() { Some(element) } else { None }
+                        },
+                    );
+
+                // Exercise both the full-chunk and partial-chunk result paths.
+                let _ = filter_map.next_chunk::<4>();
+            }
+        };
+    }
+
+    generate_next_chunk_harness!(harness_next_chunk_i8, i8);
+    generate_next_chunk_harness!(harness_next_chunk_i16, i16);
+    generate_next_chunk_harness!(harness_next_chunk_i32, i32);
+    generate_next_chunk_harness!(harness_next_chunk_i64, i64);
+    generate_next_chunk_harness!(harness_next_chunk_i128, i128);
+    generate_next_chunk_harness!(harness_next_chunk_u8, u8);
+    generate_next_chunk_harness!(harness_next_chunk_u16, u16);
+    generate_next_chunk_harness!(harness_next_chunk_u32, u32);
+    generate_next_chunk_harness!(harness_next_chunk_u64, u64);
+    generate_next_chunk_harness!(harness_next_chunk_u128, u128);
+    generate_next_chunk_harness!(harness_next_chunk_array, [u8; 4]);
+    generate_next_chunk_harness!(harness_next_chunk_bool, bool);
+    generate_next_chunk_harness!(harness_next_chunk_unit, ());
+}
diff --git a/library/core/src/iter/adapters/fuse.rs b/library/core/src/iter/adapters/fuse.rs
index fcad6168d85cd..86008a4f60e68 100644
--- a/library/core/src/iter/adapters/fuse.rs
+++ b/library/core/src/iter/adapters/fuse.rs
@@ -478,3 +478,69 @@ 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::*;
+
+    // Harnesses for `__iterator_get_unchecked` for Fuse
+    // Use a regular proof because `proof_for_contract` cannot resolve this trait method path.
+    macro_rules! generate_fuse_get_unchecked_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                // Generate a symbolic logical length with no explicit upper bound.
+                let len: usize = kani::any();
+                // Generate a symbolic access index.
+                let idx: usize = kani::any();
+                // Generate an arbitrary inner item.
+                let value: $ty = kani::any();
+                // Record the index actually received by the inner iterator.
+                let observed_idx = crate::cell::Cell::new(usize::MAX);
+
+                // Build a lazy iterator of length `len` without allocating `len` elements.
+                let source = (0..len).map(|position| {
+                    // Record which inner element the target actually requested.
+                    observed_idx.set(position);
+                    value
+                });
+                // Construct an active `Fuse<I>` whose inner state is `Some(source)`.
+                let mut iter = Fuse::new(source);
+
+                // Express the target's `idx < self.size()` precondition.
+                kani::assume(idx < iter.size_hint().0);
+                // Save observable iterator state before random access.
+                let size_before = iter.size_hint();
+                assert!(iter.iter.is_some());
+
+                // Call the target `Fuse<I>` implementation through the trait path.
+                let result =
+                    unsafe { crate::iter::Iterator::__iterator_get_unchecked(&mut iter, idx) };
+
+                // Check that the target forwarded `idx` exactly.
+                assert_eq!(observed_idx.get(), idx);
+                // Check that the inner item was forwarded unchanged.
+                assert_eq!(result, value);
+                // Check that random access kept the inner iterator active.
+                assert!(iter.iter.is_some());
+                // Check that random access did not consume the iterator.
+                assert_eq!(iter.size_hint(), size_before);
+            }
+        };
+    }
+
+    generate_fuse_get_unchecked_harness!(harness_fuse_get_unchecked_i8, i8);
+    generate_fuse_get_unchecked_harness!(harness_fuse_get_unchecked_i16, i16);
+    generate_fuse_get_unchecked_harness!(harness_fuse_get_unchecked_i32, i32);
+    generate_fuse_get_unchecked_harness!(harness_fuse_get_unchecked_i64, i64);
+    generate_fuse_get_unchecked_harness!(harness_fuse_get_unchecked_i128, i128);
+    generate_fuse_get_unchecked_harness!(harness_fuse_get_unchecked_u8, u8);
+    generate_fuse_get_unchecked_harness!(harness_fuse_get_unchecked_u16, u16);
+    generate_fuse_get_unchecked_harness!(harness_fuse_get_unchecked_u32, u32);
+    generate_fuse_get_unchecked_harness!(harness_fuse_get_unchecked_u64, u64);
+    generate_fuse_get_unchecked_harness!(harness_fuse_get_unchecked_u128, u128);
+    generate_fuse_get_unchecked_harness!(harness_fuse_get_unchecked_array, [u8; 4]);
+    generate_fuse_get_unchecked_harness!(harness_fuse_get_unchecked_bool, bool);
+    generate_fuse_get_unchecked_harness!(harness_fuse_get_unchecked_unit, ());
+}
diff --git a/library/core/src/iter/adapters/map.rs b/library/core/src/iter/adapters/map.rs
index bf9f0c48fec3b..9e657f2342c21 100644
--- a/library/core/src/iter/adapters/map.rs
+++ b/library/core/src/iter/adapters/map.rs
@@ -134,6 +134,7 @@ where
 
     #[inline]
     #[requires(idx < self.iter.size_hint().0)]
+    #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> B
     where
         Self: TrustedRandomAccessNoCoerce,
@@ -205,6 +206,7 @@ where
     F: FnMut(I::Item) -> B,
 {
     #[requires(self.iter.size_hint().0 > 0)]
+    #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn next_unchecked(&mut self) -> B {
         // SAFETY: `Map` is 1:1 with the inner iterator, so if the caller promised
         // that there's an element left, the inner iterator has one too.
@@ -245,3 +247,128 @@ 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::*;
+
+    // Harnesses for `__iterator_get_unchecked` for Map
+    // Use a regular proof because `proof_for_contract` cannot resolve this trait method path.
+    macro_rules! generate_map_get_unchecked_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                // Generate a symbolic logical length with no explicit upper bound.
+                let len: usize = kani::any();
+                // Generate a symbolic access index.
+                let idx: usize = kani::any();
+                // Generate arbitrary data captured by the mapping closure.
+                let value: $ty = kani::any();
+                // Record the inner item passed to the mapping closure.
+                let observed_input = crate::cell::Cell::new(usize::MAX);
+                // Count how many times the target invokes the mapping closure.
+                let closure_calls = crate::cell::Cell::new(0usize);
+
+                // Use the range item itself as the observable inner position.
+                let source = 0..len;
+                // Construct the target with a stateful, type-changing closure.
+                let mut iter = Map::new(source, |position| {
+                    observed_input.set(position);
+                    closure_calls.set(closure_calls.get() + 1);
+                    (value, position, closure_calls.get())
+                });
+
+                // Express the target's `idx < self.size()` precondition.
+                kani::assume(idx < iter.size_hint().0);
+                // Save the iterator size before random access.
+                let size_before = iter.size_hint();
+
+                // Call the target `Map<I, F>` implementation through the trait path.
+                let result =
+                    unsafe { crate::iter::Iterator::__iterator_get_unchecked(&mut iter, idx) };
+
+                // Check that the target forwarded `idx` to the inner range exactly.
+                assert_eq!(observed_input.get(), idx);
+                // Check that the target invoked the mapping closure exactly once.
+                assert_eq!(closure_calls.get(), 1);
+                // Check the closure input, captured value, and stateful output.
+                assert_eq!(result, (value, idx, 1));
+                // Check that random access did not consume the iterator.
+                assert_eq!(iter.size_hint(), size_before);
+            }
+        };
+    }
+
+    generate_map_get_unchecked_harness!(harness_map_get_unchecked_i8, i8);
+    generate_map_get_unchecked_harness!(harness_map_get_unchecked_i16, i16);
+    generate_map_get_unchecked_harness!(harness_map_get_unchecked_i32, i32);
+    generate_map_get_unchecked_harness!(harness_map_get_unchecked_i64, i64);
+    generate_map_get_unchecked_harness!(harness_map_get_unchecked_i128, i128);
+    generate_map_get_unchecked_harness!(harness_map_get_unchecked_u8, u8);
+    generate_map_get_unchecked_harness!(harness_map_get_unchecked_u16, u16);
+    generate_map_get_unchecked_harness!(harness_map_get_unchecked_u32, u32);
+    generate_map_get_unchecked_harness!(harness_map_get_unchecked_u64, u64);
+    generate_map_get_unchecked_harness!(harness_map_get_unchecked_u128, u128);
+    generate_map_get_unchecked_harness!(harness_map_get_unchecked_array, [u8; 4]);
+    generate_map_get_unchecked_harness!(harness_map_get_unchecked_bool, bool);
+    generate_map_get_unchecked_harness!(harness_map_get_unchecked_unit, ());
+
+    // Harnesses for `next_unchecked` for Map
+    // Use a regular proof because `proof_for_contract` cannot resolve this trait method path.
+    macro_rules! generate_map_next_unchecked_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                // Generate arbitrary data captured by the mapping closure.
+                let value: $ty = kani::any();
+                // Generate an arbitrary inner item.
+                let inner_value: usize = kani::any();
+                // Generate a symbolic logical length with no explicit upper bound.
+                let len: usize = kani::any();
+                // Record the inner item passed to the mapping closure.
+                let observed_input = crate::cell::Cell::new(usize::MAX);
+                // Count how many times the target invokes the mapping closure.
+                let closure_calls = crate::cell::Cell::new(0usize);
+
+                // Build an exact-length iterator without allocating `len` elements.
+                let source = crate::iter::repeat_n(inner_value, len);
+                // Construct the target with a stateful, type-changing closure.
+                let mut iter = Map::new(source, |item| {
+                    observed_input.set(item);
+                    closure_calls.set(closure_calls.get() + 1);
+                    (value, item, closure_calls.get())
+                });
+
+                // Express the target's non-empty precondition.
+                kani::assume(iter.size_hint().0 > 0);
+
+                // Call the target `Map<I, F>` implementation through the trait path.
+                let result = unsafe { UncheckedIterator::next_unchecked(&mut iter) };
+
+                // Check that the closure received the consumed inner item.
+                assert_eq!(observed_input.get(), inner_value);
+                // Check that the target invoked the mapping closure exactly once.
+                assert_eq!(closure_calls.get(), 1);
+                // Check the closure input, captured value, and stateful output.
+                assert_eq!(result, (value, inner_value, 1));
+                // Check that the target consumed exactly one inner element.
+                assert_eq!(iter.size_hint(), (len - 1, Some(len - 1)));
+            }
+        };
+    }
+
+    generate_map_next_unchecked_harness!(harness_map_next_unchecked_i8, i8);
+    generate_map_next_unchecked_harness!(harness_map_next_unchecked_i16, i16);
+    generate_map_next_unchecked_harness!(harness_map_next_unchecked_i32, i32);
+    generate_map_next_unchecked_harness!(harness_map_next_unchecked_i64, i64);
+    generate_map_next_unchecked_harness!(harness_map_next_unchecked_i128, i128);
+    generate_map_next_unchecked_harness!(harness_map_next_unchecked_u8, u8);
+    generate_map_next_unchecked_harness!(harness_map_next_unchecked_u16, u16);
+    generate_map_next_unchecked_harness!(harness_map_next_unchecked_u32, u32);
+    generate_map_next_unchecked_harness!(harness_map_next_unchecked_u64, u64);
+    generate_map_next_unchecked_harness!(harness_map_next_unchecked_u128, u128);
+    generate_map_next_unchecked_harness!(harness_map_next_unchecked_array, [u8; 4]);
+    generate_map_next_unchecked_harness!(harness_map_next_unchecked_bool, bool);
+    generate_map_next_unchecked_harness!(harness_map_next_unchecked_unit, ());
+}
diff --git a/library/core/src/iter/adapters/map_windows.rs b/library/core/src/iter/adapters/map_windows.rs
index 536251a137da0..b02af53890312 100644
--- a/library/core/src/iter/adapters/map_windows.rs
+++ b/library/core/src/iter/adapters/map_windows.rs
@@ -1,4 +1,6 @@
 use crate::iter::FusedIterator;
+#[cfg(kani)]
+use crate::kani;
 use crate::mem::MaybeUninit;
 use crate::ub_checks::Invariant;
 use crate::{fmt, ptr};
@@ -297,3 +299,158 @@ 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::*;
+
+    fn any_buffer<T: Copy + kani::Arbitrary, const N: usize>() -> (Buffer<T, N>, [T; N]) {
+        // Symbolize a valid starting position for the active window.
+        let start = kani::any_where(|start: &usize| *start <= N);
+
+        // Symbolize the values that occupy the active window.
+        let values: [T; N] = kani::any();
+        let mut storage = [[MaybeUninit::uninit(); N]; 2];
+
+        // Initialize exactly storage[start .. start + N] without raw pointers.
+        for offset in 0..N {
+            let index = start + offset;
+            if index < N {
+                storage[0][index].write(values[offset]);
+            } else {
+                storage[1][index - N].write(values[offset]);
+            }
+        }
+
+        (Buffer { buffer: storage, start }, values)
+    }
+
+    // Harnesses for `as_array_ref` for Buffer
+    macro_rules! generate_buffer_as_array_ref_harness {
+        ($name:ident, $ty:ty, $n:expr) => {
+            #[kani::proof]
+            fn $name() {
+                // Build a symbolic Buffer satisfying its representation invariant.
+                let (buffer, expected) = any_buffer::<$ty, $n>();
+
+                // Call the safe function under test.
+                let window = buffer.as_array_ref();
+            }
+        };
+    }
+
+    generate_buffer_as_array_ref_harness!(harness_buffer_as_array_ref_u8_n1, u8, 1);
+    generate_buffer_as_array_ref_harness!(harness_buffer_as_array_ref_u8_n2, u8, 2);
+    generate_buffer_as_array_ref_harness!(harness_buffer_as_array_ref_u8_n4, u8, 4);
+    generate_buffer_as_array_ref_harness!(harness_buffer_as_array_ref_u16, u16, 2);
+    generate_buffer_as_array_ref_harness!(harness_buffer_as_array_ref_u32, u32, 2);
+    generate_buffer_as_array_ref_harness!(harness_buffer_as_array_ref_u64, u64, 2);
+    generate_buffer_as_array_ref_harness!(harness_buffer_as_array_ref_u128, u128, 2);
+    generate_buffer_as_array_ref_harness!(harness_buffer_as_array_ref_i8, i8, 2);
+    generate_buffer_as_array_ref_harness!(harness_buffer_as_array_ref_i16, i16, 2);
+    generate_buffer_as_array_ref_harness!(harness_buffer_as_array_ref_i32, i32, 2);
+    generate_buffer_as_array_ref_harness!(harness_buffer_as_array_ref_i64, i64, 2);
+    generate_buffer_as_array_ref_harness!(harness_buffer_as_array_ref_i128, i128, 2);
+    generate_buffer_as_array_ref_harness!(harness_buffer_as_array_ref_bool, bool, 2);
+    generate_buffer_as_array_ref_harness!(harness_buffer_as_array_ref_unit, (), 2);
+    generate_buffer_as_array_ref_harness!(harness_buffer_as_array_ref_array, [u8; 4], 2);
+
+    // Harnesses for `as_uninit_array_mut` for Buffer
+    macro_rules! generate_buffer_as_uninit_array_mut_harness {
+        ($name:ident, $ty:ty, $n:expr) => {
+            #[kani::proof]
+            fn $name() {
+                // Build a valid symbolic Buffer without raw pointers.
+                let (mut buffer, _) = any_buffer::<$ty, $n>();
+
+                // Symbolize a fully initialized replacement window.
+                let replacement: [$ty; $n] = kani::any();
+
+                // Write through the safe function's returned MaybeUninit reference.
+                buffer.as_uninit_array_mut().write(replacement);
+            }
+        };
+    }
+
+    generate_buffer_as_uninit_array_mut_harness!(harness_buffer_as_uninit_array_mut_u8_n1, u8, 1);
+    generate_buffer_as_uninit_array_mut_harness!(harness_buffer_as_uninit_array_mut_u8_n2, u8, 2);
+    generate_buffer_as_uninit_array_mut_harness!(harness_buffer_as_uninit_array_mut_u8_n4, u8, 4);
+    generate_buffer_as_uninit_array_mut_harness!(harness_buffer_as_uninit_array_mut_u16, u16, 2);
+    generate_buffer_as_uninit_array_mut_harness!(harness_buffer_as_uninit_array_mut_u32, u32, 2);
+    generate_buffer_as_uninit_array_mut_harness!(harness_buffer_as_uninit_array_mut_u64, u64, 2);
+    generate_buffer_as_uninit_array_mut_harness!(harness_buffer_as_uninit_array_mut_u128, u128, 2);
+    generate_buffer_as_uninit_array_mut_harness!(harness_buffer_as_uninit_array_mut_i8, i8, 2);
+    generate_buffer_as_uninit_array_mut_harness!(harness_buffer_as_uninit_array_mut_i16, i16, 2);
+    generate_buffer_as_uninit_array_mut_harness!(harness_buffer_as_uninit_array_mut_i32, i32, 2);
+    generate_buffer_as_uninit_array_mut_harness!(harness_buffer_as_uninit_array_mut_i64, i64, 2);
+    generate_buffer_as_uninit_array_mut_harness!(harness_buffer_as_uninit_array_mut_i128, i128, 2);
+    generate_buffer_as_uninit_array_mut_harness!(harness_buffer_as_uninit_array_mut_bool, bool, 2);
+    generate_buffer_as_uninit_array_mut_harness!(harness_buffer_as_uninit_array_mut_unit, (), 2);
+    generate_buffer_as_uninit_array_mut_harness!(
+        harness_buffer_as_uninit_array_mut_array,
+        [u8; 4],
+        2
+    );
+
+    // Harnesses for `push` for Buffer.
+    macro_rules! generate_buffer_push_harness {
+        ($name:ident, $ty:ty, $n:expr) => {
+            #[kani::proof]
+            fn $name() {
+                // Build a valid Buffer with a symbolic active-window position.
+                let (mut buffer, before) = any_buffer::<$ty, $n>();
+                // Symbolize the item appended to the window.
+                let next: $ty = kani::any();
+                // Call the safe function under test.
+                buffer.push(next);
+            }
+        };
+    }
+
+    generate_buffer_push_harness!(harness_buffer_push_u8_n1, u8, 1);
+    generate_buffer_push_harness!(harness_buffer_push_u8_n2, u8, 2);
+    generate_buffer_push_harness!(harness_buffer_push_u8_n4, u8, 4);
+    generate_buffer_push_harness!(harness_buffer_push_u16, u16, 2);
+    generate_buffer_push_harness!(harness_buffer_push_u32, u32, 2);
+    generate_buffer_push_harness!(harness_buffer_push_u64, u64, 2);
+    generate_buffer_push_harness!(harness_buffer_push_u128, u128, 2);
+    generate_buffer_push_harness!(harness_buffer_push_i8, i8, 2);
+    generate_buffer_push_harness!(harness_buffer_push_i16, i16, 2);
+    generate_buffer_push_harness!(harness_buffer_push_i32, i32, 2);
+    generate_buffer_push_harness!(harness_buffer_push_i64, i64, 2);
+    generate_buffer_push_harness!(harness_buffer_push_i128, i128, 2);
+    generate_buffer_push_harness!(harness_buffer_push_bool, bool, 2);
+    generate_buffer_push_harness!(harness_buffer_push_unit, (), 2);
+    generate_buffer_push_harness!(harness_buffer_push_array, [u8; 4], 2);
+
+    // Harnesses for `Drop::drop` for Buffer.
+    macro_rules! generate_buffer_drop_harness {
+        ($name:ident, $ty:ty, $n:expr) => {
+            #[kani::proof]
+            fn $name() {
+                // Build a valid Buffer with a symbolic active-window position.
+                let (buffer, _) = any_buffer::<$ty, $n>();
+
+                // Invoke Buffer::drop through the safe drop function.
+                crate::mem::drop(buffer);
+            }
+        };
+    }
+
+    generate_buffer_drop_harness!(harness_buffer_drop_u8_n1, u8, 1);
+    generate_buffer_drop_harness!(harness_buffer_drop_u8_n2, u8, 2);
+    generate_buffer_drop_harness!(harness_buffer_drop_u8_n4, u8, 4);
+    generate_buffer_drop_harness!(harness_buffer_drop_u16, u16, 2);
+    generate_buffer_drop_harness!(harness_buffer_drop_u32, u32, 2);
+    generate_buffer_drop_harness!(harness_buffer_drop_u64, u64, 2);
+    generate_buffer_drop_harness!(harness_buffer_drop_u128, u128, 2);
+    generate_buffer_drop_harness!(harness_buffer_drop_i8, i8, 2);
+    generate_buffer_drop_harness!(harness_buffer_drop_i16, i16, 2);
+    generate_buffer_drop_harness!(harness_buffer_drop_i32, i32, 2);
+    generate_buffer_drop_harness!(harness_buffer_drop_i64, i64, 2);
+    generate_buffer_drop_harness!(harness_buffer_drop_i128, i128, 2);
+    generate_buffer_drop_harness!(harness_buffer_drop_bool, bool, 2);
+    generate_buffer_drop_harness!(harness_buffer_drop_unit, (), 2);
+    generate_buffer_drop_harness!(harness_buffer_drop_array, [u8; 4], 2);
+}
diff --git a/library/core/src/iter/adapters/skip.rs b/library/core/src/iter/adapters/skip.rs
index ac3cc4c4f1152..c09117bc78ad3 100644
--- a/library/core/src/iter/adapters/skip.rs
+++ b/library/core/src/iter/adapters/skip.rs
@@ -180,6 +180,18 @@ where
         //   before something is written into the storage used by the prefix
         unsafe {
             if Self::MAY_HAVE_SIDE_EFFECT && idx == 0 {
+                #[cfg(kani)]
+                let inner_size_hint = self.iter.size_hint();
+                // The outer precondition and `idx == 0` imply `self.n < inner_size_hint.0`.
+                // Random access may mutate the inner iterator, but it must preserve its size.
+                #[cfg_attr(
+                    kani,
+                    kani::loop_invariant(
+                        kani::index <= self.n
+                            && self.n < inner_size_hint.0
+                            && self.iter.size_hint() == inner_size_hint
+                    )
+                )]
                 for skipped_idx in 0..self.n {
                     drop(try_get_unchecked(&mut self.iter, skipped_idx));
                 }
@@ -293,3 +305,136 @@ 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::*;
+
+    // Harnesses for `__iterator_get_unchecked` for Skip
+    // Use a regular proof because `proof_for_contract` cannot resolve this trait method path.
+    macro_rules! generate_skip_get_unchecked_unbounded_harness {
+        ($name:ident) => {
+            #[kani::proof]
+            pub fn $name() {
+                // Generate a symbolic pending skip count.
+                let n: usize = kani::any();
+                // Generate a symbolic index in the shortened iterator.
+                let idx: usize = kani::any();
+
+                // Use a maximal lazy range with no random-access side effects.
+                let source = 0..usize::MAX;
+                // Construct the target with a symbolic skip offset.
+                let mut iter = Skip::new(source, n);
+
+                // Express the target's `idx < self.size()` precondition.
+                kani::assume(idx < iter.size_hint().0);
+                // Save observable iterator state before random access.
+                let n_before = iter.n;
+                let size_before = iter.size_hint();
+
+                // Call the target `Skip<I>` implementation through the trait path.
+                let result =
+                    unsafe { crate::iter::Iterator::__iterator_get_unchecked(&mut iter, idx) };
+
+                // Check that `Skip` translated the outer index to `n + idx`.
+                assert_eq!(result, n + idx);
+                // Check that random access did not consume the pending skip count.
+                assert_eq!(iter.n, n_before);
+                // Check that random access did not consume the iterator.
+                assert_eq!(iter.size_hint(), size_before);
+            }
+        };
+    }
+
+    // Cover Copy item types with core's non-side-effecting array iterator
+    macro_rules! generate_skip_get_unchecked_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                // Generate a symbolic pending skip count and outer index.
+                let n: usize = kani::any();
+                let idx: usize = kani::any();
+                // Generate four independent symbolic values of the selected item type.
+                let values: [$ty; 4] = kani::any();
+                // Keep a Copy snapshot for checking the translated index.
+                let expected_values = values;
+
+                // Use core's generic trusted-random-access iterator with no side effects.
+                let source: crate::array::IntoIter<$ty, 4> = values.into_iter();
+                // Construct the target with a symbolic skip offset.
+                let mut iter = Skip::new(source, n);
+
+                // Express the target's `idx < self.size()` precondition.
+                kani::assume(idx < iter.size_hint().0);
+                // The precondition guarantees that `n + idx` indexes the original array.
+                let expected = expected_values[n + idx];
+                // Save observable iterator state before random access.
+                let n_before = iter.n;
+                let size_before = iter.size_hint();
+
+                // Call the target `Skip<I>` implementation through the trait path.
+                let result =
+                    unsafe { crate::iter::Iterator::__iterator_get_unchecked(&mut iter, idx) };
+
+                // Check that `Skip` selected the original element at `n + idx`.
+                assert_eq!(result, expected);
+                // Check that random access did not consume the adapter state.
+                assert_eq!(iter.n, n_before);
+                assert_eq!(iter.size_hint(), size_before);
+            }
+        };
+    }
+
+    // Cover side-effecting path
+    macro_rules! generate_skip_get_unchecked_side_effect_harness {
+        ($name:ident) => {
+            #[kani::proof]
+            pub fn $name() {
+                // Generate a symbolic pending skip count.
+                let n: usize = kani::any();
+                // Generate a symbolic index in the shortened iterator.
+                let idx: usize = kani::any();
+
+                // `Map` sets `MAY_HAVE_SIDE_EFFECT = true` for every mapping closure,
+                // so this selects `Skip`'s side-effecting random-access branch.
+                // Keep the closure stateless because this harness does not track exact effects.
+                let source = (0..usize::MAX).map(|position| position);
+                // Construct the target with a symbolic skip offset.
+                let mut iter = Skip::new(source, n);
+
+                // Express the target's `idx < self.size()` precondition.
+                kani::assume(idx < iter.size_hint().0);
+                // Save observable iterator state before random access.
+                let n_before = iter.n;
+                let size_before = iter.size_hint();
+
+                // Call the target `Skip<I>` implementation through the trait path.
+                let result =
+                    unsafe { crate::iter::Iterator::__iterator_get_unchecked(&mut iter, idx) };
+
+                // Check that `Skip` translated the outer index to `n + idx`.
+                assert_eq!(result, n + idx);
+                // Check that random access did not consume the adapter state.
+                assert_eq!(iter.n, n_before);
+                assert_eq!(iter.size_hint(), size_before);
+            }
+        };
+    }
+
+    generate_skip_get_unchecked_unbounded_harness!(harness_skip_get_unchecked_unbounded);
+    generate_skip_get_unchecked_harness!(harness_skip_get_unchecked_i8, i8);
+    generate_skip_get_unchecked_harness!(harness_skip_get_unchecked_i16, i16);
+    generate_skip_get_unchecked_harness!(harness_skip_get_unchecked_i32, i32);
+    generate_skip_get_unchecked_harness!(harness_skip_get_unchecked_i64, i64);
+    generate_skip_get_unchecked_harness!(harness_skip_get_unchecked_i128, i128);
+    generate_skip_get_unchecked_harness!(harness_skip_get_unchecked_u8, u8);
+    generate_skip_get_unchecked_harness!(harness_skip_get_unchecked_u16, u16);
+    generate_skip_get_unchecked_harness!(harness_skip_get_unchecked_u32, u32);
+    generate_skip_get_unchecked_harness!(harness_skip_get_unchecked_u64, u64);
+    generate_skip_get_unchecked_harness!(harness_skip_get_unchecked_u128, u128);
+    generate_skip_get_unchecked_harness!(harness_skip_get_unchecked_array, [u8; 4]);
+    generate_skip_get_unchecked_harness!(harness_skip_get_unchecked_bool, bool);
+    generate_skip_get_unchecked_harness!(harness_skip_get_unchecked_unit, ());
+    generate_skip_get_unchecked_side_effect_harness!(harness_skip_get_unchecked_side_effect);
+}
diff --git a/library/core/src/iter/adapters/step_by.rs b/library/core/src/iter/adapters/step_by.rs
index 32604a07ca40c..bca59ec4117e8 100644
--- a/library/core/src/iter/adapters/step_by.rs
+++ b/library/core/src/iter/adapters/step_by.rs
@@ -589,3 +589,22 @@ 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::*;
+
+    // Harness for `original_step` for StepBy.
+    #[kani::proof]
+    fn harness_step_by_original_step() {
+        // StepBy::new requires a nonzero step.
+        let step = kani::any_where(|step: &usize| *step != 0);
+
+        // The inner iterator is irrelevant to original_step.
+        let step_by = StepBy::new((), step);
+
+        // Call the safe function under test.
+        let _ = step_by.original_step();
+    }
+}
diff --git a/library/core/src/iter/adapters/take.rs b/library/core/src/iter/adapters/take.rs
index b96335f415257..2a4c98658bf87 100644
--- a/library/core/src/iter/adapters/take.rs
+++ b/library/core/src/iter/adapters/take.rs
@@ -1,6 +1,8 @@
 use crate::cmp;
 use crate::iter::adapters::SourceIter;
 use crate::iter::{FusedIterator, InPlaceIterable, TrustedFused, TrustedLen, TrustedRandomAccess};
+#[cfg(kani)]
+use crate::kani;
 use crate::num::NonZero;
 use crate::ops::{ControlFlow, Try};
 
@@ -299,6 +301,7 @@ impl<I: Iterator + TrustedRandomAccess> SpecTake for Take<I> {
     {
         let mut acc = init;
         let end = self.n.min(self.iter.size());
+        #[cfg_attr(kani, kani::loop_invariant(end <= self.iter.size()))]
         for i in 0..end {
             // SAFETY: i < end <= self.iter.size() and we discard the iterator at the end
             let val = unsafe { self.iter.__iterator_get_unchecked(i) };
@@ -310,6 +313,7 @@ impl<I: Iterator + TrustedRandomAccess> SpecTake for Take<I> {
     #[inline]
     fn spec_for_each<F: FnMut(Self::Item)>(mut self, mut f: F) {
         let end = self.n.min(self.iter.size());
+        #[cfg_attr(kani, kani::loop_invariant(end <= self.iter.size()))]
         for i in 0..end {
             // SAFETY: i < end <= self.iter.size() and we discard the iterator at the end
             let val = unsafe { self.iter.__iterator_get_unchecked(i) };
@@ -374,3 +378,81 @@ 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::*;
+
+    // Harnesses for `spec_fold` for Take.
+    macro_rules! generate_take_spec_fold_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            fn $name() {
+                // Symbolize the logical iterator length without an explicit bound.
+                let len: usize = kani::any();
+
+                // Symbolize the take count independently of the iterator length.
+                let n: usize = kani::any();
+
+                // Map retains TrustedRandomAccess while generalizing the item type.
+                let value: $ty = kani::any();
+                let source = (0..len).map(move |_| value);
+                let taken = Take::new(source, n);
+
+                // Call the specialized safe function under test.
+                SpecTake::spec_fold(taken, (), |(), _item| ());
+            }
+        };
+    }
+
+    generate_take_spec_fold_harness!(harness_take_spec_fold_i8, i8);
+    generate_take_spec_fold_harness!(harness_take_spec_fold_i16, i16);
+    generate_take_spec_fold_harness!(harness_take_spec_fold_i32, i32);
+    generate_take_spec_fold_harness!(harness_take_spec_fold_i64, i64);
+    generate_take_spec_fold_harness!(harness_take_spec_fold_i128, i128);
+    generate_take_spec_fold_harness!(harness_take_spec_fold_u8, u8);
+    generate_take_spec_fold_harness!(harness_take_spec_fold_u16, u16);
+    generate_take_spec_fold_harness!(harness_take_spec_fold_u32, u32);
+    generate_take_spec_fold_harness!(harness_take_spec_fold_u64, u64);
+    generate_take_spec_fold_harness!(harness_take_spec_fold_u128, u128);
+    generate_take_spec_fold_harness!(harness_take_spec_fold_bool, bool);
+    generate_take_spec_fold_harness!(harness_take_spec_fold_unit, ());
+    generate_take_spec_fold_harness!(harness_take_spec_fold_array, [u8; 4]);
+
+    // Harnesses for `spec_for_each` for Take.
+    macro_rules! generate_take_spec_for_each_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            fn $name() {
+                // Symbolize the logical iterator length without an explicit bound.
+                let len: usize = kani::any();
+
+                // Symbolize the take count independently of the iterator length.
+                let n: usize = kani::any();
+
+                // Map retains TrustedRandomAccess while generalizing the item type.
+                let value: $ty = kani::any();
+                let source = (0..len).map(move |_| value);
+                let taken = Take::new(source, n);
+
+                // Call the specialized safe function under test.
+                SpecTake::spec_for_each(taken, |_item| ());
+            }
+        };
+    }
+
+    generate_take_spec_for_each_harness!(harness_take_spec_for_each_i8, i8);
+    generate_take_spec_for_each_harness!(harness_take_spec_for_each_i16, i16);
+    generate_take_spec_for_each_harness!(harness_take_spec_for_each_i32, i32);
+    generate_take_spec_for_each_harness!(harness_take_spec_for_each_i64, i64);
+    generate_take_spec_for_each_harness!(harness_take_spec_for_each_i128, i128);
+    generate_take_spec_for_each_harness!(harness_take_spec_for_each_u8, u8);
+    generate_take_spec_for_each_harness!(harness_take_spec_for_each_u16, u16);
+    generate_take_spec_for_each_harness!(harness_take_spec_for_each_u32, u32);
+    generate_take_spec_for_each_harness!(harness_take_spec_for_each_u64, u64);
+    generate_take_spec_for_each_harness!(harness_take_spec_for_each_u128, u128);
+    generate_take_spec_for_each_harness!(harness_take_spec_for_each_bool, bool);
+    generate_take_spec_for_each_harness!(harness_take_spec_for_each_unit, ());
+    generate_take_spec_for_each_harness!(harness_take_spec_for_each_array, [u8; 4]);
+}
diff --git a/library/core/src/iter/adapters/zip.rs b/library/core/src/iter/adapters/zip.rs
index e39f1535bd95d..242a84d406d59 100644
--- a/library/core/src/iter/adapters/zip.rs
+++ b/library/core/src/iter/adapters/zip.rs
@@ -28,6 +28,23 @@ impl<A: Iterator, B: Iterator> Zip<A, B> {
         ZipImpl::new(a, b)
     }
     fn super_nth(&mut self, mut n: usize) -> Option<(A::Item, B::Item)> {
+        #[cfg_attr(
+            kani,
+            kani::loop_invariant(
+                self.index <= self.len
+                    && self.len <= self.a.size_hint().0
+                    && self.len <= self.b.size_hint().0
+            )
+        )]
+        #[cfg_attr(
+            kani,
+            kani::loop_modifies(
+                &mut self.a,
+                &mut self.b,
+                &mut self.index,
+                &mut n
+            )
+        )]
         while let Some(x) = Iterator::next(self) {
             if n == 0 {
                 return Some(x);
@@ -270,6 +287,7 @@ where
     }
 
     #[inline]
+    #[cfg_attr(kani, kani::requires(idx < TrustedRandomAccessNoCoerce::size(self)))]
     #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn get_unchecked(&mut self, idx: usize) -> <Self as Iterator>::Item {
         let idx = self.index + idx;
@@ -285,6 +303,18 @@ where
     {
         let mut accum = init;
         let len = ZipImpl::size_hint(&self).0;
+        #[cfg_attr(
+            kani,
+            kani::loop_invariant(
+                kani::index <= len
+                    && len <= ZipImpl::size_hint(&self).0
+                    && self.index <= self.a.size()
+                    && len <= self.a.size() - self.index
+                    && self.index <= self.b.size()
+                    && len <= self.b.size() - self.index
+            )
+        )]
+        #[cfg_attr(kani, kani::loop_modifies(&self, &accum, &f))]
         for i in 0..len {
             // SAFETY: since Self: TrustedRandomAccessNoCoerce we can trust the size-hint to
             // calculate the length and then use that to do unchecked iteration.
@@ -334,6 +364,19 @@ where
     fn nth(&mut self, n: usize) -> Option<Self::Item> {
         let delta = cmp::min(n, self.len - self.index);
         let end = self.index + delta;
+        #[cfg_attr(
+            kani,
+            kani::loop_invariant(
+                self.index <= end
+                    && end <= self.len
+                    && self.len <= self.a.size()
+                    && self.len <= self.b.size()
+            )
+        )]
+        #[cfg_attr(
+            kani,
+            kani::loop_modifies(&mut self.index, &mut self.a, &mut self.b)
+        )]
         while self.index < end {
             let i = self.index;
             // since get_unchecked executes code which can panic we increment the counters beforehand
@@ -669,6 +712,8 @@ impl<A: TrustedLen, B: TrustedLen> SpecFold for Zip<A, B> {
         F: FnMut(Acc, Self::Item) -> Acc,
     {
         let mut accum = init;
+
+        #[cfg(not(kani))]
         loop {
             let (upper, more) = if let Some(upper) = ZipImpl::size_hint(&self).1 {
                 (upper, false)
@@ -689,6 +734,380 @@ impl<A: TrustedLen, B: TrustedLen> SpecFold for Zip<A, B> {
                 break;
             }
         }
+
+        // Loop stub: choose one arbitrary iteration from a chunk
+        // and preserve the unchecked-access safety check without a
+        // writeset over generic iterator structs.
+        #[cfg(kani)]
+        {
+            let upper = ZipImpl::size_hint(&self).1.unwrap_or(usize::MAX);
+            if upper != 0 {
+                let index: usize = kani::any();
+                kani::assume(index < upper);
+                let pair = unsafe {
+                    (self.a.nth(index).unwrap_unchecked(), self.b.nth(index).unwrap_unchecked())
+                };
+                accum = f(accum, pair);
+            }
+        }
+
         accum
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+
+    // Harnesses for `__iterator_get_unchecked` for ZipImpl.
+    // Use a regular proof because `proof_for_contract` cannot resolve this trait method path.
+    // Use core's non-side-effecting `Copied<slice::Iter<T>>` for item-type coverage.
+    macro_rules! generate_zip_iterator_get_unchecked_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                // Generate independent symbolic values for both sides.
+                let left: [$ty; 4] = kani::any();
+                let right: [$ty; 4] = kani::any();
+                // Generate a symbolic reachable offset and remaining-relative index.
+                let index: usize = kani::any();
+                let idx: usize = kani::any();
+
+                // `Copied<slice::Iter<T>>` implements full trusted random access.
+                let mut zip = Zip::new(left.iter().copied(), right.iter().copied());
+                // Specialized `next` changes only `index`, so this models a reachable state.
+                kani::assume(index <= zip.len);
+                zip.index = index;
+
+                // Express the target's `idx < self.size()` precondition.
+                kani::assume(idx < TrustedRandomAccessNoCoerce::size(&zip));
+                let absolute_idx = index + idx;
+                let expected = (left[absolute_idx], right[absolute_idx]);
+                // Save observable `Zip` state before random access.
+                let index_before = zip.index;
+                let len_before = zip.len;
+                let size_before = Iterator::size_hint(&zip);
+
+                // Call the outer `Iterator` target through its trait path.
+                let result = unsafe { Iterator::__iterator_get_unchecked(&mut zip, idx) };
+
+                // Check both values at the translated absolute index.
+                assert_eq!(result, expected);
+                // Check that random access did not consume the zipped iterator.
+                assert_eq!(zip.index, index_before);
+                assert_eq!(zip.len, len_before);
+                assert_eq!(Iterator::size_hint(&zip), size_before);
+            }
+        };
+    }
+
+    #[kani::proof]
+    fn harness_zip_iterator_get_unchecked_unbounded() {
+        // Generate independent symbolic lengths for both inner iterators.
+        let left_len: usize = kani::any();
+        let right_len: usize = kani::any();
+        // Generate a symbolic reachable offset in the specialized `Zip` state.
+        let index: usize = kani::any();
+        // Generate a symbolic index relative to the remaining zipped iterator.
+        let idx: usize = kani::any();
+
+        // Use core ranges to keep both input lengths unbounded by a harness constant.
+        let mut zip = Zip::new(0..left_len, 0..right_len);
+        // Specialized `next` reaches this state by changing only `index`.
+        kani::assume(index <= zip.len);
+        zip.index = index;
+
+        // Express the target's `idx < self.size()` precondition.
+        kani::assume(idx < TrustedRandomAccessNoCoerce::size(&zip));
+        let absolute_idx = index + idx;
+        // Save all observable iterator state before random access.
+        let index_before = zip.index;
+        let len_before = zip.len;
+        let left_size_before = zip.a.size_hint();
+        let right_size_before = zip.b.size_hint();
+        let size_before = Iterator::size_hint(&zip);
+
+        // Call the outer `Iterator` target, which delegates to `ZipImpl`.
+        let result = unsafe { Iterator::__iterator_get_unchecked(&mut zip, idx) };
+
+        // Check that both sides received the same translated absolute index.
+        assert_eq!(result, (absolute_idx, absolute_idx));
+        // Check that random access did not consume or resize any iterator state.
+        assert_eq!(zip.index, index_before);
+        assert_eq!(zip.len, len_before);
+        assert_eq!(zip.a.size_hint(), left_size_before);
+        assert_eq!(zip.b.size_hint(), right_size_before);
+        assert_eq!(Iterator::size_hint(&zip), size_before);
+    }
+
+    generate_zip_iterator_get_unchecked_harness!(harness_zip_iterator_get_unchecked_i8, i8);
+    generate_zip_iterator_get_unchecked_harness!(harness_zip_iterator_get_unchecked_i16, i16);
+    generate_zip_iterator_get_unchecked_harness!(harness_zip_iterator_get_unchecked_i32, i32);
+    generate_zip_iterator_get_unchecked_harness!(harness_zip_iterator_get_unchecked_i64, i64);
+    generate_zip_iterator_get_unchecked_harness!(harness_zip_iterator_get_unchecked_i128, i128);
+    generate_zip_iterator_get_unchecked_harness!(harness_zip_iterator_get_unchecked_u8, u8);
+    generate_zip_iterator_get_unchecked_harness!(harness_zip_iterator_get_unchecked_u16, u16);
+    generate_zip_iterator_get_unchecked_harness!(harness_zip_iterator_get_unchecked_u32, u32);
+    generate_zip_iterator_get_unchecked_harness!(harness_zip_iterator_get_unchecked_u64, u64);
+    generate_zip_iterator_get_unchecked_harness!(harness_zip_iterator_get_unchecked_u128, u128);
+    generate_zip_iterator_get_unchecked_harness!(harness_zip_iterator_get_unchecked_array, [u8; 4]);
+    generate_zip_iterator_get_unchecked_harness!(harness_zip_iterator_get_unchecked_bool, bool);
+    generate_zip_iterator_get_unchecked_harness!(harness_zip_iterator_get_unchecked_unit, ());
+
+    // Harnesses for `get_unchecked` for ZipImpl.
+    // Use a regular proof because `proof_for_contract` cannot resolve this trait method path.
+    // Use stateless maps to combine unbounded positions with symbolic Copy payloads.
+    macro_rules! generate_zip_get_unchecked_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                // Generate independent symbolic lengths and payloads for both sides.
+                let left_len: usize = kani::any();
+                let right_len: usize = kani::any();
+                let left_value: $ty = kani::any();
+                let right_value: $ty = kani::any();
+                let left_expected = left_value;
+                let right_expected = right_value;
+                // Generate a symbolic reachable offset and remaining-relative index.
+                let index: usize = kani::any();
+                let idx: usize = kani::any();
+
+                // Preserve each absolute position while attaching a symbolic payload.
+                // These closures copy captured values without mutating any state.
+                let left = (0..left_len).map(move |position| (position, left_value));
+                let right = (0..right_len).map(move |position| (position, right_value));
+                let mut zip = Zip::new(left, right);
+
+                // Full trusted-random-access `Zip::next` changes only `index`.
+                kani::assume(index <= zip.len);
+                zip.index = index;
+
+                // Express the target's `idx < self.size()` precondition.
+                kani::assume(idx < TrustedRandomAccessNoCoerce::size(&zip));
+                let absolute_idx = index + idx;
+                let expected = ((absolute_idx, left_expected), (absolute_idx, right_expected));
+                // Save all observable state before the internal random-access call.
+                let index_before = zip.index;
+                let len_before = zip.len;
+                let left_size_before = zip.a.size_hint();
+                let right_size_before = zip.b.size_hint();
+                let size_before = Iterator::size_hint(&zip);
+
+                // Call the internal target directly rather than the outer `Iterator` method.
+                let result = unsafe { ZipImpl::get_unchecked(&mut zip, idx) };
+
+                // Check the shared translated index, both payloads, and state preservation.
+                assert_eq!(result, expected);
+                assert_eq!(zip.index, index_before);
+                assert_eq!(zip.len, len_before);
+                assert_eq!(zip.a.size_hint(), left_size_before);
+                assert_eq!(zip.b.size_hint(), right_size_before);
+                assert_eq!(Iterator::size_hint(&zip), size_before);
+            }
+        };
+    }
+
+    generate_zip_get_unchecked_harness!(harness_zip_get_unchecked_i8, i8);
+    generate_zip_get_unchecked_harness!(harness_zip_get_unchecked_i16, i16);
+    generate_zip_get_unchecked_harness!(harness_zip_get_unchecked_i32, i32);
+    generate_zip_get_unchecked_harness!(harness_zip_get_unchecked_i64, i64);
+    generate_zip_get_unchecked_harness!(harness_zip_get_unchecked_i128, i128);
+    generate_zip_get_unchecked_harness!(harness_zip_get_unchecked_u8, u8);
+    generate_zip_get_unchecked_harness!(harness_zip_get_unchecked_u16, u16);
+    generate_zip_get_unchecked_harness!(harness_zip_get_unchecked_u32, u32);
+    generate_zip_get_unchecked_harness!(harness_zip_get_unchecked_u64, u64);
+    generate_zip_get_unchecked_harness!(harness_zip_get_unchecked_u128, u128);
+    generate_zip_get_unchecked_harness!(harness_zip_get_unchecked_array, [u8; 4]);
+    generate_zip_get_unchecked_harness!(harness_zip_get_unchecked_bool, bool);
+    generate_zip_get_unchecked_harness!(harness_zip_get_unchecked_unit, ());
+
+    // Harnesses for `fold` for ZipImpl.
+    macro_rules! generate_zip_fold_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            fn $name() {
+                // Generate independent symbolic lengths for both sides.
+                let left_len: usize = kani::any();
+                let right_len: usize = kani::any();
+
+                // Generate independent symbolic payloads for both sides.
+                let left_value: $ty = kani::any();
+                let right_value: $ty = kani::any();
+
+                // Map preserves full trusted random access with unbounded lengths.
+                let left = (0..left_len).map(move |_| left_value);
+                let right = (0..right_len).map(move |_| right_value);
+                let mut zip = Zip::new(left, right);
+
+                // Model any reachable offset in the full trusted-random-access Zip.
+                let index: usize = kani::any();
+                kani::assume(index <= zip.len);
+                zip.index = index;
+
+                // Call the specialized safe function directly.
+                ZipImpl::fold(zip, (), |(), _pair| ());
+            }
+        };
+    }
+
+    generate_zip_fold_harness!(harness_zip_fold_i8, i8);
+    generate_zip_fold_harness!(harness_zip_fold_i16, i16);
+    generate_zip_fold_harness!(harness_zip_fold_i32, i32);
+    generate_zip_fold_harness!(harness_zip_fold_i64, i64);
+    generate_zip_fold_harness!(harness_zip_fold_i128, i128);
+    generate_zip_fold_harness!(harness_zip_fold_u8, u8);
+    generate_zip_fold_harness!(harness_zip_fold_u16, u16);
+    generate_zip_fold_harness!(harness_zip_fold_u32, u32);
+    generate_zip_fold_harness!(harness_zip_fold_u64, u64);
+    generate_zip_fold_harness!(harness_zip_fold_u128, u128);
+    generate_zip_fold_harness!(harness_zip_fold_bool, bool);
+    generate_zip_fold_harness!(harness_zip_fold_unit, ());
+    generate_zip_fold_harness!(harness_zip_fold_array, [u8; 4]);
+
+    // Harnesses for `next` for ZipImpl.
+    macro_rules! generate_zip_next_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            fn $name() {
+                // Generate independent symbolic lengths for both sides.
+                let left_len: usize = kani::any();
+                let right_len: usize = kani::any();
+
+                // Generate independent symbolic payloads for both sides.
+                let left_value: $ty = kani::any();
+                let right_value: $ty = kani::any();
+
+                // Map over Range preserves TrustedRandomAccess.
+                let left = (0..left_len).map(move |_| left_value);
+                let right = (0..right_len).map(move |_| right_value);
+                let mut zip = Zip::new(left, right);
+
+                // Model any reachable offset in the full trusted-random-access Zip.
+                let index: usize = kani::any();
+                kani::assume(index <= zip.len);
+                zip.index = index;
+
+                // Call the specialized safe function directly.
+                ZipImpl::next(&mut zip);
+            }
+        };
+    }
+
+    generate_zip_next_harness!(harness_zip_next_i8, i8);
+    generate_zip_next_harness!(harness_zip_next_i16, i16);
+    generate_zip_next_harness!(harness_zip_next_i32, i32);
+    generate_zip_next_harness!(harness_zip_next_i64, i64);
+    generate_zip_next_harness!(harness_zip_next_i128, i128);
+    generate_zip_next_harness!(harness_zip_next_u8, u8);
+    generate_zip_next_harness!(harness_zip_next_u16, u16);
+    generate_zip_next_harness!(harness_zip_next_u32, u32);
+    generate_zip_next_harness!(harness_zip_next_u64, u64);
+    generate_zip_next_harness!(harness_zip_next_u128, u128);
+    generate_zip_next_harness!(harness_zip_next_bool, bool);
+    generate_zip_next_harness!(harness_zip_next_unit, ());
+    generate_zip_next_harness!(harness_zip_next_array, [u8; 4]);
+
+    // Harnesses for `next` for ZipImpl.
+    macro_rules! generate_zip_nth_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            fn $name() {
+                // Generate independent symbolic lengths and the requested index.
+                let left_len: usize = kani::any();
+                let right_len: usize = kani::any();
+                let n: usize = kani::any();
+
+                // Generate independent symbolic payloads for both sides.
+                let left_value: $ty = kani::any();
+                let right_value: $ty = kani::any();
+
+                // Map selects the full trusted-random-access specialization.
+                let left = (0..left_len).map(move |_| left_value);
+                let right = (0..right_len).map(move |_| right_value);
+                let mut zip = Zip::new(left, right);
+
+                // Model any state reachable by prior forward iteration.
+                let index: usize = kani::any();
+                kani::assume(index <= zip.len);
+                zip.index = index;
+
+                // Call the specialized safe function directly.
+                ZipImpl::nth(&mut zip, n);
+            }
+        };
+    }
+
+    generate_zip_nth_harness!(harness_zip_nth_i8, i8);
+    generate_zip_nth_harness!(harness_zip_nth_i16, i16);
+    generate_zip_nth_harness!(harness_zip_nth_i32, i32);
+    generate_zip_nth_harness!(harness_zip_nth_i64, i64);
+    generate_zip_nth_harness!(harness_zip_nth_i128, i128);
+    generate_zip_nth_harness!(harness_zip_nth_u8, u8);
+    generate_zip_nth_harness!(harness_zip_nth_u16, u16);
+    generate_zip_nth_harness!(harness_zip_nth_u32, u32);
+    generate_zip_nth_harness!(harness_zip_nth_u64, u64);
+    generate_zip_nth_harness!(harness_zip_nth_u128, u128);
+    generate_zip_nth_harness!(harness_zip_nth_bool, bool);
+    generate_zip_nth_harness!(harness_zip_nth_unit, ());
+    generate_zip_nth_harness!(harness_zip_nth_array, [u8; 4]);
+
+    // Harnesses for `next_back` for ZipImpl.
+    #[kani::proof]
+    fn harness_zip_next_back() {
+        // Generate independent unbounded lengths.
+        let left_len: usize = kani::any();
+        let right_len: usize = kani::any();
+
+        // Core Range iterators provide trusted random access.
+        let left = 0..left_len;
+        let right = 0..right_len;
+        let mut zip = Zip::new(left, right);
+
+        // Model any state reachable after prior forward iteration.
+        let index: usize = kani::any();
+        kani::assume(index <= zip.len);
+        zip.index = index;
+
+        // Call the specialized safe function directly.
+        ZipImpl::next_back(&mut zip);
+    }
+
+    // Harnesses for `spec_fold` for ZipImpl.
+    macro_rules! generate_zip_spec_fold_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            fn $name() {
+                // Generate independent symbolic finite lengths.
+                let left_len: usize = kani::any();
+                let right_len: usize = kani::any();
+
+                // Generate independent symbolic values for both sides.
+                let left_value: $ty = kani::any();
+                let right_value: $ty = kani::any();
+
+                // Take<Repeat<T>> preserves full trusted random access.
+                let left = crate::iter::repeat(left_value).take(left_len);
+                let right = crate::iter::repeat(right_value).take(right_len);
+                let zip = Zip::new(left, right);
+
+                // Call the TrustedLen-specialized safe function directly.
+                SpecFold::spec_fold(zip, (), |(), _pair| ());
+            }
+        };
+    }
+
+    generate_zip_spec_fold_harness!(harness_zip_spec_fold_i8, i8);
+    generate_zip_spec_fold_harness!(harness_zip_spec_fold_i16, i16);
+    generate_zip_spec_fold_harness!(harness_zip_spec_fold_i32, i32);
+    generate_zip_spec_fold_harness!(harness_zip_spec_fold_i64, i64);
+    generate_zip_spec_fold_harness!(harness_zip_spec_fold_i128, i128);
+    generate_zip_spec_fold_harness!(harness_zip_spec_fold_u8, u8);
+    generate_zip_spec_fold_harness!(harness_zip_spec_fold_u16, u16);
+    generate_zip_spec_fold_harness!(harness_zip_spec_fold_u32, u32);
+    generate_zip_spec_fold_harness!(harness_zip_spec_fold_u64, u64);
+    generate_zip_spec_fold_harness!(harness_zip_spec_fold_u128, u128);
+    generate_zip_spec_fold_harness!(harness_zip_spec_fold_bool, bool);
+    generate_zip_spec_fold_harness!(harness_zip_spec_fold_unit, ());
+    generate_zip_spec_fold_harness!(harness_zip_spec_fold_array, [u8; 4]);
+}