diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs
index b2cecbf053c81..ec67d891686fd 100644
--- a/library/core/src/ptr/const_ptr.rs
+++ b/library/core/src/ptr/const_ptr.rs
@@ -406,6 +406,21 @@ impl<T: ?Sized> *const T {
     #[rustc_const_stable(feature = "const_ptr_offset", since = "1.61.0")]
     #[inline(always)]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+    #[requires(
+        // Precondition 1: the computed offset `count * size_of::<T>()` does not overflow `isize`.
+        // Precondition 2: adding the computed offset to `self` does not cause overflow.
+        // These two preconditions are combined for performance reason, as multiplication is computationally expensive in Kani.
+        count.checked_mul(core::mem::size_of::<T>() as isize)
+        .map_or(false, |computed_offset| (self as isize).checked_add(computed_offset).is_some()) &&
+        // Precondition 3: If `T` is a unit type (`size_of::<T>() == 0`), this check is unnecessary as it has no allocated memory.
+        // Otherwise, for non-unit types, `self` and `self.wrapping_offset(count)` should point to the same allocated object,
+        // restricting `count` to prevent crossing allocation boundaries.
+        ((core::mem::size_of::<T>() == 0) || (core::ub_checks::same_allocation(self, self.wrapping_offset(count))))
+    )]
+    // Postcondition: If `T` is a unit type (`size_of::<T>() == 0`), no allocation check is needed.
+    // Otherwise, for non-unit types, ensure that `self` and `result` point to the same allocated object,
+    // verifying that the result remains within the same allocation as `self`.
+    #[ensures(|result| (core::mem::size_of::<T>() == 0) || core::ub_checks::same_allocation(self, *result as *const T))]
     pub const unsafe fn offset(self, count: isize) -> *const T
     where
         T: Sized,
@@ -673,7 +688,7 @@ impl<T: ?Sized> *const T {
         // Ensure the distance between `self` and `origin` is aligned to `T`
         (self as isize - origin as isize) % (mem::size_of::<T>() as isize) == 0 &&
         // Ensure both pointers are in the same allocation or are pointing to the same address
-        (self as isize == origin as isize || kani::mem::same_allocation(self, origin))
+        (self as isize == origin as isize || core::ub_checks::same_allocation(self, origin))
     )]
     // The result should equal the distance in terms of elements of type `T` as per the documentation above
     #[ensures(|result| *result == (self as isize - origin as isize) / (mem::size_of::<T>() as isize))]
@@ -928,6 +943,23 @@ impl<T: ?Sized> *const T {
     #[rustc_const_stable(feature = "const_ptr_offset", since = "1.61.0")]
     #[inline(always)]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+    #[requires(
+        // Precondition 1: the computed offset `count * size_of::<T>()` does not overflow `isize`.
+        // Precondition 2: adding the computed offset to `self` does not cause overflow.
+        // These two preconditions are combined for performance reason, as multiplication is computationally expensive in Kani. 
+        count.checked_mul(core::mem::size_of::<T>())
+        .map_or(false, |computed_offset| {
+            computed_offset <= isize::MAX as usize && (self as isize).checked_add(computed_offset as isize).is_some()
+        }) &&
+        // Precondition 3: If `T` is a unit type (`size_of::<T>() == 0`), this check is unnecessary as it has no allocated memory.
+        // Otherwise, for non-unit types, `self` and `self.wrapping_add(count)` should point to the same allocated object,
+        // restricting `count` to prevent crossing allocation boundaries.
+        ((core::mem::size_of::<T>() == 0) || (core::ub_checks::same_allocation(self, self.wrapping_add(count))))
+    )]
+    // Postcondition: If `T` is a unit type (`size_of::<T>() == 0`), no allocation check is needed.
+    // Otherwise, for non-unit types, ensure that `self` and `result` point to the same allocated object,
+    // verifying that the result remains within the same allocation as `self`.
+    #[ensures(|result| (core::mem::size_of::<T>() == 0) || core::ub_checks::same_allocation(self, *result as *const T))]
     pub const unsafe fn add(self, count: usize) -> Self
     where
         T: Sized,
