diff --git a/library/core/src/iter/adapters/array_chunks.rs b/library/core/src/iter/adapters/array_chunks.rs
index 6c502ee75e17f..600e64e1d2a47 100644
--- a/library/core/src/iter/adapters/array_chunks.rs
+++ b/library/core/src/iter/adapters/array_chunks.rs
@@ -1,6 +1,8 @@
 use crate::array;
 use crate::iter::adapters::SourceIter;
 use crate::iter::{FusedIterator, InPlaceIterable, TrustedFused, TrustedRandomAccessNoCoerce};
+#[cfg(kani)]
+use crate::kani;
 use crate::num::NonZero;
 use crate::ops::{ControlFlow, NeverShortCircuit, Try};
 
@@ -224,6 +226,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
@@ -268,3 +279,80 @@ 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]
+            #[kani::unwind(5)]
+            // The input length remains unbounded. Kani cannot automatically infer that
+            // `array::write` iterates at most `end % 4 <= 3` times, so `unwind(5)`
+            // bounds loop expansion, not input length; unwinding assertions ensure completeness.
+            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 86d92b56c3984..1f1c05c7f243a 100644
--- a/library/core/src/iter/adapters/cloned.rs
+++ b/library/core/src/iter/adapters/cloned.rs
@@ -180,3 +180,49 @@ 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.
+    macro_rules! generate_cloned_get_unchecked_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof_for_contract(
+                            <Cloned<crate::slice::Iter<'static, $ty>> as crate::iter::Iterator>::
+                                __iterator_get_unchecked
+                        )]
+            pub fn $name() {
+                let len: usize = kani::any();
+                let idx: usize = kani::any();
+                let value: $ty = kani::any();
+                let source = (0..len).map(|_| &value);
+                let mut iter = Cloned::new(source);
+                let _ = unsafe { crate::iter::Iterator::__iterator_get_unchecked(&mut iter, idx) };
+                // Place witnesses after the call so they exercise the contract.
+                kani::cover(idx == 0, "first element");
+                kani::cover(idx > 0 && idx < len - 1, "interior element");
+                kani::cover(idx == len - 1, "last element");
+                kani::cover(
+                    len == usize::MAX && idx == len - 1,
+                    "last element at the maximum logical length",
+                );
+            }
+        };
+    }
+
+    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, ());
+}
diff --git a/library/core/src/iter/adapters/copied.rs b/library/core/src/iter/adapters/copied.rs
index a8592c8e3c671..dd15e1e15aaae 100644
--- a/library/core/src/iter/adapters/copied.rs
+++ b/library/core/src/iter/adapters/copied.rs
@@ -284,3 +284,91 @@ 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.
+    macro_rules! generate_copied_get_unchecked_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof_for_contract(
+                            <Copied<crate::slice::Iter<'static, $ty>> as crate::iter::Iterator>::
+                                __iterator_get_unchecked
+                        )]
+            pub fn $name() {
+                let len: usize = kani::any();
+                let idx: usize = kani::any();
+                let value: $ty = kani::any();
+                let source = (0..len).map(|_| &value);
+                let mut iter = Copied::new(source);
+                let _ = unsafe { crate::iter::Iterator::__iterator_get_unchecked(&mut iter, idx) };
+                kani::cover(idx == 0, "first element");
+                kani::cover(idx > 0 && idx < len - 1, "interior element");
+                kani::cover(idx == len - 1, "last element");
+                kani::cover(
+                    len == usize::MAX && idx == len - 1,
+                    "last element at the maximum logical length",
+                );
+            }
+        };
+    }
+
+    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 8d83a8caaf53f..b59687b2986b5 100644
--- a/library/core/src/iter/adapters/enumerate.rs
+++ b/library/core/src/iter/adapters/enumerate.rs
@@ -321,3 +321,55 @@ 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.
+    macro_rules! generate_enumerate_get_unchecked_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof_for_contract(
+                            <Enumerate<
+                                crate::iter::Map<crate::ops::Range<usize>, fn(usize) -> $ty>,
+                            > as crate::iter::Iterator>::__iterator_get_unchecked
+                        )]
+            pub fn $name() {
+                let count: usize = kani::any();
+                let end: usize = kani::any();
+                let idx: usize = kani::any();
+                let value: $ty = kani::any();
+                let source = (count..end).map(move |_| value);
+                let mut iter = Enumerate { iter: source, count };
+                let _ = unsafe { crate::iter::Iterator::__iterator_get_unchecked(&mut iter, idx) };
+                let len = end - count;
+                kani::cover(count == 0 && idx == 0, "first element");
+                kani::cover(
+                    count > 0 && idx > 0 && idx < len - 1,
+                    "interior element after a prefix",
+                );
+                kani::cover(idx == len - 1, "last element");
+                kani::cover(count == usize::MAX - 1 && idx == 0, "large enumeration offset");
+                kani::cover(
+                    len == usize::MAX && idx == len - 1,
+                    "last element at the maximum logical length",
+                );
+            }
+        };
+    }
+
+    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 cf21536784a28..59e568657139b 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, TrustedLen};
+#[cfg(kani)]
+use crate::kani;
 use crate::num::NonZero;
 use crate::ops::Try;
 
