diff --git a/library/core/src/clone.rs b/library/core/src/clone.rs
index 7f2a40f753fa6..29923926df734 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;
@@ -544,8 +548,11 @@ 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 non-null, valid for size_of_val(self) writes,
+    // and properly aligned (u8 alignment is always satisfied for non-null pointers).
+    #[requires(!dest.is_null())]
     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 715d0d8db4025..d3cdcdd7efd25 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,59 @@ 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());
+    }
 }