@@ -1035,6 +1067,23 @@ impl<T: ?Sized> *const T {
     #[cfg_attr(bootstrap, rustc_allow_const_fn_unstable(unchecked_neg))]
     #[inline(always)]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+    #[requires(
+        // Precondition 1: the computed offset `count * size_of::<T>()` does not overflow `isize`.
+        // Precondition 2: substracting the computed offset from `self` does not cause overflow.
+        // These two preconditions are combined for performance reason, as multiplication is computationally expensive in Kani.
+        count.checked_mul(core::mem::size_of::<T>())
+        .map_or(false, |computed_offset| {
+            computed_offset <= isize::MAX as usize && (self as isize).checked_sub(computed_offset as isize).is_some()
+        }) &&
+        // Precondition 3: If `T` is a unit type (`size_of::<T>() == 0`), this check is unnecessary as it has no allocated memory.
+        // Otherwise, for non-unit types, `self` and `self.wrapping_sub(count)` should point to the same allocated object,
+        // restricting `count` to prevent crossing allocation boundaries.
+        ((core::mem::size_of::<T>() == 0) || (core::ub_checks::same_allocation(self, self.wrapping_sub(count))))
+    )]
+    // Postcondition: If `T` is a unit type (`size_of::<T>() == 0`), no allocation check is needed.
+    // Otherwise, for non-unit types, ensure that `self` and `result` point to the same allocated object,
+    // verifying that the result remains within the same allocation as `self`.
+    #[ensures(|result| (core::mem::size_of::<T>() == 0) || core::ub_checks::same_allocation(self, *result as *const T))]
     pub const unsafe fn sub(self, count: usize) -> Self
     where
         T: Sized,