@@ -251,3 +253,41 @@ impl<I: TrustedLen> SpecAssumeCount for I {
         unsafe { crate::hint::assert_unchecked(count <= upper) }
     }
 }
+
+#[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 3fd7e16d1c148..68e3a0aae06bf 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 837cd43c12226..6f82c8f170983 100644
--- a/library/core/src/iter/adapters/fuse.rs
+++ b/library/core/src/iter/adapters/fuse.rs
@@ -511,3 +511,49 @@ 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.
+    macro_rules! generate_fuse_get_unchecked_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof_for_contract(
+                            <Fuse<
+                                crate::iter::Map<crate::ops::Range<usize>, fn(usize) -> $ty>,
+                            > as crate::iter::Iterator>::__iterator_get_unchecked
+                        )]
+            pub fn $name() {
+                let len: usize = kani::any();
+                let idx: usize = kani::any();
+                let value: $ty = kani::any();
+                let source = (0..len).map(move |_| value);
+                let mut iter = Fuse { iter: if kani::any() { Some(source) } else { None } };
+                let _ = unsafe { crate::iter::Iterator::__iterator_get_unchecked(&mut iter, idx) };
+                kani::cover(idx == 0, "first element");
+                kani::cover(idx > 0 && idx < len - 1, "interior element");
+                kani::cover(idx == len - 1, "last element");
+                kani::cover(
+                    len == usize::MAX && idx == len - 1,
+                    "last element at the maximum logical length",
+                );
+            }
+        };
+    }
+
+    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 0bc4dac44b9a6..fad965b0622c1 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,
@@ -231,3 +232,55 @@ 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.
+    macro_rules! generate_map_get_unchecked_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof_for_contract(
+                                        <Map<
+                                            crate::ops::Range<usize>,
+                                            fn(usize) -> ($ty, usize, usize),
+                                        > as crate::iter::Iterator>::__iterator_get_unchecked
+                                    )]
+            pub fn $name() {
+                let len: usize = kani::any();
+                let idx: usize = kani::any();
+                let value: $ty = kani::any();
+                let initial_calls: usize = kani::any();
+                let mut calls = initial_calls;
+                let mut iter = Map::new(0..len, move |position| {
+                    calls = calls.wrapping_add(1);
+                    (value, position, calls)
+                });
+                let _ = unsafe { crate::iter::Iterator::__iterator_get_unchecked(&mut iter, idx) };
+                kani::cover(idx == 0, "first element");
+                kani::cover(idx > 0 && idx < len - 1, "interior element");
+                kani::cover(idx == len - 1, "last element");
+                kani::cover(initial_calls == usize::MAX, "wrapping closure state");
+                kani::cover(
+                    len == usize::MAX && idx == len - 1,
+                    "last element at the maximum logical length",
+                );
+            }
+        };
+    }
+
+    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, ());
+}
diff --git a/library/core/src/iter/adapters/map_windows.rs b/library/core/src/iter/adapters/map_windows.rs
index cbde6c92b752e..b3a30b540110d 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::{ManuallyDrop, MaybeUninit, SizedTypeProperties};
 use crate::ub_checks::Invariant;
 use crate::{fmt, ptr};
