diff --git a/library/core/src/clone.rs b/library/core/src/clone.rs
index bf8875098edfa..b363c85bb9921 100644
--- a/library/core/src/clone.rs
+++ b/library/core/src/clone.rs
@@ -36,6 +36,10 @@
 
 #![stable(feature = "rust1", since = "1.0.0")]
 
+use safety::requires;
+
+#[cfg(kani)]
+use crate::kani;
 use crate::marker::{Destruct, PointeeSized};
 
 mod uninit;
@@ -576,8 +580,24 @@ unsafe impl CloneToUninit for str {
 #[unstable(feature = "clone_to_uninit", issue = "126799")]
 unsafe impl CloneToUninit for crate::ffi::CStr {
     #[cfg_attr(debug_assertions, track_caller)]
+    // Safety contract: `dest` must be valid for writes of `size_of_val(self)`
+    // bytes (the whole string including its NUL terminator) and properly
+    // aligned. `can_write` checks non-null, single-allocation bounds, and
+    // alignment (trivial for u8), matching the pointer contracts in
+    // `core::ptr` (e.g. `NonNull::write_bytes`); it subsumes the previous
+    // `!dest.is_null()`. The body writes exactly `size_of_val(self)` bytes
+    // through `dest`, which the modifies clause captures. Verified by
+    // `check_clone_to_uninit_contract` in ffi/c_str.rs.
+    #[requires(crate::ub_checks::can_write(crate::ptr::slice_from_raw_parts_mut(
+        dest,
+        crate::mem::size_of_val(self)
+    )))]
+    #[cfg_attr(
+        kani,
+        kani::modifies(crate::ptr::slice_from_raw_parts_mut(dest, crate::mem::size_of_val(self)))
+    )]
     unsafe fn clone_to_uninit(&self, dest: *mut u8) {
-        // SAFETY: For now, CStr is just a #[repr(trasnsparent)] [c_char] with some invariants.
+        // SAFETY: For now, CStr is just a #[repr(transparent)] [c_char] with some invariants.
         // And we can cast [c_char] to [u8] on all supported platforms (see: to_bytes_with_nul).
         // The pointer metadata properly preserves the length (so NUL is also copied).
         // See: `cstr_metadata_is_length_with_nul` in tests.
diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs
index b471eb5b7ff5d..b4ffae79f7494 100644
--- a/library/core/src/ffi/c_str.rs
+++ b/library/core/src/ffi/c_str.rs
@@ -875,6 +875,7 @@ impl FusedIterator for Bytes<'_> {}
 #[unstable(feature = "kani", issue = "none")]
 mod verify {
     use super::*;
+    use crate::clone::CloneToUninit;
 
     // Helper function
     fn arbitrary_cstr(slice: &[u8]) -> &CStr {
@@ -1096,4 +1097,84 @@ mod verify {
         assert_eq!(expected_is_empty, c_str.is_empty());
         assert!(c_str.is_safe());
     }
+
+    // ops::Index<ops::RangeFrom<usize>> for CStr
+    #[kani::proof]
+    #[kani::unwind(33)]
+    fn check_index_from() {
+        const MAX_SIZE: usize = 32;
+        let string: [u8; MAX_SIZE] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&string);
+        let c_str = arbitrary_cstr(slice);
+
+        let bytes_with_nul = c_str.to_bytes_with_nul();
+        let idx: usize = kani::any();
+        kani::assume(idx < bytes_with_nul.len());
+
+        let indexed = &c_str[idx..];
+        assert!(indexed.is_safe());
+        // The indexed result should correspond to the tail of the original bytes
+        assert_eq!(indexed.to_bytes_with_nul(), &bytes_with_nul[idx..]);
+    }
+
+    // CloneToUninit for CStr
+    // MAX_SIZE is kept small to avoid CBMC timeout: the symbolic pointer
+    // arithmetic in clone_to_uninit is expensive; 8 bytes is sufficient to
+    // cover empty, single-char, and multi-char C strings.
+    #[kani::proof]
+    #[kani::unwind(9)]
+    fn check_clone_to_uninit() {
+        const MAX_SIZE: usize = 8;
+        let string: [u8; MAX_SIZE] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&string);
+        let c_str = arbitrary_cstr(slice);
+
+        let len = c_str.to_bytes_with_nul().len();
+
+        // Use an initialized buffer to avoid UB from reading uninitialized
+        // memory if clone_to_uninit were buggy and failed to write all bytes.
+        let mut buf = [0u8; MAX_SIZE];
+        let dest = buf.as_mut_ptr();
+
+        // Safety: dest is non-null (stack allocation), valid for len writes,
+        // properly aligned (u8 has alignment 1)
+        unsafe {
+            c_str.clone_to_uninit(dest);
+        }
+
+        // Verify the cloned bytes form a valid CStr
+        let cloned_slice = unsafe { core::slice::from_raw_parts(dest, len) };
+        let cloned_cstr = CStr::from_bytes_with_nul(cloned_slice);
+        assert!(cloned_cstr.is_ok());
+        let cloned = cloned_cstr.unwrap();
+        assert!(cloned.is_safe());
+
+        // Verify exact byte-for-byte match with source (including NUL terminator)
+        assert_eq!(cloned.to_bytes_with_nul(), c_str.to_bytes_with_nul());
+    }
+
+    // Contract harness for `CloneToUninit for CStr` (Challenge 13,
+    // criterion 4): checks that the impl's `#[requires]` (dest valid for
+    // writes of `size_of_val(self)` bytes) and modifies clause rule out UB
+    // in the real body, following the pattern of the other contract
+    // harnesses in this file (`check_from_bytes_with_nul_unchecked`,
+    // `check_from_ptr`). The destination buffer is deliberately
+    // uninitialized: the contract only claims validity for writes, so the
+    // harness must not rely on `dest`'s contents. The functional
+    // (byte-for-byte) check stays in `check_clone_to_uninit` above.
+    #[kani::proof_for_contract(CStr::clone_to_uninit)]
+    #[kani::unwind(17)]
+    fn check_clone_to_uninit_contract() {
+        const MAX_SIZE: usize = 16;
+        let string: [u8; MAX_SIZE] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&string);
+        let c_str = arbitrary_cstr(slice);
+
+        // Buffer of MAX_SIZE >= size_of_val(c_str) bytes, so the contract's
+        // `can_write` precondition is satisfiable for every generated length.
+        let mut dest = [crate::mem::MaybeUninit::<u8>::uninit(); MAX_SIZE];
+        unsafe {
+            crate::clone::CloneToUninit::clone_to_uninit(c_str, dest.as_mut_ptr().cast::<u8>())
+        };
+    }
 }