@@ -1726,19 +1775,300 @@ mod verify {
     use core::mem;
     use kani::PointerGenerator;
 
-    // Proof for unit size will panic as offset_from needs the pointee size to be greater then 0
-    #[kani::proof_for_contract(<*const ()>::offset_from)]
-    #[kani::should_panic]
-    pub fn check_const_offset_from_unit() {
-        let val: () = ();
-        let src_ptr: *const () = &val;
-        let dest_ptr: *const () = &val;
-        unsafe {
-            dest_ptr.offset_from(src_ptr);
-        }
+    /// This macro generates a single verification harness for the `offset`, `add`, or `sub`
+    /// pointer operations, supporting integer, composite, or unit types.
+    /// - `$ty`: The type of the slice's elements (e.g., `i32`, `u32`, tuples).
+    /// - `$fn_name`: The name of the function being checked (`add`, `sub`, or `offset`).
+    /// - `$proof_name`: The name assigned to the generated proof for the contract.
+    /// - `$count_ty:ty`: The type of the input variable passed to the method being invoked.
+    ///
+    /// Note: This macro is intended for internal use only and should be invoked exclusively
+    /// by the `generate_arithmetic_harnesses` macro. Its purpose is to reduce code duplication,
+    /// and it is not meant to be used directly elsewhere in the codebase.
+    macro_rules! generate_single_arithmetic_harness {
+        ($ty:ty, $proof_name:ident, $fn_name:ident, $count_ty:ty) => {
+            #[kani::proof_for_contract(<*const $ty>::$fn_name)]
+            pub fn $proof_name() {
+                // 200 bytes are large enough to cover all pointee types used for testing
+                const BUF_SIZE: usize = 200;
+                let mut generator = kani::PointerGenerator::<BUF_SIZE>::new();
+                let test_ptr: *const $ty = generator.any_in_bounds().ptr;
+                let count: $count_ty = kani::any();
+                unsafe {
+                    test_ptr.$fn_name(count);
+                }
+            }
+        };
+    }
+
+    /// This macro generates verification harnesses for the `offset`, `add`, and `sub`
+    /// pointer operations, supporting integer, composite, or unit types.
+    /// - `$ty`: The pointee type (e.g., i32, u32, tuples).
+    /// - `$offset_fn_name`: The name for the `offset` proof for contract.
+    /// - `$add_fn_name`: The name for the `add` proof for contract.
+    /// - `$sub_fn_name`: The name for the `sub` proof for contract.
+    macro_rules! generate_arithmetic_harnesses {
+        ($ty:ty, $add_fn_name:ident, $sub_fn_name:ident, $offset_fn_name:ident) => {
+            generate_single_arithmetic_harness!($ty, $add_fn_name, add, usize);
+            generate_single_arithmetic_harness!($ty, $sub_fn_name, sub, usize);
+            generate_single_arithmetic_harness!($ty, $offset_fn_name, offset, isize);
+        };
     }
 
-    // Array size bound for kani::any_array
+    // Generate harnesses for unit type (add, sub, offset)
+    generate_arithmetic_harnesses!(
+        (),
+        check_const_add_unit,
+        check_const_sub_unit,
+        check_const_offset_unit
+    );
+
+    // Generate harnesses for integer types (add, sub, offset)
+    generate_arithmetic_harnesses!(
+        i8,
+        check_const_add_i8,
+        check_const_sub_i8,
+        check_const_offset_i8
+    );
+    generate_arithmetic_harnesses!(
+        i16,
+        check_const_add_i16,
+        check_const_sub_i16,
+        check_const_offset_i16
+    );
+    generate_arithmetic_harnesses!(
+        i32,
+        check_const_add_i32,
+        check_const_sub_i32,
+        check_const_offset_i32
+    );
+    generate_arithmetic_harnesses!(
+        i64,
+        check_const_add_i64,
+        check_const_sub_i64,
+        check_const_offset_i64
+    );
+    generate_arithmetic_harnesses!(
+        i128,
+        check_const_add_i128,
+        check_const_sub_i128,
+        check_const_offset_i128
+    );
+    generate_arithmetic_harnesses!(
+        isize,
+        check_const_add_isize,
+        check_const_sub_isize,
+        check_const_offset_isize
+    );
+    generate_arithmetic_harnesses!(
+        u8,
+        check_const_add_u8,
+        check_const_sub_u8,
+        check_const_offset_u8
+    );
+    generate_arithmetic_harnesses!(
+        u16,
+        check_const_add_u16,
+        check_const_sub_u16,
+        check_const_offset_u16
+    );
+    generate_arithmetic_harnesses!(
+        u32,
+        check_const_add_u32,
+        check_const_sub_u32,
+        check_const_offset_u32
+    );
+    generate_arithmetic_harnesses!(
+        u64,
+        check_const_add_u64,
+        check_const_sub_u64,
+        check_const_offset_u64
+    );
+    generate_arithmetic_harnesses!(
+        u128,
+        check_const_add_u128,
+        check_const_sub_u128,
+        check_const_offset_u128
+    );
+    generate_arithmetic_harnesses!(
+        usize,
+        check_const_add_usize,
+        check_const_sub_usize,
+        check_const_offset_usize
+    );
+
+    // Generte harnesses for composite types (add, sub, offset)
+    generate_arithmetic_harnesses!(
+        (i8, i8),
+        check_const_add_tuple_1,
+        check_const_sub_tuple_1,
+        check_const_offset_tuple_1
+    );
+    generate_arithmetic_harnesses!(
+        (f64, bool),
+        check_const_add_tuple_2,
+        check_const_sub_tuple_2,
+        check_const_offset_tuple_2
+    );
+    generate_arithmetic_harnesses!(
+        (i32, f64, bool),
+        check_const_add_tuple_3,
+        check_const_sub_tuple_3,
+        check_const_offset_tuple_3
+    );
+    generate_arithmetic_harnesses!(
+        (i8, u16, i32, u64, isize),
+        check_const_add_tuple_4,
+        check_const_sub_tuple_4,
+        check_const_offset_tuple_4
+    );
+
+    // Constant for array size used in all tests
+    const ARRAY_SIZE: usize = 5;
+
+    /// This macro generates a single verification harness for the `offset`, `add`, or `sub`
+    /// pointer operations for a slice type.
+    /// - `$ty`: The type of the array's elements (e.g., `i32`, `u32`, tuples).
+    /// - `$fn_name`: The name of the function being checked (`add`, `sub`, or `offset`).
+    /// - `$proof_name`: The name assigned to the generated proof for the contract.
+    /// - `$count_ty:ty`: The type of the input variable passed to the method being invoked.
+    ///
+    /// Note: This macro is intended for internal use only and should be invoked exclusively
+    /// by the `generate_slice_harnesses` macro. Its purpose is to reduce code duplication,
+    /// and it is not meant to be used directly elsewhere in the codebase.
+    macro_rules! generate_single_slice_harness {
+        ($ty:ty, $proof_name:ident, $fn_name:ident, $count_ty:ty) => {
+            #[kani::proof_for_contract(<*const $ty>::$fn_name)]
+            fn $proof_name() {
+                let arr: [$ty; ARRAY_SIZE] = kani::Arbitrary::any_array();
+                let test_ptr: *const $ty = arr.as_ptr();
+                let offset: usize = kani::any();
+                kani::assume(offset <= ARRAY_SIZE * mem::size_of::<$ty>());
+                let ptr_with_offset: *const $ty = test_ptr.wrapping_byte_add(offset);
+
+                let count: $count_ty = kani::any();
+                unsafe {
+                    ptr_with_offset.$fn_name(count);
+                }
+            }
+        };
+    }
+
+    /// This macro generates verification harnesses for the `offset`, `add`, and `sub`
+    /// pointer operations for a slice type.
+    /// - `$ty`: The type of the array (e.g., i32, u32, tuples).
+    /// - `$offset_fn_name`: The name for the `offset` proof for contract.
+    /// - `$add_fn_name`: The name for the `add` proof for contract.
+    /// - `$sub_fn_name`: The name for the `sub` proof for contract.
+    macro_rules! generate_slice_harnesses {
+        ($ty:ty, $add_fn_name:ident, $sub_fn_name:ident, $offset_fn_name:ident) => {
+            generate_single_slice_harness!($ty, $add_fn_name, add, usize);
+            generate_single_slice_harness!($ty, $sub_fn_name, sub, usize);
+            generate_single_slice_harness!($ty, $offset_fn_name, offset, isize);
+        };
+    }
+
+    // Generate slice harnesses for various types (add, sub, offset)
+    generate_slice_harnesses!(
+        i8,
+        check_const_add_slice_i8,
+        check_const_sub_slice_i8,
+        check_const_offset_slice_i8
+    );
+    generate_slice_harnesses!(
+        i16,
+        check_const_add_slice_i16,
+        check_const_sub_slice_i16,
+        check_const_offset_slice_i16
+    );
+    generate_slice_harnesses!(
+        i32,
+        check_const_add_slice_i32,
+        check_const_sub_slice_i32,
+        check_const_offset_slice_i32
+    );
+    generate_slice_harnesses!(
+        i64,
+        check_const_add_slice_i64,
+        check_const_sub_slice_i64,
+        check_const_offset_slice_i64
+    );
+    generate_slice_harnesses!(
+        i128,
+        check_const_add_slice_i128,
+        check_const_sub_slice_i128,
+        check_const_offset_slice_i128
+    );
+    generate_slice_harnesses!(
+        isize,
+        check_const_add_slice_isize,
+        check_const_sub_slice_isize,
+        check_const_offset_slice_isize
+    );
+    generate_slice_harnesses!(
+        u8,
+        check_const_add_slice_u8,
+        check_const_sub_slice_u8,
+        check_const_offset_slice_u8
+    );
+    generate_slice_harnesses!(
+        u16,
+        check_const_add_slice_u16,
+        check_const_sub_slice_u16,
+        check_const_offset_slice_u16
+    );
+    generate_slice_harnesses!(
+        u32,
+        check_const_add_slice_u32,
+        check_const_sub_slice_u32,
+        check_const_offset_slice_u32
+    );
+    generate_slice_harnesses!(
+        u64,
+        check_const_add_slice_u64,
+        check_const_sub_slice_u64,
+        check_const_offset_slice_u64
+    );
+    generate_slice_harnesses!(
+        u128,
+        check_const_add_slice_u128,
+        check_const_sub_slice_u128,
+        check_const_offset_slice_u128
+    );
+    generate_slice_harnesses!(
+        usize,
+        check_const_add_slice_usize,
+        check_const_sub_slice_usize,
+        check_const_offset_slice_usize
+    );
+
+    // Generate slice harnesses for tuples (add, sub, offset)
+    generate_slice_harnesses!(
+        (i8, i8),
+        check_const_add_slice_tuple_1,
+        check_const_sub_slice_tuple_1,
+        check_const_offset_slice_tuple_1
+    );
+    generate_slice_harnesses!(
+        (f64, bool),
+        check_const_add_slice_tuple_2,
+        check_const_sub_slice_tuple_2,
+        check_const_offset_slice_tuple_2
+    );
+    generate_slice_harnesses!(
+        (i32, f64, bool),
+        check_const_add_slice_tuple_3,
+        check_const_sub_slice_tuple_3,
+        check_const_offset_slice_tuple_3
+    );
+    generate_slice_harnesses!(
+        (i8, u16, i32, u64, isize),
+        check_const_add_slice_tuple_4,
+        check_const_sub_slice_tuple_4,
+        check_const_offset_slice_tuple_4
+    );
+
+    // Array size bound for kani::any_array for `offset_from` verification
     const ARRAY_LEN: usize = 40;
 
     macro_rules! generate_offset_from_harness {
@@ -1781,6 +2111,19 @@ mod verify {
         };
     }
 
+    // Proof for unit size will panic as offset_from needs the pointee size to be greater then 0
+    #[kani::proof_for_contract(<*const ()>::offset_from)]
+    #[kani::should_panic]
+    pub fn check_const_offset_from_unit() {
+        let val: () = ();
+        let src_ptr: *const () = &val;
+        let dest_ptr: *const () = &val;
+        unsafe {
+            dest_ptr.offset_from(src_ptr);
+        }
+    }
+
+    // fn <*const T>::offset_from() integer and integer slice types verification
     generate_offset_from_harness!(
         u8,
         check_const_offset_from_u8,
@@ -1811,7 +2154,6 @@ mod verify {
         check_const_offset_from_usize,
         check_const_offset_from_usize_arr
     );
-
     generate_offset_from_harness!(
         i8,
         check_const_offset_from_i8,
@@ -1843,6 +2185,7 @@ mod verify {
         check_const_offset_from_isize_arr
     );
 
+    // fn <*const T>::offset_from() tuple and tuple slice types verification
     generate_offset_from_harness!(
         (i8, i8),
         check_const_offset_from_tuple_1,