diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs
index 5d2a544238ef9..a4492a41bf109 100644
--- a/library/core/src/ptr/mut_ptr.rs
+++ b/library/core/src/ptr/mut_ptr.rs
@@ -2583,6 +2583,7 @@ mod verify {
             }
 
             // Below function is for large arrays
+            #[kani::proof_for_contract(<*mut $type>::offset_from)]
             pub fn $proof_name2() {
                 const gen_size: usize = mem::size_of::<$type>();
                 let mut generator1 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new();