diff --git a/tests/std-checks/core/Cargo.toml b/tests/std-checks/core/Cargo.toml
index f6e1645c3a39..a1496a0c81a7 100644
--- a/tests/std-checks/core/Cargo.toml
+++ b/tests/std-checks/core/Cargo.toml
@@ -7,7 +7,7 @@ edition = "2021"
 description = "This crate contains contracts and harnesses for core library"
 
 [package.metadata.kani]
-unstable = { function-contracts = true, mem-predicates = true, ptr-to-ref-cast-checks = true }
+unstable = { function-contracts = true, mem-predicates = true, ptr-to-ref-cast-checks = true, uninit-checks = true }
 
 [package.metadata.kani.flags]
 output-format = "terse"
diff --git a/tests/std-checks/core/src/slice.rs b/tests/std-checks/core/src/slice.rs
index 044f4bd38586..fe627f21a5ae 100644
--- a/tests/std-checks/core/src/slice.rs
+++ b/tests/std-checks/core/src/slice.rs
@@ -1,25 +1,30 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
+extern crate kani;
+
 /// Create wrapper functions to standard library functions that contains their contract.
 pub mod contracts {
     use kani::{mem::*, requires};
 
     #[requires(can_dereference(std::ptr::slice_from_raw_parts(data, len)))]
-    #[requires(is_initialized(data, len))]
     pub unsafe fn from_raw_parts<'a, T>(data: *const T, len: usize) -> &'a [T] {
         std::slice::from_raw_parts(data, len)
     }
+
+    #[requires(can_dereference(std::ptr::slice_from_raw_parts(data, len)))]
+    pub unsafe fn from_raw_parts_mut<'a, T>(data: *mut T, len: usize) -> &'a mut [T] {
+        std::slice::from_raw_parts_mut(data, len)
+    }
 }
 
 #[cfg(kani)]
 mod verify {
     use super::*;
 
-    const MAX_LEN: usize = 2;
+    const MAX_LEN: usize = isize::MAX as usize;
 
     #[kani::proof_for_contract(contracts::from_raw_parts)]
-    #[kani::unwind(25)]
     pub fn check_from_raw_parts_primitive() {
         let len: usize = kani::any();
         kani::assume(len < MAX_LEN);
@@ -27,4 +32,13 @@ mod verify {
         let arr = vec![0u8; len];
         let _slice = unsafe { contracts::from_raw_parts(arr.as_ptr(), len) };
     }
+
+    #[kani::proof_for_contract(contracts::from_raw_parts_mut)]
+    pub fn check_from_raw_parts_mut_primitive() {
+        let len: usize = kani::any();
+        kani::assume(len < MAX_LEN);
+
+        let mut arr = vec![0u8; len];
+        let _slice = unsafe { contracts::from_raw_parts_mut(arr.as_mut_ptr(), len) };
+    }
 }