diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs
index 57a7c0fc0925c..db5b08e59be90 100644
--- a/library/core/src/ptr/const_ptr.rs
+++ b/library/core/src/ptr/const_ptr.rs
@@ -3,6 +3,11 @@ use crate::cmp::Ordering::{Equal, Greater, Less};
 use crate::intrinsics::const_eval_select;
 use crate::mem::SizedTypeProperties;
 use crate::slice::{self, SliceIndex};
+use safety::{ensures, requires};
+
+#[cfg(kani)]
+use crate::kani;
+use core::mem;
 
 impl<T: ?Sized> *const T {
     /// Returns `true` if the pointer is null.
@@ -459,6 +464,22 @@ impl<T: ?Sized> *const T {
     #[stable(feature = "pointer_byte_offsets", since = "1.75.0")]
     #[rustc_const_stable(feature = "const_pointer_byte_offsets", since = "1.75.0")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+    #[requires(
+        // If the size of the pointee is zero, then `count` must also be zero
+        (mem::size_of_val_raw(self) == 0 && count == 0) ||
+        // If the size of the pointee is not zero, then ensure that adding `count`
+        // bytes doesn't cause overflow and that both pointers `self` and the result
+        // are pointing to the same address or in the same allocation
+        (mem::size_of_val_raw(self) != 0 &&
+            (self as *const u8 as isize).checked_add(count).is_some() &&
+            ((self as *const u8 as usize) == (self.wrapping_byte_offset(count) as *const u8 as usize) ||
+                kani::mem::same_allocation(self, self.wrapping_byte_offset(count))))
+    )]
+    #[ensures(|result|
+        // The resulting pointer should either be unchanged or still point to the same allocation
+        ((self as *const u8 as usize) == (*result as *const u8 as usize)) ||
+        (kani::mem::same_allocation(self, *result))
+    )]
     pub const unsafe fn byte_offset(self, count: isize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `offset`.
         unsafe { self.cast::<u8>().offset(count).with_metadata_of(self) }
@@ -972,6 +993,22 @@ impl<T: ?Sized> *const T {
     #[stable(feature = "pointer_byte_offsets", since = "1.75.0")]
     #[rustc_const_stable(feature = "const_pointer_byte_offsets", since = "1.75.0")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+    #[requires(
+        // If the size of the pointee is zero, then `count` must also be zero
+        (mem::size_of_val_raw(self) == 0 && count == 0) ||
+        // If the size of the pointee is not zero, then ensure that adding `count`
+        // bytes doesn't cause overflow and that both pointers `self` and the result
+        // are pointing to the same address or in the same allocation
+        (mem::size_of_val_raw(self) != 0 &&
+            (self as *const u8 as isize).checked_add(count as isize).is_some() &&
+            ((self as *const u8 as usize) == (self.wrapping_byte_add(count) as *const u8 as usize) ||
+                kani::mem::same_allocation(self, self.wrapping_byte_add(count))))
+    )]
+    #[ensures(|result|
+        // The resulting pointer should either be unchanged or still point to the same allocation
+        ((self as *const u8 as usize) == (*result as *const u8 as usize)) ||
+        (kani::mem::same_allocation(self, *result))
+    )]
     pub const unsafe fn byte_add(self, count: usize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `add`.
         unsafe { self.cast::<u8>().add(count).with_metadata_of(self) }
@@ -1087,6 +1124,22 @@ impl<T: ?Sized> *const T {
     #[stable(feature = "pointer_byte_offsets", since = "1.75.0")]
     #[rustc_const_stable(feature = "const_pointer_byte_offsets", since = "1.75.0")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+    #[requires(
+        // If the size of the pointee is zero, then `count` must also be zero
+        (mem::size_of_val_raw(self) == 0 && count == 0) ||
+        // If the size of the pointee is not zero then ensure that adding `count`
+        // bytes doesn't cause overflow and that both pointers `self` and the result
+        // would be pointing to the same address or in the same allocation
+        (mem::size_of_val_raw(self) != 0 &&
+            (self as *const u8 as isize).checked_sub(count as isize).is_some() &&
+            ((self as *const u8 as usize) == (self.wrapping_byte_sub(count) as *const u8 as usize) ||
+                kani::mem::same_allocation(self, self.wrapping_byte_sub(count))))
+    )]
+    #[ensures(|result|
+         // The resulting pointer should either be unchanged or still point to the same allocation
+        ((self as *const u8 as isize) == (*result as *const u8 as isize)) ||
+        (kani::mem::same_allocation(self, *result))
+    )]
     pub const unsafe fn byte_sub(self, count: usize) -> Self {
         // SAFETY: the caller must uphold the safety contract for `sub`.
         unsafe { self.cast::<u8>().sub(count).with_metadata_of(self) }
@@ -1899,3 +1952,249 @@ impl<T: ?Sized> PartialOrd for *const T {
         *self >= *other
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+pub mod verify {
+    use crate::kani;
+    use core::mem;
+    use kani::PointerGenerator;
+
+    // generate proof for contracts of byte_add, byte_sub and byte_offset to verify
+    // unit pointee type
+    // - `$fn_name`: function for which the contract must be verified
+    // - `$proof_name`: name of the harness generated
+    macro_rules! gen_const_byte_arith_harness_for_unit {
+        (byte_offset, $proof_name:ident) => {
+            #[kani::proof_for_contract(<*const ()>::byte_offset)]
+            pub fn $proof_name() {
+                let val = ();
+                let ptr: *const () = &val;
+                let count: isize = kani::any();
+                unsafe {
+                    ptr.byte_offset(count);
+                }
+            }
+        };
+
+        ($fn_name:ident, $proof_name:ident) => {
+            #[kani::proof_for_contract(<*const ()>::$fn_name)]
+            pub fn $proof_name() {
+                let val = ();
+                let ptr: *const () = &val;
+                //byte_add and byte_sub need count to be usize unlike byte_offset
+                let count: usize = kani::any();
+                unsafe {
+                    ptr.$fn_name(count);
+                }
+            }
+        };
+    }
+
+    gen_const_byte_arith_harness_for_unit!(byte_add, check_const_byte_add_unit);
+    gen_const_byte_arith_harness_for_unit!(byte_sub, check_const_byte_sub_unit);
+    gen_const_byte_arith_harness_for_unit!(byte_offset, check_const_byte_offset_unit);
+
+    // bounding space for PointerGenerator to accommodate 40 elements.
+    const ARRAY_LEN: usize = 40;
+
+    // generate proof for contracts for byte_add, byte_sub and byte_offset
+    // - `$type`: pointee type
+    // - `$fn_name`: function for which the contract must be verified
+    // - `$proof_name`: name of the harness generated
+    macro_rules! gen_const_byte_arith_harness {
+        ($type:ty, byte_offset, $proof_name:ident) => {
+            #[kani::proof_for_contract(<*const $type>::byte_offset)]
+            pub fn $proof_name() {
+                // generator with space for single element
+                let mut generator1 = PointerGenerator::<{ mem::size_of::<$type>() }>::new();
+                // generator with space for multiple elements
+                let mut generator2 =
+                    PointerGenerator::<{ mem::size_of::<$type>() * ARRAY_LEN }>::new();
+
+                let ptr: *const $type = if kani::any() {
+                    generator1.any_in_bounds().ptr
+                } else {
+                    generator2.any_in_bounds().ptr
+                };
+
+                let count: isize = kani::any();
+
+                unsafe {
+                    ptr.byte_offset(count);
+                }
+            }
+        };
+
+        ($type:ty, $fn_name:ident, $proof_name:ident) => {
+            #[kani::proof_for_contract(<*const $type>::$fn_name)]
+            pub fn $proof_name() {
+                // generator with space for single element
+                let mut generator1 = PointerGenerator::<{ mem::size_of::<$type>() }>::new();
+                // generator with space for multiple elements
+                let mut generator2 =
+                    PointerGenerator::<{ mem::size_of::<$type>() * ARRAY_LEN }>::new();
+
+                let ptr: *const $type = if kani::any() {
+                    generator1.any_in_bounds().ptr
+                } else {
+                    generator2.any_in_bounds().ptr
+                };
+
+                //byte_add and byte_sub need count to be usize unlike byte_offset
+                let count: usize = kani::any();
+
+                unsafe {
+                    ptr.$fn_name(count);
+                }
+            }
+        };
+    }
+
+    gen_const_byte_arith_harness!(i8, byte_add, check_const_byte_add_i8);
+    gen_const_byte_arith_harness!(i16, byte_add, check_const_byte_add_i16);
+    gen_const_byte_arith_harness!(i32, byte_add, check_const_byte_add_i32);
+    gen_const_byte_arith_harness!(i64, byte_add, check_const_byte_add_i64);
+    gen_const_byte_arith_harness!(i128, byte_add, check_const_byte_add_i128);
+    gen_const_byte_arith_harness!(isize, byte_add, check_const_byte_add_isize);
+    gen_const_byte_arith_harness!(u8, byte_add, check_const_byte_add_u8);
+    gen_const_byte_arith_harness!(u16, byte_add, check_const_byte_add_u16);
+    gen_const_byte_arith_harness!(u32, byte_add, check_const_byte_add_u32);
+    gen_const_byte_arith_harness!(u64, byte_add, check_const_byte_add_u64);
+    gen_const_byte_arith_harness!(u128, byte_add, check_const_byte_add_u128);
+    gen_const_byte_arith_harness!(usize, byte_add, check_const_byte_add_usize);
+    gen_const_byte_arith_harness!((i8, i8), byte_add, check_const_byte_add_tuple_1);
+    gen_const_byte_arith_harness!((f64, bool), byte_add, check_const_byte_add_tuple_2);
+    gen_const_byte_arith_harness!((i32, f64, bool), byte_add, check_const_byte_add_tuple_3);
+    gen_const_byte_arith_harness!(
+        (i8, u16, i32, u64, isize),
+        byte_add,
+        check_const_byte_add_tuple_4
+    );
+
+    gen_const_byte_arith_harness!(i8, byte_sub, check_const_byte_sub_i8);
+    gen_const_byte_arith_harness!(i16, byte_sub, check_const_byte_sub_i16);
+    gen_const_byte_arith_harness!(i32, byte_sub, check_const_byte_sub_i32);
+    gen_const_byte_arith_harness!(i64, byte_sub, check_const_byte_sub_i64);
+    gen_const_byte_arith_harness!(i128, byte_sub, check_const_byte_sub_i128);
+    gen_const_byte_arith_harness!(isize, byte_sub, check_const_byte_sub_isize);
+    gen_const_byte_arith_harness!(u8, byte_sub, check_const_byte_sub_u8);
+    gen_const_byte_arith_harness!(u16, byte_sub, check_const_byte_sub_u16);
+    gen_const_byte_arith_harness!(u32, byte_sub, check_const_byte_sub_u32);
+    gen_const_byte_arith_harness!(u64, byte_sub, check_const_byte_sub_u64);
+    gen_const_byte_arith_harness!(u128, byte_sub, check_const_byte_sub_u128);
+    gen_const_byte_arith_harness!(usize, byte_sub, check_const_byte_sub_usize);
+    gen_const_byte_arith_harness!((i8, i8), byte_sub, check_const_byte_sub_tuple_1);
+    gen_const_byte_arith_harness!((f64, bool), byte_sub, check_const_byte_sub_tuple_2);
+    gen_const_byte_arith_harness!((i32, f64, bool), byte_sub, check_const_byte_sub_tuple_3);
+    gen_const_byte_arith_harness!(
+        (i8, u16, i32, u64, isize),
+        byte_sub,
+        check_const_byte_sub_tuple_4
+    );
+
+    gen_const_byte_arith_harness!(i8, byte_offset, check_const_byte_offset_i8);
+    gen_const_byte_arith_harness!(i16, byte_offset, check_const_byte_offset_i16);
+    gen_const_byte_arith_harness!(i32, byte_offset, check_const_byte_offset_i32);
+    gen_const_byte_arith_harness!(i64, byte_offset, check_const_byte_offset_i64);
+    gen_const_byte_arith_harness!(i128, byte_offset, check_const_byte_offset_i128);
+    gen_const_byte_arith_harness!(isize, byte_offset, check_const_byte_offset_isize);
+    gen_const_byte_arith_harness!(u8, byte_offset, check_const_byte_offset_u8);
+    gen_const_byte_arith_harness!(u16, byte_offset, check_const_byte_offset_u16);
+    gen_const_byte_arith_harness!(u32, byte_offset, check_const_byte_offset_u32);
+    gen_const_byte_arith_harness!(u64, byte_offset, check_const_byte_offset_u64);
+    gen_const_byte_arith_harness!(u128, byte_offset, check_const_byte_offset_u128);
+    gen_const_byte_arith_harness!(usize, byte_offset, check_const_byte_offset_usize);
+    gen_const_byte_arith_harness!((i8, i8), byte_offset, check_const_byte_offset_tuple_1);
+    gen_const_byte_arith_harness!((f64, bool), byte_offset, check_const_byte_offset_tuple_2);
+    gen_const_byte_arith_harness!(
+        (i32, f64, bool),
+        byte_offset,
+        check_const_byte_offset_tuple_3
+    );
+    gen_const_byte_arith_harness!(
+        (i8, u16, i32, u64, isize),
+        byte_offset,
+        check_const_byte_offset_tuple_4
+    );
+
+    macro_rules! gen_const_byte_arith_harness_for_slice {
+        ($type:ty, byte_offset, $proof_name:ident) => {
+            #[kani::proof_for_contract(<*const [$type]>::byte_offset)]
+            pub fn $proof_name() {
+                let arr: [$type; ARRAY_LEN] = kani::Arbitrary::any_array();
+                let slice: &[$type] = kani::slice::any_slice_of_array(&arr);
+                let ptr: *const [$type] = slice;
+
+                let count: isize = kani::any();
+
+                unsafe {
+                    ptr.byte_offset(count);
+                }
+            }
+        };
+
+        ($type:ty, $fn_name: ident, $proof_name:ident) => {
+            #[kani::proof_for_contract(<*const [$type]>::$fn_name)]
+            pub fn $proof_name() {
+                let arr: [$type; ARRAY_LEN] = kani::Arbitrary::any_array();
+                let slice: &[$type] = kani::slice::any_slice_of_array(&arr);
+                let ptr: *const [$type] = slice;
+
+                //byte_add and byte_sub need count to be usize unlike byte_offset
+                let count: usize = kani::any();
+
+                unsafe {
+                    ptr.$fn_name(count);
+                }
+            }
+        };
+    }
+
+    gen_const_byte_arith_harness_for_slice!(i8, byte_add, check_const_byte_add_i8_slice);
+    gen_const_byte_arith_harness_for_slice!(i16, byte_add, check_const_byte_add_i16_slice);
+    gen_const_byte_arith_harness_for_slice!(i32, byte_add, check_const_byte_add_i32_slice);
+    gen_const_byte_arith_harness_for_slice!(i64, byte_add, check_const_byte_add_i64_slice);
+    gen_const_byte_arith_harness_for_slice!(i128, byte_add, check_const_byte_add_i128_slice);
+    gen_const_byte_arith_harness_for_slice!(isize, byte_add, check_const_byte_add_isize_slice);
+    gen_const_byte_arith_harness_for_slice!(u8, byte_add, check_const_byte_add_u8_slice);
+    gen_const_byte_arith_harness_for_slice!(u16, byte_add, check_const_byte_add_u16_slice);
+    gen_const_byte_arith_harness_for_slice!(u32, byte_add, check_const_byte_add_u32_slice);
+    gen_const_byte_arith_harness_for_slice!(u64, byte_add, check_const_byte_add_u64_slice);
+    gen_const_byte_arith_harness_for_slice!(u128, byte_add, check_const_byte_add_u128_slice);
+    gen_const_byte_arith_harness_for_slice!(usize, byte_add, check_const_byte_add_usize_slice);
+
+    gen_const_byte_arith_harness_for_slice!(i8, byte_sub, check_const_byte_sub_i8_slice);
+    gen_const_byte_arith_harness_for_slice!(i16, byte_sub, check_const_byte_sub_i16_slice);
+    gen_const_byte_arith_harness_for_slice!(i32, byte_sub, check_const_byte_sub_i32_slice);
+    gen_const_byte_arith_harness_for_slice!(i64, byte_sub, check_const_byte_sub_i64_slice);
+    gen_const_byte_arith_harness_for_slice!(i128, byte_sub, check_const_byte_sub_i128_slice);
+    gen_const_byte_arith_harness_for_slice!(isize, byte_sub, check_const_byte_sub_isize_slice);
+    gen_const_byte_arith_harness_for_slice!(u8, byte_sub, check_const_byte_sub_u8_slice);
+    gen_const_byte_arith_harness_for_slice!(u16, byte_sub, check_const_byte_sub_u16_slice);
+    gen_const_byte_arith_harness_for_slice!(u32, byte_sub, check_const_byte_sub_u32_slice);
+    gen_const_byte_arith_harness_for_slice!(u64, byte_sub, check_const_byte_sub_u64_slice);
+    gen_const_byte_arith_harness_for_slice!(u128, byte_sub, check_const_byte_sub_u128_slice);
+    gen_const_byte_arith_harness_for_slice!(usize, byte_sub, check_const_byte_sub_usize_slice);
+
+    gen_const_byte_arith_harness_for_slice!(i8, byte_offset, check_const_byte_offset_i8_slice);
+    gen_const_byte_arith_harness_for_slice!(i16, byte_offset, check_const_byte_offset_i16_slice);
+    gen_const_byte_arith_harness_for_slice!(i32, byte_offset, check_const_byte_offset_i32_slice);
+    gen_const_byte_arith_harness_for_slice!(i64, byte_offset, check_const_byte_offset_i64_slice);
+    gen_const_byte_arith_harness_for_slice!(i128, byte_offset, check_const_byte_offset_i128_slice);
+    gen_const_byte_arith_harness_for_slice!(
+        isize,
+        byte_offset,
+        check_const_byte_offset_isize_slice
+    );
+    gen_const_byte_arith_harness_for_slice!(u8, byte_offset, check_const_byte_offset_u8_slice);
+    gen_const_byte_arith_harness_for_slice!(u16, byte_offset, check_const_byte_offset_u16_slice);
+    gen_const_byte_arith_harness_for_slice!(u32, byte_offset, check_const_byte_offset_u32_slice);
+    gen_const_byte_arith_harness_for_slice!(u64, byte_offset, check_const_byte_offset_u64_slice);
+    gen_const_byte_arith_harness_for_slice!(u128, byte_offset, check_const_byte_offset_u128_slice);
+    gen_const_byte_arith_harness_for_slice!(
+        usize,
+        byte_offset,
+        check_const_byte_offset_usize_slice
+    );
+}