diff --git a/cprover_bindings/src/goto_program/expr.rs b/cprover_bindings/src/goto_program/expr.rs
index 09adbdb20df3..28f8afb4fae7 100644
--- a/cprover_bindings/src/goto_program/expr.rs
+++ b/cprover_bindings/src/goto_program/expr.rs
@@ -126,6 +126,10 @@ pub enum ExprValue {
     Nondet,
     /// `NULL`
     PointerConstant(u64),
+    ReadOk {
+        ptr: Expr,
+        size: Expr,
+    },
     // `op++` etc
     SelfOp {
         op: SelfOperator,
@@ -717,6 +721,14 @@ impl Expr {
         expr!(Nondet, typ)
     }
 
+    /// `read_ok(ptr, size)`
+    pub fn read_ok(ptr: Expr, size: Expr) -> Self {
+        assert_eq!(*ptr.typ(), Type::void_pointer());
+        assert_eq!(*size.typ(), Type::size_t());
+
+        expr!(ReadOk { ptr, size }, Type::bool())
+    }
+
     /// `e.g. NULL`
     pub fn pointer_constant(c: u64, typ: Type) -> Self {
         assert!(typ.is_pointer());
diff --git a/cprover_bindings/src/irep/to_irep.rs b/cprover_bindings/src/irep/to_irep.rs
index 5c17ecf87b5d..9ec8c49e80bf 100644
--- a/cprover_bindings/src/irep/to_irep.rs
+++ b/cprover_bindings/src/irep/to_irep.rs
@@ -293,6 +293,11 @@ impl ToIrep for ExprValue {
                     Irep::just_bitpattern_id(*i, mm.pointer_width, false)
                 )],
             },
+            ExprValue::ReadOk { ptr, size } => Irep {
+                id: IrepId::ROk,
+                sub: vec![ptr.to_irep(mm), size.to_irep(mm)],
+                named_sub: linear_map![],
+            },
             ExprValue::SelfOp { op, e } => side_effect_irep(op.to_irep_id(), vec![e.to_irep(mm)]),
             ExprValue::StatementExpression { statements: ops } => side_effect_irep(
                 IrepId::StatementExpression,
diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
index 0141c2886539..2fcbaa36fb44 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs
@@ -217,6 +217,41 @@ impl GotocHook for Panic {
     }
 }
 
+/// Encodes __CPROVER_r_ok
+struct IsReadOk;
+impl GotocHook for IsReadOk {
+    fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool {
+        matches_function(tcx, instance, "KaniIsReadOk")
+    }
+
+    fn handle(
+        &self,
+        gcx: &mut GotocCtx,
+        _instance: Instance,
+        mut fargs: Vec<Expr>,
+        assign_to: &Place,
+        target: Option<BasicBlockIdx>,
+        span: Span,
+    ) -> Stmt {
+        assert_eq!(fargs.len(), 2);
+        let size = fargs.pop().unwrap();
+        let ptr = fargs.pop().unwrap().cast_to(Type::void_pointer());
+        let target = target.unwrap();
+        let loc = gcx.codegen_caller_span_stable(span);
+        let ret_place =
+            unwrap_or_return_codegen_unimplemented_stmt!(gcx, gcx.codegen_place_stable(assign_to));
+        let ret_type = ret_place.goto_expr.typ().clone();
+
+        Stmt::block(
+            vec![
+                ret_place.goto_expr.assign(Expr::read_ok(ptr, size).cast_to(ret_type), loc),
+                Stmt::goto(bb_label(target), Location::none()),
+            ],
+            Location::none(),
+        )
+    }
+}
+
 struct RustAlloc;
 // Removing this hook causes regression failures.
 // https://github.com/model-checking/kani/issues/1170
@@ -373,6 +408,7 @@ pub fn fn_hooks() -> GotocHooks {
             Rc::new(Assert),
             Rc::new(Cover),
             Rc::new(Nondet),
+            Rc::new(IsReadOk),
             Rc::new(RustAlloc),
             Rc::new(MemCmp),
             Rc::new(UntrackedDeref),
diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs
index 060508666735..3820f3f2238e 100644
--- a/kani_metadata/src/unstable.rs
+++ b/kani_metadata/src/unstable.rs
@@ -82,6 +82,8 @@ pub enum UnstableFeature {
     LineCoverage,
     /// Enable function contracts [RFC 9](https://model-checking.github.io/kani/rfc/rfcs/0009-function-contracts.html)
     FunctionContracts,
+    /// Memory predicate APIs.
+    MemPredicates,
 }
 
 impl UnstableFeature {
diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs
index 087e23c7d47e..e3d27c4b1bfb 100644
--- a/library/kani/src/lib.rs
+++ b/library/kani/src/lib.rs
@@ -14,13 +14,16 @@
 #![feature(repr_simd)]
 // Features used for tests only.
 #![cfg_attr(test, feature(core_intrinsics, portable_simd))]
-// Required for rustc_diagnostic_item
+// Required for `rustc_diagnostic_item` and `core_intrinsics`
 #![allow(internal_features)]
+// Required for implementing memory predicates.
+#![feature(ptr_metadata)]
 
 pub mod arbitrary;
 #[cfg(feature = "concrete_playback")]
 mod concrete_playback;
 pub mod futures;
+pub mod mem;
 pub mod slice;
 pub mod tuple;
 pub mod vec;
@@ -33,6 +36,7 @@ mod models;
 pub use arbitrary::Arbitrary;
 #[cfg(feature = "concrete_playback")]
 pub use concrete_playback::concrete_playback_run;
+
 #[cfg(not(feature = "concrete_playback"))]
 /// NOP `concrete_playback` for type checking during verification mode.
 pub fn concrete_playback_run<F: Fn()>(_: Vec<Vec<u8>>, _: F) {
@@ -80,18 +84,12 @@ pub fn assume(cond: bool) {
 /// `implies!(premise => conclusion)` means that if the `premise` is true, so
 /// must be the `conclusion`.
 ///
-/// This simply expands to `!premise || conclusion` and is intended to be used
-/// in function contracts to make them more readable, as the concept of an
-/// implication is more natural to think about than its expansion.
-///
-/// For further convenience multiple comma separated premises are allowed, and
-/// are joined with `||` in the expansion. E.g. `implies!(a, b => c)` expands to
-/// `!a || !b || c` and says that `c` is true if both `a` and `b` are true (see
-/// also [Horn Clauses](https://en.wikipedia.org/wiki/Horn_clause)).
+/// This simply expands to `!premise || conclusion` and is intended to make checks more readable,
+/// as the concept of an implication is more natural to think about than its expansion.
 #[macro_export]
 macro_rules! implies {
-    ($($premise:expr),+ => $conclusion:expr) => {
-        $(!$premise)||+ || ($conclusion)
+    ($premise:expr => $conclusion:expr) => {
+        !($premise) || ($conclusion)
     };
 }
 
@@ -217,13 +215,7 @@ pub(crate) unsafe fn any_raw_internal<T, const SIZE_T: usize>() -> T {
 #[inline(never)]
 #[allow(dead_code)]
 fn any_raw_inner<T>() -> T {
-    // while we could use `unreachable!()` or `panic!()` as the body of this
-    // function, both cause Kani to produce a warning on any program that uses
-    // kani::any() (see https://github.com/model-checking/kani/issues/2010).
-    // This function is handled via a hook anyway, so we just need to put a body
-    // that rustc does not complain about. An infinite loop works out nicely.
-    #[allow(clippy::empty_loop)]
-    loop {}
+    kani_intrinsic()
 }
 
 /// Function used to generate panic with a static message as this is the only one currently
@@ -239,6 +231,20 @@ pub const fn panic(message: &'static str) -> ! {
     panic!("{}", message)
 }
 
+/// An empty body that can be used to define Kani intrinsic functions.
+///
+/// A Kani intrinsic is a function that is interpreted by Kani compiler.
+/// While we could use `unreachable!()` or `panic!()` as the body of a kani intrinsic
+/// function, both cause Kani to produce a warning since we don't support caller location.
+/// (see https://github.com/model-checking/kani/issues/2010).
+///
+/// This function is dead, since its caller is always  handled via a hook anyway,
+/// so we just need to put a body that rustc does not complain about.
+/// An infinite loop works out nicely.
+fn kani_intrinsic<T>() -> T {
+    #[allow(clippy::empty_loop)]
+    loop {}
+}
 /// A macro to check if a condition is satisfiable at a specific location in the
 /// code.
 ///
diff --git a/library/kani/src/mem.rs b/library/kani/src/mem.rs
new file mode 100644
index 000000000000..203eae2229c4
--- /dev/null
+++ b/library/kani/src/mem.rs
@@ -0,0 +1,282 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! This module contains functions useful for checking unsafe memory access.
+//!
+//! Given the following validity rules provided in the Rust documentation:
+//! <https://doc.rust-lang.org/std/ptr/index.html> (accessed Feb 6th, 2024)
+//!
+//! 1. A null pointer is never valid, not even for accesses of size zero.
+//! 2. For a pointer to be valid, it is necessary, but not always sufficient, that the pointer
+//!    be dereferenceable: the memory range of the given size starting at the pointer must all be
+//!    within the bounds of a single allocated object. Note that in Rust, every (stack-allocated)
+//!    variable is considered a separate allocated object.
+//!    Even for operations of size zero, the pointer must not be pointing to deallocated memory,
+//!    i.e., deallocation makes pointers invalid even for zero-sized operations.
+//! 3. However, casting any non-zero integer literal to a pointer is valid for zero-sized
+//!    accesses, even if some memory happens to exist at that address and gets deallocated.
+//!    This corresponds to writing your own allocator: allocating zero-sized objects is not very
+//!    hard. The canonical way to obtain a pointer that is valid for zero-sized accesses is
+//!    `NonNull::dangling`.
+//! 4. All accesses performed by functions in this module are non-atomic in the sense of atomic
+//!    operations used to synchronize between threads.
+//!    This means it is undefined behavior to perform two concurrent accesses to the same location
+//!    from different threads unless both accesses only read from memory.
+//!    Notice that this explicitly includes `read_volatile` and `write_volatile`:
+//!    Volatile accesses cannot be used for inter-thread synchronization.
+//! 5. The result of casting a reference to a pointer is valid for as long as the underlying
+//!    object is live and no reference (just raw pointers) is used to access the same memory.
+//!    That is, reference and pointer accesses cannot be interleaved.
+//!
+//! Kani is able to verify #1 and #2 today.
+//!
+//! For #3, we are overly cautious, and Kani will only consider zero-sized pointer access safe if
+//! the address matches `NonNull::<()>::dangling()`.
+//! The way Kani tracks provenance is not enough to check if the address was the result of a cast
+//! from a non-zero integer literal.
+
+use crate::kani_intrinsic;
+use crate::mem::private::Internal;
+use std::mem::{align_of, size_of};
+use std::ptr::{DynMetadata, NonNull, Pointee};
+
+/// Assert that the pointer is valid for access according to [crate::mem] conditions 1, 2 and 3.
+///
+/// Note that an unaligned pointer is still considered valid.
+///
+/// TODO: Kani should automatically add those checks when a de-reference happens.
+/// https://github.com/model-checking/kani/issues/2975
+///
+/// This function will either panic or return `true`. This is to make it easier to use it in
+/// contracts.
+#[crate::unstable(
+    feature = "mem-predicates",
+    issue = 2690,
+    reason = "experimental memory predicate API"
+)]
+pub fn assert_valid_ptr<T>(ptr: *const T) -> bool
+where
+    T: ?Sized,
+    <T as Pointee>::Metadata: PtrProperties<T>,
+{
+    crate::assert(!ptr.is_null(), "Expected valid pointer, but found `null`");
+
+    let (thin_ptr, metadata) = ptr.to_raw_parts();
+    can_read(&metadata, thin_ptr)
+}
+
+fn can_read<M, T>(metadata: &M, data_ptr: *const ()) -> bool
+where
+    M: PtrProperties<T>,
+    T: ?Sized,
+{
+    let marker = Internal;
+    let sz = metadata.pointee_size(marker);
+    if metadata.dangling(marker) as *const _ == data_ptr {
+        crate::assert(sz == 0, "Dangling pointer is only valid for zero-sized access")
+    } else {
+        crate::assert(
+            is_read_ok(data_ptr, sz),
+            "Expected valid pointer, but found dangling pointer",
+        );
+    }
+    true
+}
+
+mod private {
+    /// Define like this to restrict usage of PtrProperties functions outside Kani.
+    #[derive(Copy, Clone)]
+    pub struct Internal;
+}
+
+/// Trait that allow us to extract information from pointers without de-referencing them.
+#[doc(hidden)]
+pub trait PtrProperties<T: ?Sized> {
+    fn pointee_size(&self, _: Internal) -> usize;
+
+    fn min_alignment(&self, _: Internal) -> usize;
+
+    fn dangling(&self, _: Internal) -> *const ();
+}
+
+/// Get the information for sized types (they don't have metadata).
+impl<T> PtrProperties<T> for () {
+    fn pointee_size(&self, _: Internal) -> usize {
+        size_of::<T>()
+    }
+
+    fn min_alignment(&self, _: Internal) -> usize {
+        align_of::<T>()
+    }
+
+    fn dangling(&self, _: Internal) -> *const () {
+        NonNull::<T>::dangling().as_ptr() as *const _
+    }
+}
+
+/// Get the information from the str metadata.
+impl PtrProperties<str> for usize {
+    #[inline(always)]
+    fn pointee_size(&self, _: Internal) -> usize {
+        *self
+    }
+
+    /// String slices are a UTF-8 representation of characters that have the same layout as slices
+    /// of type [u8].
+    /// <https://doc.rust-lang.org/reference/type-layout.html#str-layout>
+    fn min_alignment(&self, _: Internal) -> usize {
+        align_of::<u8>()
+    }
+
+    fn dangling(&self, _: Internal) -> *const () {
+        NonNull::<u8>::dangling().as_ptr() as _
+    }
+}
+
+/// Get the information from the slice metadata.
+impl<T> PtrProperties<[T]> for usize {
+    fn pointee_size(&self, _: Internal) -> usize {
+        *self * size_of::<T>()
+    }
+
+    fn min_alignment(&self, _: Internal) -> usize {
+        align_of::<T>()
+    }
+
+    fn dangling(&self, _: Internal) -> *const () {
+        NonNull::<T>::dangling().as_ptr() as _
+    }
+}
+
+/// Get the information from the vtable.
+impl<T> PtrProperties<T> for DynMetadata<T>
+where
+    T: ?Sized,
+{
+    fn pointee_size(&self, _: Internal) -> usize {
+        self.size_of()
+    }
+
+    fn min_alignment(&self, _: Internal) -> usize {
+        self.align_of()
+    }
+
+    fn dangling(&self, _: Internal) -> *const () {
+        NonNull::<&T>::dangling().as_ptr() as _
+    }
+}
+
+/// Check if the pointer `_ptr` contains an allocated address of size equal or greater than `_size`.
+///
+/// This function should only be called to ensure a pointer is valid. The opposite isn't true.
+/// I.e.: This function always returns `true` if the pointer is valid.
+/// Otherwise, it returns non-det boolean.
+#[rustc_diagnostic_item = "KaniIsReadOk"]
+#[inline(never)]
+fn is_read_ok(_ptr: *const (), _size: usize) -> bool {
+    kani_intrinsic()
+}
+
+#[cfg(test)]
+mod tests {
+    use super::{assert_valid_ptr, PtrProperties};
+    use crate::mem::private::Internal;
+    use std::fmt::Debug;
+    use std::intrinsics::size_of;
+    use std::mem::{align_of, align_of_val, size_of_val};
+    use std::ptr;
+    use std::ptr::{NonNull, Pointee};
+
+    fn size_of_t<T>(ptr: *const T) -> usize
+    where
+        T: ?Sized,
+        <T as Pointee>::Metadata: PtrProperties<T>,
+    {
+        let (_, metadata) = ptr.to_raw_parts();
+        metadata.pointee_size(Internal)
+    }
+
+    fn align_of_t<T>(ptr: *const T) -> usize
+    where
+        T: ?Sized,
+        <T as Pointee>::Metadata: PtrProperties<T>,
+    {
+        let (_, metadata) = ptr.to_raw_parts();
+        metadata.min_alignment(Internal)
+    }
+
+    #[test]
+    fn test_size_of() {
+        assert_eq!(size_of_t("hi"), size_of_val("hi"));
+        assert_eq!(size_of_t(&0u8), size_of_val(&0u8));
+        assert_eq!(size_of_t(&0u8 as *const dyn std::fmt::Display), size_of_val(&0u8));
+        assert_eq!(size_of_t(&[0u8, 1u8] as &[u8]), size_of_val(&[0u8, 1u8]));
+        assert_eq!(size_of_t(&[] as &[u8]), size_of_val::<[u8; 0]>(&[]));
+        assert_eq!(
+            size_of_t(NonNull::<u32>::dangling().as_ptr() as *const dyn std::fmt::Display),
+            size_of::<u32>()
+        );
+    }
+
+    #[test]
+    fn test_alignment() {
+        assert_eq!(align_of_t("hi"), align_of_val("hi"));
+        assert_eq!(align_of_t(&0u8), align_of_val(&0u8));
+        assert_eq!(align_of_t(&0u32 as *const dyn std::fmt::Display), align_of_val(&0u32));
+        assert_eq!(align_of_t(&[0isize, 1isize] as &[isize]), align_of_val(&[0isize, 1isize]));
+        assert_eq!(align_of_t(&[] as &[u8]), align_of_val::<[u8; 0]>(&[]));
+        assert_eq!(
+            align_of_t(NonNull::<u32>::dangling().as_ptr() as *const dyn std::fmt::Display),
+            align_of::<u32>()
+        );
+    }
+
+    #[test]
+    pub fn test_empty_slice() {
+        let slice_ptr = Vec::<char>::new().as_slice() as *const [char];
+        assert_valid_ptr(slice_ptr);
+    }
+
+    #[test]
+    pub fn test_empty_str() {
+        let slice_ptr = String::new().as_str() as *const str;
+        assert_valid_ptr(slice_ptr);
+    }
+
+    #[test]
+    fn test_dangling_zst() {
+        test_dangling_of_t::<()>();
+        test_dangling_of_t::<[(); 10]>();
+    }
+
+    fn test_dangling_of_t<T>() {
+        let dangling: *const T = NonNull::<T>::dangling().as_ptr();
+        assert_valid_ptr(dangling);
+
+        let vec_ptr = Vec::<T>::new().as_ptr();
+        assert_valid_ptr(vec_ptr);
+    }
+
+    #[test]
+    #[should_panic(expected = "Dangling pointer is only valid for zero-sized access")]
+    fn test_dangling_char() {
+        test_dangling_of_t::<char>();
+    }
+
+    #[test]
+    #[should_panic(expected = "Dangling pointer is only valid for zero-sized access")]
+    fn test_dangling_slice() {
+        test_dangling_of_t::<&str>();
+    }
+
+    #[test]
+    #[should_panic(expected = "Expected valid pointer, but found `null`")]
+    fn test_null_fat_ptr() {
+        assert_valid_ptr(ptr::null::<char>() as *const dyn Debug);
+    }
+
+    #[test]
+    #[should_panic(expected = "Expected valid pointer, but found `null`")]
+    fn test_null_char() {
+        assert_valid_ptr(ptr::null::<char>());
+    }
+}
diff --git a/scripts/kani-regression.sh b/scripts/kani-regression.sh
index 20782abe5cbc..3b029c475d5f 100755
--- a/scripts/kani-regression.sh
+++ b/scripts/kani-regression.sh
@@ -41,7 +41,8 @@ cargo test -p cprover_bindings
 cargo test -p kani-compiler
 cargo test -p kani-driver
 cargo test -p kani_metadata
-cargo test -p kani --lib # skip doc tests.
+# skip doc tests and enable assertions to fail
+cargo test -p kani --lib --features concrete_playback
 # Test the actual macros, skipping doc tests and enabling extra traits for "syn"
 # so we can debug print AST
 RUSTFLAGS=--cfg=kani_sysroot cargo test -p kani_macros --features syn/extra-traits --lib
diff --git a/tests/expected/function-contract/valid_ptr.expected b/tests/expected/function-contract/valid_ptr.expected
new file mode 100644
index 000000000000..a9dc8dd5992d
--- /dev/null
+++ b/tests/expected/function-contract/valid_ptr.expected
@@ -0,0 +1,11 @@
+Checking harness pre_condition::harness_invalid_ptr...
+Failed Checks: Dangling pointer is only valid for zero-sized access
+
+Checking harness pre_condition::harness_stack_ptr...
+VERIFICATION:- SUCCESSFUL
+
+Checking harness pre_condition::harness_head_ptr...
+VERIFICATION:- SUCCESSFUL
+
+Verification failed for - pre_condition::harness_invalid_ptr
+Complete - 2 successfully verified harnesses, 1 failures, 3 total
diff --git a/tests/expected/function-contract/valid_ptr.rs b/tests/expected/function-contract/valid_ptr.rs
new file mode 100644
index 000000000000..da212c7fa63e
--- /dev/null
+++ b/tests/expected/function-contract/valid_ptr.rs
@@ -0,0 +1,61 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts -Zmem-predicates
+
+//! Test that it is sound to use `assert_valid_ptr` inside a contract pre-condition.
+//! We cannot validate post-condition yet. This can be done once we fix:
+//! <https://github.com/model-checking/kani/issues/2997>
+#![feature(pointer_is_aligned)]
+
+mod pre_condition {
+    /// This contract should succeed only if the input is a valid pointer.
+    #[kani::requires(kani::mem::assert_valid_ptr(ptr) && ptr.is_aligned())]
+    unsafe fn read_ptr(ptr: *const i32) -> i32 {
+        *ptr
+    }
+
+    #[kani::proof_for_contract(read_ptr)]
+    fn harness_head_ptr() {
+        let boxed = Box::new(10);
+        let raw_ptr = Box::into_raw(boxed);
+        assert_eq!(unsafe { read_ptr(raw_ptr) }, 10);
+        let _ = unsafe { Box::from_raw(raw_ptr) };
+    }
+
+    #[kani::proof_for_contract(read_ptr)]
+    fn harness_stack_ptr() {
+        let val = -20;
+        assert_eq!(unsafe { read_ptr(&val) }, -20);
+    }
+
+    #[kani::proof_for_contract(read_ptr)]
+    fn harness_invalid_ptr() {
+        let ptr = std::ptr::NonNull::<i32>::dangling().as_ptr();
+        assert_eq!(unsafe { read_ptr(ptr) }, -20);
+    }
+}
+
+/// TODO: Enable once we fix: <https://github.com/model-checking/kani/issues/2997>
+#[cfg(not_supported)]
+mod post_condition {
+
+    /// This contract should fail since we are creating a dangling pointer.
+    #[kani::ensures(kani::mem::assert_valid_ptr(result.0))]
+    unsafe fn new_invalid_ptr() -> PtrWrapper<char> {
+        let var = 'c';
+        PtrWrapper(&var as *const _)
+    }
+
+    #[kani::proof_for_contract(new_invalid_ptr)]
+    fn harness() {
+        let _ = unsafe { new_invalid_ptr() };
+    }
+
+    struct PtrWrapper<T>(*const T);
+
+    impl<T> kani::Arbitrary for PtrWrapper<T> {
+        fn any() -> Self {
+            unreachable!("Do not invoke stubbing")
+        }
+    }
+}
diff --git a/tests/kani/MemPredicates/fat_ptr_validity.rs b/tests/kani/MemPredicates/fat_ptr_validity.rs
new file mode 100644
index 000000000000..51d784f06566
--- /dev/null
+++ b/tests/kani/MemPredicates/fat_ptr_validity.rs
@@ -0,0 +1,69 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z mem-predicates
+//! Check that Kani's memory predicates work for fat pointers.
+
+extern crate kani;
+
+use kani::mem::assert_valid_ptr;
+
+mod valid_access {
+    use super::*;
+    #[kani::proof]
+    pub fn check_valid_dyn_ptr() {
+        let boxed: Box<dyn PartialEq<u8>> = Box::new(10u8);
+        let raw_ptr = Box::into_raw(boxed);
+        assert_valid_ptr(raw_ptr);
+        let boxed = unsafe { Box::from_raw(raw_ptr) };
+        assert_ne!(*boxed, 0);
+    }
+
+    #[kani::proof]
+    pub fn check_valid_slice_ptr() {
+        let array = ['a', 'b', 'c'];
+        let slice = &array as *const [char];
+        assert_valid_ptr(slice);
+        assert_eq!(unsafe { &*slice }[0], 'a');
+        assert_eq!(unsafe { &*slice }[2], 'c');
+    }
+
+    #[kani::proof]
+    pub fn check_valid_zst() {
+        let slice_ptr = Vec::<char>::new().as_slice() as *const [char];
+        assert_valid_ptr(slice_ptr);
+
+        let str_ptr = String::new().as_str() as *const str;
+        assert_valid_ptr(str_ptr);
+    }
+}
+
+mod invalid_access {
+    use super::*;
+    #[kani::proof]
+    #[kani::should_panic]
+    pub fn check_invalid_dyn_ptr() {
+        let raw_ptr: *const dyn PartialEq<u8> = unsafe { new_dead_ptr::<u8>(0) };
+        assert_valid_ptr(raw_ptr);
+    }
+
+    #[kani::proof]
+    #[kani::should_panic]
+    pub fn check_invalid_slice_ptr() {
+        let raw_ptr: *const [char] = unsafe { new_dead_ptr::<[char; 2]>(['a', 'b']) };
+        assert_valid_ptr(raw_ptr);
+    }
+
+    #[kani::proof]
+    #[kani::should_panic]
+    pub fn check_invalid_slice_len() {
+        let array = [10usize; 10];
+        let invalid: *const [usize; 11] = &array as *const [usize; 10] as *const [usize; 11];
+        let ptr: *const [usize] = invalid as *const _;
+        assert_valid_ptr(ptr);
+    }
+
+    unsafe fn new_dead_ptr<T>(val: T) -> *const T {
+        let local = val;
+        &local as *const _
+    }
+}
diff --git a/tests/kani/MemPredicates/thin_ptr_validity.rs b/tests/kani/MemPredicates/thin_ptr_validity.rs
new file mode 100644
index 000000000000..638b7e1d1fc8
--- /dev/null
+++ b/tests/kani/MemPredicates/thin_ptr_validity.rs
@@ -0,0 +1,60 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z mem-predicates
+//! Check that Kani's memory predicates work for thin pointers.
+
+extern crate kani;
+
+use kani::mem::assert_valid_ptr;
+use std::ptr::NonNull;
+
+mod valid_access {
+    use super::*;
+    #[kani::proof]
+    pub fn check_dangling_zst() {
+        let dangling = NonNull::<()>::dangling().as_ptr();
+        assert_valid_ptr(dangling);
+
+        let vec_ptr = Vec::<()>::new().as_ptr();
+        assert_valid_ptr(vec_ptr);
+
+        let dangling = NonNull::<[char; 0]>::dangling().as_ptr();
+        assert_valid_ptr(dangling);
+    }
+
+    #[kani::proof]
+    pub fn check_valid_array() {
+        let array = ['a', 'b', 'c'];
+        assert_valid_ptr(&array);
+    }
+}
+
+mod invalid_access {
+    use super::*;
+    #[kani::proof]
+    #[kani::should_panic]
+    pub fn check_invalid_ptr() {
+        let raw_ptr = unsafe { new_dead_ptr::<u8>(0) };
+        assert_valid_ptr(raw_ptr);
+    }
+
+    #[kani::proof]
+    #[kani::should_panic]
+    pub fn check_invalid_array() {
+        let raw_ptr = unsafe { new_dead_ptr::<[char; 2]>(['a', 'b']) };
+        assert_valid_ptr(raw_ptr);
+    }
+
+    #[kani::proof]
+    #[kani::should_panic]
+    pub fn check_invalid_zst() {
+        let raw_ptr: *const [char; 0] =
+            unsafe { new_dead_ptr::<[char; 2]>(['a', 'b']) } as *const _;
+        assert_valid_ptr(raw_ptr);
+    }
+
+    unsafe fn new_dead_ptr<T>(val: T) -> *const T {
+        let local = val;
+        &local as *const _
+    }
+}