diff --git a/library/core/src/iter/range.rs b/library/core/src/iter/range.rs
index 4fa719de5ebf0..ec0be9439cfe1 100644
--- a/library/core/src/iter/range.rs
+++ b/library/core/src/iter/range.rs
@@ -1,7 +1,11 @@
+use safety::requires;
+
 use super::{
     FusedIterator, TrustedLen, TrustedRandomAccess, TrustedRandomAccessNoCoerce, TrustedStep,
 };
 use crate::ascii::Char as AsciiChar;
+#[cfg(kani)]
+use crate::kani;
 use crate::mem;
 use crate::net::{Ipv4Addr, Ipv6Addr};
 use crate::num::NonZero;
@@ -183,12 +187,14 @@ pub trait Step: Clone + PartialOrd + Sized {
 // than the signed::MAX value. Therefore `as` casting to the signed type would be incorrect.
 macro_rules! step_signed_methods {
     ($unsigned: ty) => {
+        #[requires(start.checked_add_unsigned(n as $unsigned).is_some())]
         #[inline]
         unsafe fn forward_unchecked(start: Self, n: usize) -> Self {
             // SAFETY: the caller has to guarantee that `start + n` doesn't overflow.
             unsafe { start.checked_add_unsigned(n as $unsigned).unwrap_unchecked() }
         }
 
+        #[requires(start.checked_sub_unsigned(n as $unsigned).is_some())]
         #[inline]
         unsafe fn backward_unchecked(start: Self, n: usize) -> Self {
             // SAFETY: the caller has to guarantee that `start - n` doesn't overflow.
@@ -199,12 +205,14 @@ macro_rules! step_signed_methods {
 
 macro_rules! step_unsigned_methods {
     () => {
+        #[requires(start.checked_add(n as Self).is_some())]
         #[inline]
         unsafe fn forward_unchecked(start: Self, n: usize) -> Self {
             // SAFETY: the caller has to guarantee that `start + n` doesn't overflow.
             unsafe { start.unchecked_add(n as Self) }
         }
 
+        #[requires(start.checked_sub(n as Self).is_some())]
         #[inline]
         unsafe fn backward_unchecked(start: Self, n: usize) -> Self {
             // SAFETY: the caller has to guarantee that `start - n` doesn't overflow.