diff --git a/library/core/src/iter/adapters/array_chunks.rs b/library/core/src/iter/adapters/array_chunks.rs
index 8f1744fc5fbb7..b053dfb5ebc2a 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};
 
@@ -274,3 +276,77 @@ unsafe impl<I: InPlaceIterable + Iterator, const N: usize> InPlaceIterable for A
         }
     };
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+
+    // next_back_remainder (uses unwrap_err_unchecked internally)
+    // Uses Range<u8> instead of slice::Iter to avoid pointer-heavy symbolic
+    // state that causes CBMC to exhaust resources. Range<u8> satisfies
+    // DoubleEndedIterator + ExactSizeIterator and exercises the same
+    // unwrap_err_unchecked path.
+    #[kani::proof]
+    #[kani::unwind(5)]
+    fn check_array_chunks_next_back_remainder_n2() {
+        let len: u8 = kani::any();
+        kani::assume(len <= 4);
+        let mut chunks = ArrayChunks::<_, 2>::new(0..len);
+        let _ = chunks.next_back();
+    }
+
+    #[kani::proof]
+    #[kani::unwind(5)]
+    fn check_array_chunks_next_back_remainder_n3() {
+        let len: u8 = kani::any();
+        kani::assume(len <= 4);
+        let mut chunks = ArrayChunks::<_, 3>::new(0..len);
+        let _ = chunks.next_back();
+    }
+
+    // fold (TRANC specialized — uses __iterator_get_unchecked in a loop)
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_array_chunks_fold_n2_u8() {
+        const MAX_LEN: usize = 8;
+        let array: [u8; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let chunks = ArrayChunks::<_, 2>::new(slice.iter());
+        let count = Iterator::fold(chunks, 0usize, |acc, _| acc + 1);
+        assert_eq!(count, slice.len() / 2);
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_array_chunks_fold_n2_unit() {
+        const MAX_LEN: usize = 8;
+        let array: [(); MAX_LEN] = [(); MAX_LEN];
+        let slice = kani::slice::any_slice_of_array(&array);
+        let chunks = ArrayChunks::<_, 2>::new(slice.iter());
+        let count = Iterator::fold(chunks, 0usize, |acc, _| acc + 1);
+        assert_eq!(count, slice.len() / 2);
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_array_chunks_fold_n3_u8() {
+        const MAX_LEN: usize = 6;
+        let array: [u8; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let chunks = ArrayChunks::<_, 3>::new(slice.iter());
+        let count = Iterator::fold(chunks, 0usize, |acc, _| acc + 1);
+        assert_eq!(count, slice.len() / 3);
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_array_chunks_fold_n2_char() {
+        const MAX_LEN: usize = 8;
+        let array: [char; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let chunks = ArrayChunks::<_, 2>::new(slice.iter());
+        let count = Iterator::fold(chunks, 0usize, |acc, _| acc + 1);
+        assert_eq!(count, slice.len() / 2);
+    }
+}
diff --git a/library/core/src/iter/adapters/cloned.rs b/library/core/src/iter/adapters/cloned.rs
index 0f05260059880..a171cf48dacf5 100644
--- a/library/core/src/iter/adapters/cloned.rs
+++ b/library/core/src/iter/adapters/cloned.rs
@@ -152,6 +152,7 @@ where
     I: UncheckedIterator<Item = &'a T>,
     T: Clone,
 {
+    #[requires(self.it.size_hint().0 > 0)]
     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 +194,102 @@ 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::*;
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_cloned_get_unchecked_u8() {
+        const MAX_LEN: usize = 8;
+        let array: [u8; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Cloned::new(slice.iter());
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let result = unsafe { iter.__iterator_get_unchecked(idx) };
+        assert_eq!(result, slice[idx]);
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_cloned_get_unchecked_unit() {
+        const MAX_LEN: usize = 8;
+        let array: [(); MAX_LEN] = [(); MAX_LEN];
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Cloned::new(slice.iter());
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_cloned_next_unchecked_u8() {
+        const MAX_LEN: usize = 8;
+        let array: [u8; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Cloned::new(slice.iter());
+        kani::assume(iter.size_hint().0 > 0);
+        let _ = unsafe { iter.next_unchecked() };
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_cloned_next_unchecked_unit() {
+        const MAX_LEN: usize = 8;
+        let array: [(); MAX_LEN] = [(); MAX_LEN];
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Cloned::new(slice.iter());
+        kani::assume(iter.size_hint().0 > 0);
+        let _ = unsafe { iter.next_unchecked() };
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_cloned_get_unchecked_char() {
+        const MAX_LEN: usize = 8;
+        let array: [char; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Cloned::new(slice.iter());
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_cloned_get_unchecked_tup() {
+        const MAX_LEN: usize = 8;
+        let array: [(char, u8); MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Cloned::new(slice.iter());
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_cloned_next_unchecked_char() {
+        const MAX_LEN: usize = 8;
+        let array: [char; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Cloned::new(slice.iter());
+        kani::assume(iter.size_hint().0 > 0);
+        let _ = unsafe { iter.next_unchecked() };
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_cloned_next_unchecked_tup() {
+        const MAX_LEN: usize = 8;
+        let array: [(char, u8); MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Cloned::new(slice.iter());
+        kani::assume(iter.size_hint().0 > 0);
+        let _ = unsafe { iter.next_unchecked() };
+    }
+}
diff --git a/library/core/src/iter/adapters/copied.rs b/library/core/src/iter/adapters/copied.rs
index 0b9da45acaa06..129c7177dbee1 100644
--- a/library/core/src/iter/adapters/copied.rs
+++ b/library/core/src/iter/adapters/copied.rs
@@ -278,3 +278,101 @@ 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::*;
+
+    // Phase 0 spike: proof_for_contract doesn't work on trait impl methods,
+    // so we use #[kani::proof] with manual precondition via kani::assume.
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_copied_get_unchecked_u8() {
+        const MAX_LEN: usize = 8;
+        let array: [u8; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Copied::new(slice.iter());
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let result = unsafe { iter.__iterator_get_unchecked(idx) };
+        assert_eq!(result, slice[idx]);
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_copied_get_unchecked_unit() {
+        const MAX_LEN: usize = 8;
+        let array: [(); MAX_LEN] = [(); MAX_LEN];
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Copied::new(slice.iter());
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+    }
+
+    // spec_next_chunk (specialized for slice::Iter, uses ptr::copy_nonoverlapping)
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_spec_next_chunk_n2_u8() {
+        const MAX_LEN: usize = 8;
+        let array: [u8; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Copied::new(slice.iter());
+        let _ = iter.next_chunk::<2>();
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_spec_next_chunk_n3_u8() {
+        const MAX_LEN: usize = 8;
+        let array: [u8; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Copied::new(slice.iter());
+        let _ = iter.next_chunk::<3>();
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_spec_next_chunk_n2_unit() {
+        const MAX_LEN: usize = 8;
+        let array: [(); MAX_LEN] = [(); MAX_LEN];
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Copied::new(slice.iter());
+        let _ = iter.next_chunk::<2>();
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_copied_get_unchecked_char() {
+        const MAX_LEN: usize = 8;
+        let array: [char; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Copied::new(slice.iter());
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_copied_get_unchecked_tup() {
+        const MAX_LEN: usize = 8;
+        let array: [(char, u8); MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Copied::new(slice.iter());
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_spec_next_chunk_n2_char() {
+        const MAX_LEN: usize = 8;
+        let array: [char; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Copied::new(slice.iter());
+        let _ = iter.next_chunk::<2>();
+    }
+}
diff --git a/library/core/src/iter/adapters/enumerate.rs b/library/core/src/iter/adapters/enumerate.rs
index e7e18d178031f..1dfcc4729ec4f 100644
--- a/library/core/src/iter/adapters/enumerate.rs
+++ b/library/core/src/iter/adapters/enumerate.rs
@@ -321,3 +321,59 @@ impl<I: Default> Default for Enumerate<I> {
         Enumerate::new(Default::default())
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_enumerate_get_unchecked_u8() {
+        const MAX_LEN: usize = 8;
+        let array: [u8; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Enumerate::new(slice.iter());
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let (i, val) = unsafe { iter.__iterator_get_unchecked(idx) };
+        assert_eq!(i, idx);
+        assert_eq!(*val, slice[idx]);
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_enumerate_get_unchecked_unit() {
+        const MAX_LEN: usize = 8;
+        let array: [(); MAX_LEN] = [(); MAX_LEN];
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Enumerate::new(slice.iter());
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_enumerate_get_unchecked_char() {
+        const MAX_LEN: usize = 8;
+        let array: [char; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Enumerate::new(slice.iter());
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_enumerate_get_unchecked_tup() {
+        const MAX_LEN: usize = 8;
+        let array: [(char, u8); MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Enumerate::new(slice.iter());
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+    }
+}
diff --git a/library/core/src/iter/adapters/filter.rs b/library/core/src/iter/adapters/filter.rs
index dd08cd6f61c4c..5ac4c8aba1e6d 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,40 @@ 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::*;
+
+    // next_chunk_dropless (uses get_unchecked_mut, array_assume_init, IntoIter::new_unchecked)
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_filter_next_chunk_dropless_n2_u8() {
+        const MAX_LEN: usize = 8;
+        let array: [u8; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Filter::new(slice.iter(), |&&x: &&u8| x < 128);
+        let _ = iter.next_chunk::<2>();
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_filter_next_chunk_dropless_n3_u8() {
+        const MAX_LEN: usize = 8;
+        let array: [u8; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Filter::new(slice.iter(), |&&x: &&u8| x < 128);
+        let _ = iter.next_chunk::<3>();
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_filter_next_chunk_dropless_n2_char() {
+        const MAX_LEN: usize = 8;
+        let array: [char; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Filter::new(slice.iter(), |&&x: &&char| (x as u32) < 128);
+        let _ = iter.next_chunk::<2>();
+    }
+}
diff --git a/library/core/src/iter/adapters/filter_map.rs b/library/core/src/iter/adapters/filter_map.rs
index 24ec6b1741ce1..b610400a4ec0d 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,42 @@ 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::*;
+
+    // next_chunk (uses get_unchecked_mut, copy_nonoverlapping, array_assume_init,
+    //             IntoIter::new_unchecked)
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_filter_map_next_chunk_n2_u8() {
+        const MAX_LEN: usize = 8;
+        let array: [u8; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = FilterMap::new(slice.iter(), |&x: &u8| if x < 128 { Some(x) } else { None });
+        let _ = iter.next_chunk::<2>();
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_filter_map_next_chunk_n3_u8() {
+        const MAX_LEN: usize = 8;
+        let array: [u8; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = FilterMap::new(slice.iter(), |&x: &u8| if x < 128 { Some(x) } else { None });
+        let _ = iter.next_chunk::<3>();
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_filter_map_next_chunk_n2_char() {
+        const MAX_LEN: usize = 8;
+        let array: [char; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter =
+            FilterMap::new(slice.iter(), |&x: &char| if (x as u32) < 128 { Some(x) } else { None });
+        let _ = iter.next_chunk::<2>();
+    }
+}
diff --git a/library/core/src/iter/adapters/fuse.rs b/library/core/src/iter/adapters/fuse.rs
index fcad6168d85cd..530241cdc25f1 100644
--- a/library/core/src/iter/adapters/fuse.rs
+++ b/library/core/src/iter/adapters/fuse.rs
@@ -478,3 +478,57 @@ 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::*;
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_fuse_get_unchecked_u8() {
+        const MAX_LEN: usize = 8;
+        let array: [u8; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Fuse::new(slice.iter());
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_fuse_get_unchecked_unit() {
+        const MAX_LEN: usize = 8;
+        let array: [(); MAX_LEN] = [(); MAX_LEN];
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Fuse::new(slice.iter());
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_fuse_get_unchecked_char() {
+        const MAX_LEN: usize = 8;
+        let array: [char; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Fuse::new(slice.iter());
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_fuse_get_unchecked_tup() {
+        const MAX_LEN: usize = 8;
+        let array: [(char, u8); MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Fuse::new(slice.iter());
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+    }
+}
diff --git a/library/core/src/iter/adapters/map.rs b/library/core/src/iter/adapters/map.rs
index bf9f0c48fec3b..81d1d1781d784 100644
--- a/library/core/src/iter/adapters/map.rs
+++ b/library/core/src/iter/adapters/map.rs
@@ -245,3 +245,102 @@ 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::*;
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_map_get_unchecked_u8() {
+        const MAX_LEN: usize = 8;
+        let array: [u8; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Map::new(slice.iter(), |x: &u8| *x);
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let result = unsafe { iter.__iterator_get_unchecked(idx) };
+        assert_eq!(result, slice[idx]);
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_map_get_unchecked_unit() {
+        const MAX_LEN: usize = 8;
+        let array: [(); MAX_LEN] = [(); MAX_LEN];
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Map::new(slice.iter(), |x: &()| *x);
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_map_next_unchecked_u8() {
+        const MAX_LEN: usize = 8;
+        let array: [u8; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Map::new(slice.iter(), |x: &u8| *x);
+        kani::assume(iter.size_hint().0 > 0);
+        let _ = unsafe { iter.next_unchecked() };
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_map_next_unchecked_unit() {
+        const MAX_LEN: usize = 8;
+        let array: [(); MAX_LEN] = [(); MAX_LEN];
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Map::new(slice.iter(), |x: &()| *x);
+        kani::assume(iter.size_hint().0 > 0);
+        let _ = unsafe { iter.next_unchecked() };
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_map_get_unchecked_char() {
+        const MAX_LEN: usize = 8;
+        let array: [char; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Map::new(slice.iter(), |x: &char| *x);
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_map_get_unchecked_tup() {
+        const MAX_LEN: usize = 8;
+        let array: [(char, u8); MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Map::new(slice.iter(), |x: &(char, u8)| *x);
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_map_next_unchecked_char() {
+        const MAX_LEN: usize = 8;
+        let array: [char; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Map::new(slice.iter(), |x: &char| *x);
+        kani::assume(iter.size_hint().0 > 0);
+        let _ = unsafe { iter.next_unchecked() };
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_map_next_unchecked_tup() {
+        const MAX_LEN: usize = 8;
+        let array: [(char, u8); MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut iter = Map::new(slice.iter(), |x: &(char, u8)| *x);
+        kani::assume(iter.size_hint().0 > 0);
+        let _ = unsafe { iter.next_unchecked() };
+    }
+}
diff --git a/library/core/src/iter/adapters/map_windows.rs b/library/core/src/iter/adapters/map_windows.rs
index 536251a137da0..7525a9e3e9ca6 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,79 @@ 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 map_sum_u8(w: &[u8; 2]) -> u8 {
+        w[0].wrapping_add(w[1])
+    }
+
+    fn map_sum3_u8(w: &[u8; 3]) -> u8 {
+        w[0].wrapping_add(w[1]).wrapping_add(w[2])
+    }
+
+    // Exercises as_array_ref (via next_window), push (via repeated next),
+    // and drop (via Drop for Buffer when MapWindows is dropped).
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_map_windows_n2_u8() {
+        const MAX_LEN: usize = 8;
+        let array: [u8; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut mw = MapWindows::new(slice.iter().copied(), map_sum_u8 as fn(&[u8; 2]) -> u8);
+        while let Some(_) = mw.next() {}
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_map_windows_n3_u8() {
+        const MAX_LEN: usize = 8;
+        let array: [u8; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut mw = MapWindows::new(slice.iter().copied(), map_sum3_u8 as fn(&[u8; 3]) -> u8);
+        while let Some(_) = mw.next() {}
+    }
+
+    // Exercises as_uninit_array_mut (via Buffer::clone when MapWindows is cloned).
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_map_windows_clone_n2_u8() {
+        const MAX_LEN: usize = 8;
+        let array: [u8; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        kani::assume(slice.len() >= 2);
+        let mut mw = MapWindows::new(slice.iter().copied(), map_sum_u8 as fn(&[u8; 2]) -> u8);
+        let _ = mw.next(); // Initialize buffer
+        let _mw_clone = mw.clone(); // Exercises as_uninit_array_mut via Buffer::clone
+    }
+
+    // Exercises clone when buffer is None (before first next() call).
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_map_windows_clone_before_next_n2_u8() {
+        const MAX_LEN: usize = 8;
+        let array: [u8; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mw = MapWindows::new(slice.iter().copied(), map_sum_u8 as fn(&[u8; 2]) -> u8);
+        let mut mw_clone = mw.clone(); // Clone before buffer is initialized
+        while let Some(_) = mw_clone.next() {}
+    }
+
+    fn map_first_char(w: &[char; 2]) -> char {
+        w[0]
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_map_windows_n2_char() {
+        const MAX_LEN: usize = 8;
+        let array: [char; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let mut mw =
+            MapWindows::new(slice.iter().copied(), map_first_char as fn(&[char; 2]) -> char);
+        while let Some(_) = mw.next() {}
+    }
+}
diff --git a/library/core/src/iter/adapters/skip.rs b/library/core/src/iter/adapters/skip.rs
index ac3cc4c4f1152..b7252c58bbeb1 100644
--- a/library/core/src/iter/adapters/skip.rs
+++ b/library/core/src/iter/adapters/skip.rs
@@ -293,3 +293,65 @@ 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::*;
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_skip_get_unchecked_u8() {
+        const MAX_LEN: usize = 8;
+        let array: [u8; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let n: usize = kani::any();
+        kani::assume(n <= slice.len());
+        let mut iter = Skip::new(slice.iter(), n);
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_skip_get_unchecked_unit() {
+        const MAX_LEN: usize = 8;
+        let array: [(); MAX_LEN] = [(); MAX_LEN];
+        let slice = kani::slice::any_slice_of_array(&array);
+        let n: usize = kani::any();
+        kani::assume(n <= slice.len());
+        let mut iter = Skip::new(slice.iter(), n);
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_skip_get_unchecked_char() {
+        const MAX_LEN: usize = 8;
+        let array: [char; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let n: usize = kani::any();
+        kani::assume(n <= slice.len());
+        let mut iter = Skip::new(slice.iter(), n);
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_skip_get_unchecked_tup() {
+        const MAX_LEN: usize = 8;
+        let array: [(char, u8); MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let n: usize = kani::any();
+        kani::assume(n <= slice.len());
+        let mut iter = Skip::new(slice.iter(), n);
+        let idx: usize = kani::any();
+        kani::assume(idx < iter.size_hint().0);
+        let _ = unsafe { iter.__iterator_get_unchecked(idx) };
+    }
+}
diff --git a/library/core/src/iter/adapters/step_by.rs b/library/core/src/iter/adapters/step_by.rs
index 32604a07ca40c..975c038fd2963 100644
--- a/library/core/src/iter/adapters/step_by.rs
+++ b/library/core/src/iter/adapters/step_by.rs
@@ -589,3 +589,63 @@ 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::*;
+
+    // original_step (uses NonZero::new_unchecked + unchecked_add)
+    // Exercised through size_hint → spec_size_hint → original_step,
+    // forward iteration via next, and backward iteration via
+    // next_back → next_back_index → original_step.
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_step_by_original_step_u8() {
+        const MAX_LEN: usize = 8;
+        let array: [u8; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let step: usize = kani::any();
+        kani::assume(step >= 1 && step <= MAX_LEN);
+        let sb = StepBy::new(slice.iter(), step);
+        // size_hint calls original_step internally
+        let _ = sb.size_hint();
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_step_by_iterate_u8() {
+        const MAX_LEN: usize = 8;
+        let array: [u8; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let step: usize = kani::any();
+        kani::assume(step >= 1 && step <= MAX_LEN);
+        let mut sb = StepBy::new(slice.iter(), step);
+        while let Some(_) = sb.next() {}
+    }
+
+    // next_back exercises next_back_index → original_step
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_step_by_next_back_u8() {
+        const MAX_LEN: usize = 8;
+        let array: [u8; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let step: usize = kani::any();
+        kani::assume(step >= 1 && step <= MAX_LEN);
+        let mut sb = StepBy::new(slice.iter(), step);
+        while let Some(_) = sb.next_back() {}
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_step_by_original_step_char() {
+        const MAX_LEN: usize = 8;
+        let array: [char; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let step: usize = kani::any();
+        kani::assume(step >= 1 && step <= MAX_LEN);
+        let sb = StepBy::new(slice.iter(), step);
+        let _ = sb.size_hint();
+    }
+}
diff --git a/library/core/src/iter/adapters/take.rs b/library/core/src/iter/adapters/take.rs
index b96335f415257..3007493341a16 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};
 
@@ -374,3 +376,91 @@ 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::*;
+
+    // spec_fold (TRA specialized — uses __iterator_get_unchecked in a loop)
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_take_spec_fold_u8() {
+        const MAX_LEN: usize = 8;
+        let array: [u8; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let n: usize = kani::any();
+        kani::assume(n <= MAX_LEN);
+        let take = Take::new(slice.iter(), n);
+        let count = take.fold(0usize, |acc, _| acc + 1);
+        assert_eq!(count, n.min(slice.len()));
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_take_spec_fold_unit() {
+        const MAX_LEN: usize = 8;
+        let array: [(); MAX_LEN] = [(); MAX_LEN];
+        let slice = kani::slice::any_slice_of_array(&array);
+        let n: usize = kani::any();
+        kani::assume(n <= MAX_LEN);
+        let take = Take::new(slice.iter(), n);
+        let count = take.fold(0usize, |acc, _| acc + 1);
+        assert_eq!(count, n.min(slice.len()));
+    }
+
+    // spec_for_each (TRA specialized — uses __iterator_get_unchecked in a loop)
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_take_spec_for_each_u8() {
+        const MAX_LEN: usize = 8;
+        let array: [u8; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let n: usize = kani::any();
+        kani::assume(n <= MAX_LEN);
+        let take = Take::new(slice.iter(), n);
+        let mut count = 0usize;
+        take.for_each(|_| count += 1);
+        assert_eq!(count, n.min(slice.len()));
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_take_spec_fold_char() {
+        const MAX_LEN: usize = 8;
+        let array: [char; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let n: usize = kani::any();
+        kani::assume(n <= MAX_LEN);
+        let take = Take::new(slice.iter(), n);
+        let count = take.fold(0usize, |acc, _| acc + 1);
+        assert_eq!(count, n.min(slice.len()));
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_take_spec_fold_tup() {
+        const MAX_LEN: usize = 8;
+        let array: [(char, u8); MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let n: usize = kani::any();
+        kani::assume(n <= MAX_LEN);
+        let take = Take::new(slice.iter(), n);
+        let count = take.fold(0usize, |acc, _| acc + 1);
+        assert_eq!(count, n.min(slice.len()));
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_take_spec_for_each_char() {
+        const MAX_LEN: usize = 8;
+        let array: [char; MAX_LEN] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&array);
+        let n: usize = kani::any();
+        kani::assume(n <= MAX_LEN);
+        let take = Take::new(slice.iter(), n);
+        let mut count = 0usize;
+        take.for_each(|_| count += 1);
+        assert_eq!(count, n.min(slice.len()));
+    }
+}
diff --git a/library/core/src/iter/adapters/zip.rs b/library/core/src/iter/adapters/zip.rs
index e39f1535bd95d..fa355b18fe00b 100644
--- a/library/core/src/iter/adapters/zip.rs
+++ b/library/core/src/iter/adapters/zip.rs
@@ -270,6 +270,7 @@ where
     }
 
     #[inline]
+    #[requires(self.index + idx < self.a.size() && self.index + idx < self.b.size())]
     #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn get_unchecked(&mut self, idx: usize) -> <Self as Iterator>::Item {
         let idx = self.index + idx;
@@ -692,3 +693,178 @@ impl<A: TrustedLen, B: TrustedLen> SpecFold for Zip<A, B> {
         accum
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+    use crate::iter;
+
+    // --- Unsafe functions ---
+
+    // __iterator_get_unchecked (delegates to ZipImpl::get_unchecked)
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_zip_iterator_get_unchecked_u8() {
+        const MAX_LEN: usize = 8;
+        let arr_a: [u8; MAX_LEN] = kani::any();
+        let arr_b: [u8; MAX_LEN] = kani::any();
+        let slice_a = kani::slice::any_slice_of_array(&arr_a);
+        let slice_b = kani::slice::any_slice_of_array(&arr_b);
+        let mut zip = Zip::new(slice_a.iter(), slice_b.iter());
+        let idx: usize = kani::any();
+        kani::assume(idx < Iterator::size_hint(&zip).0);
+        let _ = unsafe { zip.__iterator_get_unchecked(idx) };
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_zip_iterator_get_unchecked_unit() {
+        const MAX_LEN: usize = 8;
+        let arr_a: [(); MAX_LEN] = [(); MAX_LEN];
+        let arr_b: [(); MAX_LEN] = [(); MAX_LEN];
+        let slice_a = kani::slice::any_slice_of_array(&arr_a);
+        let slice_b = kani::slice::any_slice_of_array(&arr_b);
+        let mut zip = Zip::new(slice_a.iter(), slice_b.iter());
+        let idx: usize = kani::any();
+        kani::assume(idx < Iterator::size_hint(&zip).0);
+        let _ = unsafe { zip.__iterator_get_unchecked(idx) };
+    }
+
+    // --- Safe abstractions ---
+
+    // next (TRA specialized — uses __iterator_get_unchecked internally)
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_zip_next_u8() {
+        const MAX_LEN: usize = 8;
+        let arr_a: [u8; MAX_LEN] = kani::any();
+        let arr_b: [u8; MAX_LEN] = kani::any();
+        let slice_a = kani::slice::any_slice_of_array(&arr_a);
+        let slice_b = kani::slice::any_slice_of_array(&arr_b);
+        let mut zip = Zip::new(slice_a.iter(), slice_b.iter());
+        let expected = cmp::min(slice_a.len(), slice_b.len());
+        let mut count = 0usize;
+        while let Some(_) = Iterator::next(&mut zip) {
+            count += 1;
+        }
+        assert_eq!(count, expected);
+    }
+
+    // nth (TRA specialized — uses __iterator_get_unchecked for side effects)
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_zip_nth_u8() {
+        const MAX_LEN: usize = 8;
+        let arr_a: [u8; MAX_LEN] = kani::any();
+        let arr_b: [u8; MAX_LEN] = kani::any();
+        let slice_a = kani::slice::any_slice_of_array(&arr_a);
+        let slice_b = kani::slice::any_slice_of_array(&arr_b);
+        let mut zip = Zip::new(slice_a.iter(), slice_b.iter());
+        let n: usize = kani::any();
+        kani::assume(n <= MAX_LEN);
+        let _ = Iterator::nth(&mut zip, n);
+    }
+
+    // next_back (TRA specialized — uses __iterator_get_unchecked internally)
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_zip_next_back_u8() {
+        const MAX_LEN: usize = 8;
+        let arr_a: [u8; MAX_LEN] = kani::any();
+        let arr_b: [u8; MAX_LEN] = kani::any();
+        let slice_a = kani::slice::any_slice_of_array(&arr_a);
+        let slice_b = kani::slice::any_slice_of_array(&arr_b);
+        let mut zip = Zip::new(slice_a.iter(), slice_b.iter());
+        while let Some(_) = DoubleEndedIterator::next_back(&mut zip) {}
+    }
+
+    // fold (TRANC specialized — uses get_unchecked in a loop)
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_zip_fold_u8() {
+        const MAX_LEN: usize = 8;
+        let arr_a: [u8; MAX_LEN] = kani::any();
+        let arr_b: [u8; MAX_LEN] = kani::any();
+        let slice_a = kani::slice::any_slice_of_array(&arr_a);
+        let slice_b = kani::slice::any_slice_of_array(&arr_b);
+        let zip = Zip::new(slice_a.iter(), slice_b.iter());
+        let expected = cmp::min(slice_a.len(), slice_b.len());
+        let count = Iterator::fold(zip, 0usize, |acc, _| acc + 1);
+        assert_eq!(count, expected);
+    }
+
+    // spec_fold (TrustedLen specialized — uses unwrap_unchecked)
+    // RepeatN implements TrustedLen but NOT TrustedRandomAccessNoCoerce,
+    // so Zip::fold delegates to SpecFold::spec_fold (the TrustedLen path).
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_zip_spec_fold() {
+        let len_a: usize = kani::any();
+        let len_b: usize = kani::any();
+        kani::assume(len_a <= 8);
+        kani::assume(len_b <= 8);
+        let zip = Zip::new(iter::repeat_n(1u8, len_a), iter::repeat_n(2u8, len_b));
+        let count = Iterator::fold(zip, 0usize, |acc, _| acc + 1);
+        assert_eq!(count, cmp::min(len_a, len_b));
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_zip_iterator_get_unchecked_char() {
+        const MAX_LEN: usize = 8;
+        let arr_a: [char; MAX_LEN] = kani::any();
+        let arr_b: [char; MAX_LEN] = kani::any();
+        let slice_a = kani::slice::any_slice_of_array(&arr_a);
+        let slice_b = kani::slice::any_slice_of_array(&arr_b);
+        let mut zip = Zip::new(slice_a.iter(), slice_b.iter());
+        let idx: usize = kani::any();
+        kani::assume(idx < Iterator::size_hint(&zip).0);
+        let _ = unsafe { zip.__iterator_get_unchecked(idx) };
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_zip_iterator_get_unchecked_tup() {
+        const MAX_LEN: usize = 8;
+        let arr_a: [(char, u8); MAX_LEN] = kani::any();
+        let arr_b: [(char, u8); MAX_LEN] = kani::any();
+        let slice_a = kani::slice::any_slice_of_array(&arr_a);
+        let slice_b = kani::slice::any_slice_of_array(&arr_b);
+        let mut zip = Zip::new(slice_a.iter(), slice_b.iter());
+        let idx: usize = kani::any();
+        kani::assume(idx < Iterator::size_hint(&zip).0);
+        let _ = unsafe { zip.__iterator_get_unchecked(idx) };
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_zip_next_char() {
+        const MAX_LEN: usize = 8;
+        let arr_a: [char; MAX_LEN] = kani::any();
+        let arr_b: [char; MAX_LEN] = kani::any();
+        let slice_a = kani::slice::any_slice_of_array(&arr_a);
+        let slice_b = kani::slice::any_slice_of_array(&arr_b);
+        let mut zip = Zip::new(slice_a.iter(), slice_b.iter());
+        let expected = cmp::min(slice_a.len(), slice_b.len());
+        let mut count = 0usize;
+        while let Some(_) = Iterator::next(&mut zip) {
+            count += 1;
+        }
+        assert_eq!(count, expected);
+    }
+
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_zip_fold_char() {
+        const MAX_LEN: usize = 8;
+        let arr_a: [char; MAX_LEN] = kani::any();
+        let arr_b: [char; MAX_LEN] = kani::any();
+        let slice_a = kani::slice::any_slice_of_array(&arr_a);
+        let slice_b = kani::slice::any_slice_of_array(&arr_b);
+        let zip = Zip::new(slice_a.iter(), slice_b.iter());
+        let expected = cmp::min(slice_a.len(), slice_b.len());
+        let count = Iterator::fold(zip, 0usize, |acc, _| acc + 1);
+        assert_eq!(count, expected);
+    }
+}