diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs
index a210821f08d10..32baf1b33941a 100644
--- a/library/core/src/ptr/const_ptr.rs
+++ b/library/core/src/ptr/const_ptr.rs
@@ -730,6 +730,16 @@ 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(
+        (mem::size_of_val_raw(self) != 0) &&
+        // Ensures subtracting `origin` from `self` doesn't overflow
+        (self.addr() as isize).checked_sub(origin.addr() as isize).is_some() &&
+        // Ensure both pointers are in the same allocation or are pointing to the same address
+        (self.addr() == origin.addr() ||
+            core::ub_checks::same_allocation(self as *const u8, origin as *const u8))
+    )]
+    // The result should equal the distance in terms of bytes
+    #[ensures(|result| *result == (self.addr() as isize - origin.addr() as isize))]
     pub const unsafe fn byte_offset_from<U: ?Sized>(self, origin: *const U) -> isize {
         // SAFETY: the caller must uphold the safety contract for `offset_from`.
         unsafe { self.cast::<u8>().offset_from(origin.cast::<u8>()) }
@@ -1940,7 +1950,7 @@ mod verify {
         check_const_offset_usize
     );
 
-    // Generte harnesses for composite types (add, sub, offset)
+    // Generate harnesses for composite types (add, sub, offset)
     generate_arithmetic_harnesses!(
         (i8, i8),
         check_const_add_tuple_1,
@@ -2116,6 +2126,17 @@ mod verify {
     // PointerGenerator does not support dynamic sized arrays.
     const ARRAY_LEN: usize = 40;
 
+    #[kani::proof]
+    pub fn check_const_byte_offset_from_fixed_offset() {
+        let arr: [u32; ARRAY_LEN] = kani::Arbitrary::any_array();
+        let offset: usize = kani::any_where(|&x| x <= ARRAY_LEN);
+        let origin_ptr: *const u32 = arr.as_ptr();
+        let self_ptr: *const u32 = unsafe { origin_ptr.byte_offset(offset as isize) };
+        let result: isize = unsafe { self_ptr.byte_offset_from(origin_ptr) };
+        assert_eq!(result, offset as isize);
+        assert_eq!(result, (self_ptr.addr() as isize - origin_ptr.addr() as isize));
+    }
+
     macro_rules! generate_offset_from_harness {
         ($type: ty, $proof_name1: ident, $proof_name2: ident) => {
             // Proof for a single element
@@ -2156,7 +2177,7 @@ mod verify {
         };
     }
 
-    // Proof for unit size will panic as offset_from needs the pointee size to be greater then 0
+    // Proof for unit size will panic as offset_from needs the pointee size to be greater than 0
     #[kani::proof_for_contract(<*const ()>::offset_from)]
     #[kani::should_panic]
     pub fn check_const_offset_from_unit() {
@@ -2252,6 +2273,186 @@ mod verify {
         check_const_offset_from_tuple_4_arr
     );
 
+    // Proof for contact of byte_offset_from to verify unit type
+    #[kani::proof_for_contract(<*const ()>::byte_offset_from)]
+    pub fn check_const_byte_offset_from_unit() {
+        let val: () = ();
+        let src_ptr: *const () = &val;
+        let dest_ptr: *const () = &val;
+        unsafe {
+            dest_ptr.byte_offset_from(src_ptr);
+        }
+    }
+
+    // generate proofs for contracts for byte_offset_from to verify int and composite
+    // types
+    // - `$type`: pointee type
+    // - `$proof_name1`: name of the harness for single element
+    // - `$proof_name2`: name of the harness for array of elements
+    macro_rules! generate_const_byte_offset_from_harness {
+        ($type: ty, $proof_name1: ident, $proof_name2: ident) => {
+            // Proof for a single element
+            #[kani::proof_for_contract(<*const $type>::byte_offset_from)]
+            pub fn $proof_name1() {
+                const gen_size: usize = mem::size_of::<$type>();
+                let mut generator1 = PointerGenerator::<gen_size>::new();
+                let mut generator2 = PointerGenerator::<gen_size>::new();
+                let ptr1: *const $type = generator1.any_in_bounds().ptr;
+                let ptr2: *const $type = if kani::any() {
+                    generator1.any_alloc_status().ptr
+                } else {
+                    generator2.any_alloc_status().ptr
+                };
+
+                unsafe {
+                    ptr1.byte_offset_from(ptr2);
+                }
+            }
+
+            // Proof for large arrays
+            #[kani::proof_for_contract(<*const $type>::byte_offset_from)]
+            pub fn $proof_name2() {
+                const gen_size: usize = mem::size_of::<$type>();
+                let mut generator1 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new();
+                let mut generator2 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new();
+                let ptr1: *const $type = generator1.any_in_bounds().ptr;
+                let ptr2: *const $type = if kani::any() {
+                    generator1.any_alloc_status().ptr
+                } else {
+                    generator2.any_alloc_status().ptr
+                };
+
+                unsafe {
+                    ptr1.byte_offset_from(ptr2);
+                }
+            }
+        };
+    }
+
+    generate_const_byte_offset_from_harness!(
+        u8,
+        check_const_byte_offset_from_u8,
+        check_const_byte_offset_from_u8_arr
+    );
+    generate_const_byte_offset_from_harness!(
+        u16,
+        check_const_byte_offset_from_u16,
+        check_const_byte_offset_from_u16_arr
+    );
+    generate_const_byte_offset_from_harness!(
+        u32,
+        check_const_byte_offset_from_u32,
+        check_const_byte_offset_from_u32_arr
+    );
+    generate_const_byte_offset_from_harness!(
+        u64,
+        check_const_byte_offset_from_u64,
+        check_const_byte_offset_from_u64_arr
+    );
+    generate_const_byte_offset_from_harness!(
+        u128,
+        check_const_byte_offset_from_u128,
+        check_const_byte_offset_from_u128_arr
+    );
+    generate_const_byte_offset_from_harness!(
+        usize,
+        check_const_byte_offset_from_usize,
+        check_const_byte_offset_from_usize_arr
+    );
+
+    generate_const_byte_offset_from_harness!(
+        i8,
+        check_const_byte_offset_from_i8,
+        check_const_byte_offset_from_i8_arr
+    );
+    generate_const_byte_offset_from_harness!(
+        i16,
+        check_const_byte_offset_from_i16,
+        check_const_byte_offset_from_i16_arr
+    );
+    generate_const_byte_offset_from_harness!(
+        i32,
+        check_const_byte_offset_from_i32,
+        check_const_byte_offset_from_i32_arr
+    );
+    generate_const_byte_offset_from_harness!(
+        i64,
+        check_const_byte_offset_from_i64,
+        check_const_byte_offset_from_i64_arr
+    );
+    generate_const_byte_offset_from_harness!(
+        i128,
+        check_const_byte_offset_from_i128,
+        check_const_byte_offset_from_i128_arr
+    );
+    generate_const_byte_offset_from_harness!(
+        isize,
+        check_const_byte_offset_from_isize,
+        check_const_byte_offset_from_isize_arr
+    );
+
+    generate_const_byte_offset_from_harness!(
+        (i8, i8),
+        check_const_byte_offset_from_tuple_1,
+        check_const_byte_offset_from_tuple_1_arr
+    );
+    generate_const_byte_offset_from_harness!(
+        (f64, bool),
+        check_const_byte_offset_from_tuple_2,
+        check_const_byte_offset_from_tuple_2_arr
+    );
+    generate_const_byte_offset_from_harness!(
+        (u32, i16, f32),
+        check_const_byte_offset_from_tuple_3,
+        check_const_byte_offset_from_tuple_3_arr
+    );
+    generate_const_byte_offset_from_harness!(
+        ((), bool, u8, u16, i32, f64, i128, usize),
+        check_const_byte_offset_from_tuple_4,
+        check_const_byte_offset_from_tuple_4_arr
+    );
+
+    // length of the slice generated from PointerGenerator
+    const SLICE_LEN: usize = 10;
+
+    // generate proofs for contracts for byte_offset_from to verify slices
+    // - `$type`: type of the underlyign element within the slice pointer
+    // - `$proof_name`: name of the harness
+    macro_rules! generate_const_byte_offset_from_slice_harness {
+        ($type: ty, $proof_name: ident) => {
+            #[kani::proof_for_contract(<*const [$type]>::byte_offset_from)]
+            pub fn $proof_name() {
+                const gen_size: usize = mem::size_of::<$type>();
+                let mut generator1 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new();
+                let mut generator2 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new();
+                let ptr1: *const [$type] =
+                    generator1.any_in_bounds().ptr as *const [$type; SLICE_LEN];
+                let ptr2: *const [$type] = if kani::any() {
+                    generator1.any_alloc_status().ptr as *const [$type; SLICE_LEN]
+                } else {
+                    generator2.any_alloc_status().ptr as *const [$type; SLICE_LEN]
+                };
+
+                unsafe {
+                    ptr1.byte_offset_from(ptr2);
+                }
+            }
+        };
+    }
+
+    generate_const_byte_offset_from_slice_harness!(u8, check_const_byte_offset_from_u8_slice);
+    generate_const_byte_offset_from_slice_harness!(u16, check_const_byte_offset_from_u16_slice);
+    generate_const_byte_offset_from_slice_harness!(u32, check_const_byte_offset_from_u32_slice);
+    generate_const_byte_offset_from_slice_harness!(u64, check_const_byte_offset_from_u64_slice);
+    generate_const_byte_offset_from_slice_harness!(u128, check_const_byte_offset_from_u128_slice);
+    generate_const_byte_offset_from_slice_harness!(usize, check_const_byte_offset_from_usize_slice);
+    generate_const_byte_offset_from_slice_harness!(i8, check_const_byte_offset_from_i8_slice);
+    generate_const_byte_offset_from_slice_harness!(i16, check_const_byte_offset_from_i16_slice);
+    generate_const_byte_offset_from_slice_harness!(i32, check_const_byte_offset_from_i32_slice);
+    generate_const_byte_offset_from_slice_harness!(i64, check_const_byte_offset_from_i64_slice);
+    generate_const_byte_offset_from_slice_harness!(i128, check_const_byte_offset_from_i128_slice);
+    generate_const_byte_offset_from_slice_harness!(isize, check_const_byte_offset_from_isize_slice);
+
     #[kani::proof_for_contract(<*const ()>::byte_offset)]
     #[kani::should_panic]
     pub fn check_const_byte_offset_unit_invalid_count() {
diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs
index fd7e4d80e676d..ef291233ae336 100644
--- a/library/core/src/ptr/mut_ptr.rs
+++ b/library/core/src/ptr/mut_ptr.rs
@@ -894,6 +894,16 @@ impl<T: ?Sized> *mut 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(
+        (mem::size_of_val_raw(self) != 0) &&
+        // Ensures subtracting `origin` from `self` doesn't overflow
+        (self.addr() as isize).checked_sub(origin.addr() as isize).is_some() &&
+        // Ensure both pointers are in the same allocation or are pointing to the same address
+        (self.addr() == origin.addr() ||
+            core::ub_checks::same_allocation(self as *const u8, origin as *const u8))
+    )]
+    // The result should equal the distance in terms of bytes
+    #[ensures(|result| *result == (self.addr() as isize - origin.addr() as isize))]
     pub const unsafe fn byte_offset_from<U: ?Sized>(self, origin: *const U) -> isize {
         // SAFETY: the caller must uphold the safety contract for `offset_from`.
         unsafe { self.cast::<u8>().offset_from(origin.cast::<u8>()) }
@@ -2236,9 +2246,202 @@ mod verify {
 
     // The array's length is set to an arbitrary value, which defines its size.
     // In this case, implementing a dynamic array is not possible, because 
-    // PointerGenerator does not support dynamic sized arrays.
+    // PointerGenerator or any_array() do not support dynamic sized arrays.
     const ARRAY_LEN: usize = 40;
 
+    #[kani::proof]
+    pub fn check_mut_byte_offset_from_fixed_offset() {
+        let mut arr: [u32; ARRAY_LEN] = kani::Arbitrary::any_array();
+        let offset: usize = kani::any_where(|&x| x <= ARRAY_LEN);
+        let origin_ptr: *mut u32 = arr.as_mut_ptr();
+        let self_ptr: *mut u32 = unsafe { origin_ptr.byte_offset(offset as isize) };
+        let result: isize = unsafe { self_ptr.byte_offset_from(origin_ptr) };
+        assert_eq!(result, offset as isize);
+        assert_eq!(result, (self_ptr.addr() as isize - origin_ptr.addr() as isize));
+    }
+
+    // Proof for unit size
+    #[kani::proof_for_contract(<*mut ()>::byte_offset_from)]
+    pub fn check_mut_byte_offset_from_unit() {
+        let mut val: () = ();
+        let src_ptr: *mut () = &mut val;
+        let dest_ptr: *mut () = &mut val;
+        unsafe {
+            dest_ptr.byte_offset_from(src_ptr);
+        }
+    }
+
+    // generate proofs for contracts for byte_offset_from to verify int and composite
+    // types
+    // - `$type`: pointee type
+    // - `$proof_name1`: name of the harness for single element
+    // - `$proof_name2`: name of the harness for array of elements
+    macro_rules! generate_mut_byte_offset_from_harness {
+        ($type: ty, $proof_name1: ident, $proof_name2: ident) => {
+            // Proof for a single element
+            #[kani::proof_for_contract(<*mut $type>::byte_offset_from)]
+            pub fn $proof_name1() {
+                const gen_size: usize = mem::size_of::<$type>();
+                let mut generator1 = PointerGenerator::<gen_size>::new();
+                let mut generator2 = PointerGenerator::<gen_size>::new();
+                let ptr1: *mut $type = generator1.any_in_bounds().ptr;
+                let ptr2: *mut $type = if kani::any() {
+                    generator1.any_alloc_status().ptr
+                } else {
+                    generator2.any_alloc_status().ptr
+                };
+
+                unsafe {
+                    ptr1.byte_offset_from(ptr2);
+                }
+            }
+
+            // Proof for large arrays
+            #[kani::proof_for_contract(<*mut $type>::byte_offset_from)]
+            pub fn $proof_name2() {
+                const gen_size: usize = mem::size_of::<$type>();
+                let mut generator1 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new();
+                let mut generator2 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new();
+                let ptr1: *mut $type = generator1.any_in_bounds().ptr;
+                let ptr2: *mut $type = if kani::any() {
+                    generator1.any_alloc_status().ptr
+                } else {
+                    generator2.any_alloc_status().ptr
+                };
+
+                unsafe {
+                    ptr1.byte_offset_from(ptr2);
+                }
+            }
+        };
+    }
+
+    generate_mut_byte_offset_from_harness!(
+        u8,
+        check_mut_byte_offset_from_u8,
+        check_mut_byte_offset_from_u8_arr
+    );
+    generate_mut_byte_offset_from_harness!(
+        u16,
+        check_mut_byte_offset_from_u16,
+        check_mut_byte_offset_from_u16_arr
+    );
+    generate_mut_byte_offset_from_harness!(
+        u32,
+        check_mut_byte_offset_from_u32,
+        check_mut_byte_offset_from_u32_arr
+    );
+    generate_mut_byte_offset_from_harness!(
+        u64,
+        check_mut_byte_offset_from_u64,
+        check_mut_byte_offset_from_u64_arr
+    );
+    generate_mut_byte_offset_from_harness!(
+        u128,
+        check_mut_byte_offset_from_u128,
+        check_mut_byte_offset_from_u128_arr
+    );
+    generate_mut_byte_offset_from_harness!(
+        usize,
+        check_mut_byte_offset_from_usize,
+        check_mut_byte_offset_from_usize_arr
+    );
+
+    generate_mut_byte_offset_from_harness!(
+        i8,
+        check_mut_byte_offset_from_i8,
+        check_mut_byte_offset_from_i8_arr
+    );
+    generate_mut_byte_offset_from_harness!(
+        i16,
+        check_mut_byte_offset_from_i16,
+        check_mut_byte_offset_from_i16_arr
+    );
+    generate_mut_byte_offset_from_harness!(
+        i32,
+        check_mut_byte_offset_from_i32,
+        check_mut_byte_offset_from_i32_arr
+    );
+    generate_mut_byte_offset_from_harness!(
+        i64,
+        check_mut_byte_offset_from_i64,
+        check_mut_byte_offset_from_i64_arr
+    );
+    generate_mut_byte_offset_from_harness!(
+        i128,
+        check_mut_byte_offset_from_i128,
+        check_mut_byte_offset_from_i128_arr
+    );
+    generate_mut_byte_offset_from_harness!(
+        isize,
+        check_mut_byte_offset_from_isize,
+        check_mut_byte_offset_from_isize_arr
+    );
+
+    generate_mut_byte_offset_from_harness!(
+        (i8, i8),
+        check_mut_byte_offset_from_tuple_1,
+        check_mut_byte_offset_from_tuple_1_arr
+    );
+    generate_mut_byte_offset_from_harness!(
+        (f64, bool),
+        check_mut_byte_offset_from_tuple_2,
+        check_mut_byte_offset_from_tuple_2_arr
+    );
+    generate_mut_byte_offset_from_harness!(
+        (u32, i16, f32),
+        check_mut_byte_offset_from_tuple_3,
+        check_mut_byte_offset_from_tuple_3_arr
+    );
+    generate_mut_byte_offset_from_harness!(
+        ((), bool, u8, u16, i32, f64, i128, usize),
+        check_mut_byte_offset_from_tuple_4,
+        check_mut_byte_offset_from_tuple_4_arr
+    );
+
+    // The length of a slice is set to an arbitrary value, which defines its size.
+    // In this case, implementing a slice with a dynamic size set using kani::any() 
+    // is not possible, because PointerGenerator does not support non-deterministic 
+    // slice pointers.
+    const SLICE_LEN: usize = 10;
+
+    // generate proofs for contracts for byte_offset_from to verify slices
+    // - `$type`: type of the underlyign element within the slice pointer
+    // - `$proof_name`: name of the harness
+    macro_rules! generate_mut_byte_offset_from_slice_harness {
+        ($type: ty, $proof_name: ident) => {
+            #[kani::proof_for_contract(<*mut [$type]>::byte_offset_from)]
+            pub fn $proof_name() {
+                const gen_size: usize = mem::size_of::<$type>();
+                let mut generator1 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new();
+                let mut generator2 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new();
+                let ptr1: *mut [$type] = generator1.any_in_bounds().ptr as *mut [$type; SLICE_LEN];
+                let ptr2: *mut [$type] = if kani::any() {
+                    generator1.any_alloc_status().ptr as *mut [$type; SLICE_LEN]
+                } else {
+                    generator2.any_alloc_status().ptr as *mut [$type; SLICE_LEN]
+                };
+
+                unsafe {
+                    ptr1.byte_offset_from(ptr2);
+                }
+            }
+        };
+    }
+
+    generate_mut_byte_offset_from_slice_harness!(u8, check_mut_byte_offset_from_u8_slice);
+    generate_mut_byte_offset_from_slice_harness!(u16, check_mut_byte_offset_from_u16_slice);
+    generate_mut_byte_offset_from_slice_harness!(u32, check_mut_byte_offset_from_u32_slice);
+    generate_mut_byte_offset_from_slice_harness!(u64, check_mut_byte_offset_from_u64_slice);
+    generate_mut_byte_offset_from_slice_harness!(u128, check_mut_byte_offset_from_u128_slice);
+    generate_mut_byte_offset_from_slice_harness!(usize, check_mut_byte_offset_from_usize_slice);
+    generate_mut_byte_offset_from_slice_harness!(i8, check_mut_byte_offset_from_i8_slice);
+    generate_mut_byte_offset_from_slice_harness!(i16, check_mut_byte_offset_from_i16_slice);
+    generate_mut_byte_offset_from_slice_harness!(i32, check_mut_byte_offset_from_i32_slice);
+    generate_mut_byte_offset_from_slice_harness!(i64, check_mut_byte_offset_from_i64_slice);
+    generate_mut_byte_offset_from_slice_harness!(i128, check_mut_byte_offset_from_i128_slice);
+    generate_mut_byte_offset_from_slice_harness!(isize, check_mut_byte_offset_from_isize_slice);
+
     #[kani::proof_for_contract(<*mut ()>::byte_offset)]
     #[kani::should_panic]
     pub fn check_mut_byte_offset_unit_invalid_count() {