@@ -295,3 +297,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 9173489531107..5eb3f1f2542ee 100644
--- a/library/core/src/iter/adapters/skip.rs
+++ b/library/core/src/iter/adapters/skip.rs
@@ -162,7 +162,8 @@ where
     }
 
     #[doc(hidden)]
-    #[requires(idx + self.n < self.iter.size_hint().0)]
+    // Express the translated index bound without overflowing in the contract.
+    #[requires(idx < self.iter.size_hint().0.saturating_sub(self.n))]
     #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn __iterator_get_unchecked(&mut self, idx: usize) -> Self::Item
     where
@@ -180,6 +181,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 +306,95 @@ 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.
+    #[kani::proof_for_contract(
+        <Skip<crate::ops::Range<usize>> as crate::iter::Iterator>::__iterator_get_unchecked
+    )]
+    pub fn harness_skip_get_unchecked_unbounded() {
+        let len: usize = kani::any();
+        let n: usize = kani::any();
+        let idx: usize = kani::any();
+        let mut iter = Skip::new(0..len, n);
+        let _ = unsafe { crate::iter::Iterator::__iterator_get_unchecked(&mut iter, idx) };
+        let remaining = len - n;
+        kani::cover(n == 0 && idx == 0, "first element without a skipped prefix");
+        kani::cover(n > 0 && idx == 0, "first element after a skipped prefix");
+        kani::cover(idx > 0 && idx < remaining - 1, "interior element");
+        kani::cover(idx == remaining - 1, "last element");
+        kani::cover(
+            len == usize::MAX && n == 0 && idx == len - 1,
+            "last element at the maximum logical length",
+        );
+    }
+
+    macro_rules! generate_skip_get_unchecked_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof_for_contract(
+                            <Skip<
+                                crate::iter::Map<crate::ops::Range<usize>, fn(usize) -> $ty>,
+                            > as crate::iter::Iterator>::__iterator_get_unchecked
+                        )]
+            pub fn $name() {
+                let len: usize = kani::any();
+                let n: usize = kani::any();
+                let idx: usize = kani::any();
+                let value: $ty = kani::any();
+                let source = (0..len).map(move |_| value);
+                let mut iter = Skip::new(source, n);
+                let _ = unsafe { crate::iter::Iterator::__iterator_get_unchecked(&mut iter, idx) };
+                let remaining = len - n;
+                kani::cover(n == 0 && idx == 0, "empty skipped prefix");
+                kani::cover(n > 0 && idx == 0, "nonempty skipped prefix");
+                kani::cover(n > 0 && idx > 0, "access without evaluating the prefix");
+                kani::cover(idx == remaining - 1, "last element");
+                kani::cover(
+                    len == usize::MAX && n == usize::MAX - 1 && idx == 0,
+                    "maximum skipped prefix",
+                );
+            }
+        };
+    }
+
+    // Use a regular proof because proof_for_contract cannot name the
+    // anonymous closure type used by Map. Mirror the target's precondition.
+    #[kani::proof]
+    pub fn harness_skip_get_unchecked_side_effect() {
+        let len: usize = kani::any();
+        let n: usize = kani::any();
+        let idx: usize = kani::any();
+        let mut calls: usize = kani::any();
+        let source = (0..usize::MAX).map(|position| position);
+        let mut iter = Skip::new(source, n);
+        // Mirror the target's #[requires] contract.
+        kani::assume(idx < iter.size_hint().0);
+        kani::cover(true, "the mirrored precondition is satisfiable");
+        let _ = unsafe { crate::iter::Iterator::__iterator_get_unchecked(&mut iter, idx) };
+        kani::cover(n == 0 && idx == 0, "empty skipped prefix");
+        kani::cover(n > 0 && idx == 0, "stateful nonempty skipped prefix");
+        kani::cover(n > 0 && idx > 0, "stateful access without evaluating the prefix");
+        kani::cover(
+            len == usize::MAX && n == usize::MAX - 1 && idx == 0,
+            "stateful maximum skipped prefix",
+        );
+    }
+
+    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, ());
+}
diff --git a/library/core/src/iter/adapters/step_by.rs b/library/core/src/iter/adapters/step_by.rs
index f1e54b9cdd322..dcc792560ae65 100644
--- a/library/core/src/iter/adapters/step_by.rs
+++ b/library/core/src/iter/adapters/step_by.rs
@@ -651,3 +651,22 @@ mod step_by_spec {
     spec_int_ranges_r!(Range; u8 u16 usize);
     spec_int_ranges_r!(RangeIter; 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 3df2c70801644..1230ec912940a 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};
 
@@ -312,6 +314,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(kani::index <= end))]
         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) };
