diff --git a/library/core/src/iter/traits/unchecked_iterator.rs b/library/core/src/iter/traits/unchecked_iterator.rs
index ae4bfcad4e68f..f32eb82b8a552 100644
--- a/library/core/src/iter/traits/unchecked_iterator.rs
+++ b/library/core/src/iter/traits/unchecked_iterator.rs
@@ -1,4 +1,8 @@
+use safety::requires;
+
 use crate::iter::TrustedLen;
+#[cfg(kani)]
+use crate::kani;
 
 /// [`TrustedLen`] cannot have methods, so this allows augmenting it.
 ///
@@ -27,6 +31,8 @@ pub(crate) trait UncheckedIterator: TrustedLen {
     /// point you might want to implement this manually instead.
     #[unstable(feature = "trusted_len_next_unchecked", issue = "37572")]
     #[inline]
+    #[requires(self.size_hint().0 != 0 && self.size_hint().1 != Some(0))]
+    #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn next_unchecked(&mut self) -> Self::Item {
         let opt = self.next();
         // SAFETY: The caller promised that we're not empty, and
@@ -34,3 +40,17 @@ pub(crate) trait UncheckedIterator: TrustedLen {
         unsafe { opt.unwrap_unchecked() }
     }
 }
+
+#[cfg(kani)]
+#[kani::proof]
+fn verify_next_unchecked() {
+    let arr: [u8; 1] = [kani::any(); 1];
+
+    let mut it = arr.iter();
+    let (lo_hint, hi_hint) = it.size_hint();
+
+    kani::assume(lo_hint != 0);
+    kani::assume(hi_hint != Some(0));
+
+    let _ = unsafe { it.next_unchecked() };
+}