diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs
index 1ab8a5ead993..d431625a350b 100644
--- a/library/kani_core/src/mem.rs
+++ b/library/kani_core/src/mem.rs
@@ -129,7 +129,10 @@ macro_rules! kani_mem {
 
         /// Compute the size of the val pointed to if it is safe to do so.
         ///
-        /// Return `None` if an overflow would occur, or if alignment is not power of two.
+        /// Returns `None` if:
+        /// - An overflow occurs during the size computation.
+        /// - The pointer’s alignment is not a power of two.
+        /// - The computed size exceeds `isize::MAX` (the maximum safe Rust allocation size).
         /// TODO: Optimize this if T is sized.
         #[kanitool::fn_marker = "CheckedSizeOfIntrinsic"]
         pub fn checked_size_of_raw<T: ?Sized>(ptr: *const T) -> Option<usize> {
@@ -166,6 +169,14 @@ macro_rules! kani_mem {
         /// Checks that `ptr` points to an allocation that can hold data of size calculated from `T`.
         ///
         /// This will panic if `ptr` points to an invalid `non_null`
+        /// Returns `false` if:
+        /// - The computed size overflows.
+        /// - The computed size exceeds `isize::MAX`.
+        /// - The pointer is null (except for zero-sized types).
+        /// - The pointer references unallocated memory.
+        ///
+        /// This function aligns with Rust's memory safety requirements, which restrict valid allocations
+        /// to sizes no larger than `isize::MAX`.
         fn is_inbounds<T: ?Sized>(ptr: *const T) -> bool {
             // If size overflows, then pointer cannot be inbounds.
             let Some(sz) = checked_size_of_raw(ptr) else { return false };
diff --git a/tests/expected/MemPredicates/ptr_size_validity.expected b/tests/expected/MemPredicates/ptr_size_validity.expected
new file mode 100644
index 000000000000..aa71ac4c4795
--- /dev/null
+++ b/tests/expected/MemPredicates/ptr_size_validity.expected
@@ -0,0 +1 @@
+Complete - 1 successfully verified harnesses, 0 failures, 1 total.
\ No newline at end of file
diff --git a/tests/expected/MemPredicates/ptr_size_validity.rs b/tests/expected/MemPredicates/ptr_size_validity.rs
new file mode 100644
index 000000000000..dabca4186b4f
--- /dev/null
+++ b/tests/expected/MemPredicates/ptr_size_validity.rs
@@ -0,0 +1,21 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z mem-predicates
+#![feature(ptr_metadata)]
+
+extern crate kani;
+
+mod size {
+    use super::*;
+
+    #[kani::proof]
+    fn verify_checked_size_of_raw_exceeds_isize_max() {
+        let len_exceeding_isize_max = (isize::MAX as usize) + 1;
+        let data_ptr: *const [u8] =
+            core::ptr::from_raw_parts(core::ptr::null::<u8>(), len_exceeding_isize_max);
+
+        let size = kani::mem::checked_size_of_raw(data_ptr);
+
+        assert!(size.is_none());
+    }
+}