@@ -323,6 +326,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(kani::index <= end))]
         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) };
@@ -387,3 +391,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 a5dc7e59096f6..94e877ae30521 100644
--- a/library/core/src/iter/adapters/zip.rs
+++ b/library/core/src/iter/adapters/zip.rs
@@ -26,6 +26,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);
@@ -265,6 +282,7 @@ where
     }
 
     #[inline]
+    #[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;
@@ -280,6 +298,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.
@@ -328,6 +358,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
@@ -679,3 +722,368 @@ impl<A: TrustedLen, B: TrustedLen> SpecFold for Zip<A, B> {
         accum
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+
+    // Harnesses for `__iterator_get_unchecked` for Zip.
+    macro_rules! generate_zip_iterator_get_unchecked_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof_for_contract(
+                            <Zip<
+                                crate::iter::Map<crate::ops::Range<usize>, fn(usize) -> $ty>,
+                                crate::iter::Map<crate::ops::Range<usize>, fn(usize) -> $ty>,
+                            > as crate::iter::Iterator>::__iterator_get_unchecked
+                        )]
+            pub fn $name() {
+                let left_len: usize = kani::any();
+                let right_len: usize = kani::any();
+                let index: usize = kani::any();
+                let idx: usize = kani::any();
+                let left_value: $ty = kani::any();
+                let right_value: $ty = kani::any();
+                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);
+                zip.index = index.min(zip.len);
+                let _ = unsafe { Iterator::__iterator_get_unchecked(&mut zip, idx) };
+                let remaining = zip.len - zip.index;
+                kani::cover(zip.index == 0 && idx == 0, "first element");
+                kani::cover(zip.index > 0 && idx == 0, "first element after a prefix");
+                kani::cover(idx > 0 && idx < remaining - 1, "interior element");
+                kani::cover(idx == remaining - 1, "last element");
+                kani::cover(left_len < right_len, "left iterator is shorter");
+                kani::cover(left_len > right_len, "right iterator is shorter");
+                kani::cover(
+                    left_len == usize::MAX && right_len == usize::MAX && idx == usize::MAX - 1,
+                    "last element at the maximum logical length",
+                );
+            }
+        };
+    }
+
+    #[kani::proof_for_contract(
+        <Zip<
+            crate::ops::Range<usize>,
+            crate::ops::Range<usize>,
+        > as crate::iter::Iterator>::__iterator_get_unchecked
+    )]
+    fn harness_zip_iterator_get_unchecked_unbounded() {
+        let left_len: usize = kani::any();
+        let right_len: usize = kani::any();
+        let index: usize = kani::any();
+        let idx: usize = kani::any();
+        let mut zip = Zip::new(0..left_len, 0..right_len);
+        zip.len = kani::any::<usize>().min(zip.len);
+        zip.index = index.min(zip.len);
+        let _ = unsafe { Iterator::__iterator_get_unchecked(&mut zip, idx) };
+        let remaining = zip.len - zip.index;
+        kani::cover(zip.index == 0 && idx == 0, "first element");
+        kani::cover(zip.index > 0 && idx == 0, "first element after a prefix");
+        kani::cover(idx > 0 && idx < remaining - 1, "interior element");
+        kani::cover(idx == remaining - 1, "last element");
+        kani::cover(zip.len < left_len.min(right_len), "access after consuming from the back");
+        kani::cover(
+            left_len == usize::MAX && right_len == usize::MAX && idx == usize::MAX - 1,
+            "last element at the maximum logical length",
+        );
+    }
+
+    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.
+    macro_rules! generate_zip_get_unchecked_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof_for_contract(
+                <Zip<
+                    crate::iter::Map<crate::ops::Range<usize>, fn(usize) -> (usize, $ty)>,
+                    crate::iter::Map<crate::ops::Range<usize>, fn(usize) -> (usize, $ty)>,
+                > as ZipImpl<
+                    crate::iter::Map<crate::ops::Range<usize>, fn(usize) -> (usize, $ty)>,
+                    crate::iter::Map<crate::ops::Range<usize>, fn(usize) -> (usize, $ty)>,
+                >>::get_unchecked
+            )]
+            pub fn $name() {
+                let left_len: usize = kani::any();
+                let right_len: usize = kani::any();
+                let index: usize = kani::any();
+                let idx: usize = kani::any();
+                let left_value: $ty = kani::any();
+                let right_value: $ty = kani::any();
+                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);
+                zip.index = index.min(zip.len);
+                let _ = unsafe { ZipImpl::get_unchecked(&mut zip, idx) };
+                let remaining = zip.len - zip.index;
+                kani::cover(zip.index == 0 && idx == 0, "first element");
+                kani::cover(zip.index > 0 && idx == 0, "first element after a prefix");
+                kani::cover(idx > 0 && idx < remaining - 1, "interior element");
+                kani::cover(idx == remaining - 1, "last element");
+                kani::cover(left_len < right_len, "left iterator is shorter");
+                kani::cover(left_len > right_len, "right iterator is shorter");
+                kani::cover(zip.index == usize::MAX - 1 && idx == 0, "maximum valid offset");
+                kani::cover(
+                    left_len == usize::MAX && right_len == usize::MAX && idx == usize::MAX - 1,
+                    "last element at the maximum logical length",
+                );
+            }
+        };
+    }
+
+    #[kani::proof_for_contract(
+        <Zip<
+            crate::ops::Range<usize>,
+            crate::ops::Range<usize>,
+        > as ZipImpl<
+            crate::ops::Range<usize>,
+            crate::ops::Range<usize>,
+        >>::get_unchecked
+    )]
+    fn harness_zip_get_unchecked_unbounded() {
+        let left_len: usize = kani::any();
+        let right_len: usize = kani::any();
+        let index: usize = kani::any();
+        let idx: usize = kani::any();
+        let mut zip = Zip::new(0..left_len, 0..right_len);
+        // For ranges, front/back consumption changes only index/len.
+        zip.len = kani::any::<usize>().min(zip.len);
+        zip.index = index.min(zip.len);
+        let _ = unsafe { ZipImpl::get_unchecked(&mut zip, idx) };
+        let remaining = zip.len - zip.index;
+        kani::cover(zip.index == 0 && idx == 0, "first element");
+        kani::cover(zip.index > 0 && idx == 0, "first element after a prefix");
+        kani::cover(idx > 0 && idx < remaining - 1, "interior element");
+        kani::cover(idx == remaining - 1, "last element");
+        kani::cover(zip.len < left_len.min(right_len), "access after consuming from the back");
+        kani::cover(zip.index == usize::MAX - 1 && idx == 0, "maximum valid offset");
+        kani::cover(
+            left_len == usize::MAX && right_len == usize::MAX && idx == usize::MAX - 1,
+            "last element at the maximum logical length",
+        );
+    }
+
+    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]
+            #[kani::unwind(8)]
+            pub fn $name() {
+                // Generate independent symbolic lengths, bounded for unwinding.
+                let left_len: usize = kani::any();
+                let right_len: usize = kani::any();
+                kani::assume(left_len <= 4 && right_len <= 4);
+                kani::cover(true, "bounded input is satisfiable");
+                // Generate independent symbolic payloads.
+                let left_value: $ty = kani::any();
+                let right_value: $ty = kani::any();
+                // Take<Repeat<T>> provides a finite TrustedLen iterator.
+                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);
+                // Exercise the real TrustedLen-specialized implementation.
+                let count = SpecFold::spec_fold(zip, 0usize, |count, _pair| count + 1);
+                // The fold must process exactly min(left_len, right_len) pairs.
+                assert_eq!(count, left_len.min(right_len));
+                kani::cover(left_len == 0 || right_len == 0, "empty zip");
+                kani::cover(left_len < right_len, "left iterator is shorter");
+                kani::cover(left_len > right_len, "right iterator is shorter");
+                kani::cover(left_len == right_len && left_len > 0, "equal nonempty lengths");
+                kani::cover(left_len == 4 && right_len == 4, "maximum bounded length");
+            }
+        };
+    }
+
+    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]);
+}