diff --git a/tests/expected/intrinsics/copy/copy-unreadable-src/expected b/tests/expected/intrinsics/copy/copy-unreadable-src/expected
new file mode 100644
index 000000000000..d050fc3af4e8
--- /dev/null
+++ b/tests/expected/intrinsics/copy/copy-unreadable-src/expected
@@ -0,0 +1,2 @@
+FAILURE\
+memmove source region readable
\ No newline at end of file
diff --git a/tests/expected/intrinsics/copy/copy-unreadable-src/main.rs b/tests/expected/intrinsics/copy/copy-unreadable-src/main.rs
new file mode 100644
index 000000000000..2b0e71cc16f3
--- /dev/null
+++ b/tests/expected/intrinsics/copy/copy-unreadable-src/main.rs
@@ -0,0 +1,16 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `copy` fails when `src` is not valid for reads.
+#[kani::proof]
+fn test_copy_invalid() {
+    let arr: [i32; 3] = [0, 1, 0];
+    let src: *const i32 = arr.as_ptr();
+
+    unsafe {
+        // Get an invalid pointer with a negative offset
+        let src_invalid = unsafe { src.sub(1) as *const i32 };
+        let dst = src.add(1) as *mut i32;
+        core::intrinsics::copy(src_invalid, dst, 1);
+    }
+}
diff --git a/tests/expected/intrinsics/copy/copy-unwritable-dst/expected b/tests/expected/intrinsics/copy/copy-unwritable-dst/expected
new file mode 100644
index 000000000000..5f190242aba6
--- /dev/null
+++ b/tests/expected/intrinsics/copy/copy-unwritable-dst/expected
@@ -0,0 +1,2 @@
+FAILURE\
+memmove destination region writeable
\ No newline at end of file
diff --git a/tests/expected/intrinsics/copy/copy-unwritable-dst/main.rs b/tests/expected/intrinsics/copy/copy-unwritable-dst/main.rs
new file mode 100644
index 000000000000..f68e9b2a807c
--- /dev/null
+++ b/tests/expected/intrinsics/copy/copy-unwritable-dst/main.rs
@@ -0,0 +1,15 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `copy` fails when `dst` is not valid for writes.
+#[kani::proof]
+fn test_copy_invalid() {
+    let arr: [i32; 3] = [0, 1, 0];
+    let src: *const i32 = arr.as_ptr();
+
+    unsafe {
+        // Get an invalid pointer with an out-of-bounds offset
+        let dst_invalid = src.add(3) as *mut i32;
+        core::intrinsics::copy(src, dst_invalid, 1);
+    }
+}