diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index c71893608796f..7923faaddfa33 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -224,6 +224,8 @@ jobs:
             --include-pattern ptr::alignment::Alignment::mask \
             --include-pattern ptr::alignment::Alignment::new \
             --include-pattern ptr::alignment::Alignment::new_unchecked \
+            --include-pattern "ptr::const_ptr::<impl[[:space:]]\*const[[:space:]](.+)>::read$" \
+            --include-pattern "ptr::mut_ptr::<impl[[:space:]]\*mut[[:space:]](.+)>::write$" \
             --include-pattern time::Duration::from_micros \
             --include-pattern time::Duration::from_millis \
             --include-pattern time::Duration::from_nanos \
diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs
index 4207d48bdb70d..ff172b809e91a 100644
--- a/library/core/src/ptr/const_ptr.rs
+++ b/library/core/src/ptr/const_ptr.rs
@@ -1264,6 +1264,8 @@ impl<T: PointeeSized> *const T {
     #[rustc_const_stable(feature = "const_ptr_read", since = "1.71.0")]
     #[inline(always)]
     #[track_caller]
+    // Safety precondition from `ptr::read`: `self` must be valid for reads and properly aligned.
+    #[requires(core::ub_checks::can_dereference(self))]
     pub const unsafe fn read(self) -> T
     where
         T: Sized,
@@ -2771,4 +2773,18 @@ mod verify {
     //         ptr_caller.byte_offset_from(ptr_input);
     //     }
     // }
+
+    // An in-bounds pointer into the generator's buffer; the precondition (`can_dereference`)
+    // is assumed on it, which prunes the misaligned and uninitialized offsets.
+    #[kani::proof_for_contract(<*const i32>::read)]
+    pub fn check_const_read_i32() {
+        const BUF_SIZE: usize = 8;
+        let mut generator = kani::PointerGenerator::<BUF_SIZE>::new();
+        let test_ptr: *const i32 = generator.any_in_bounds().ptr;
+        unsafe {
+            let val = test_ptr.read();
+            // Read back the value and assert it's correct
+            assert_eq!(val, *test_ptr);
+        }
+    }
 }
diff --git a/library/core/src/ptr/mut_ptr.rs b/library/core/src/ptr/mut_ptr.rs
index 90a04a13dd78d..e1614e5797719 100644
--- a/library/core/src/ptr/mut_ptr.rs
+++ b/library/core/src/ptr/mut_ptr.rs
@@ -1522,6 +1522,9 @@ impl<T: PointeeSized> *mut T {
     #[rustc_const_stable(feature = "const_ptr_write", since = "1.83.0")]
     #[inline(always)]
     #[track_caller]
+    // Safety precondition from `ptr::write`: `self` must be valid for writes and properly aligned.
+    #[requires(core::ub_checks::can_write(self))]
+    #[cfg_attr(kani, kani::modifies(self))]
     pub const unsafe fn write(self, val: T)
     where
         T: Sized,
@@ -3155,4 +3158,19 @@ mod verify {
     //         ptr_caller.byte_offset_from(ptr_input);
     //     }
     // }
+
+    // An in-bounds pointer into the generator's buffer; the precondition (`can_write`)
+    // is assumed on it, which prunes the misaligned offsets.
+    #[kani::proof_for_contract(<*mut i32>::write)]
+    pub fn check_mut_write_i32() {
+        const BUF_SIZE: usize = 8;
+        let mut generator = kani::PointerGenerator::<BUF_SIZE>::new();
+        let test_ptr: *mut i32 = generator.any_in_bounds().ptr;
+        let val: i32 = kani::any();
+        unsafe {
+            test_ptr.write(val);
+            // Read back the value and assert it's correct
+            assert_eq!(*test_ptr, val);
+        }
+    }
 }