diff --git a/library/alloc/src/string.rs b/library/alloc/src/string.rs
index ae30cabf5af5b..f02f244d8722a 100644
--- a/library/alloc/src/string.rs
+++ b/library/alloc/src/string.rs
@@ -3488,3 +3488,193 @@ impl From<char> for String {
         c.to_string()
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use core::kani;
+
+    use super::*;
+
+    /// Helper: create a symbolic ASCII string of arbitrary length up to N bytes.
+    /// All bytes are constrained to be valid ASCII (0..=127), ensuring valid UTF-8.
+    fn any_ascii_string<const N: usize>() -> String {
+        let mut bytes: [u8; N] = kani::any();
+        let len: usize = kani::any();
+        kani::assume(len <= N);
+        // Constrain all active bytes to ASCII range for valid UTF-8
+        for i in 0..N {
+            if i < len {
+                kani::assume(bytes[i] <= 127);
+            }
+        }
+        unsafe { String::from_utf8_unchecked(bytes[..len].to_vec()) }
+    }
+
+    // ---- from_utf16le ----
+
+    #[kani::proof]
+    #[kani::unwind(6)]
+    fn check_from_utf16le() {
+        let bytes: [u8; 8] = kani::any();
+        let len: usize = kani::any();
+        kani::assume(len <= 8);
+        let _ = String::from_utf16le(&bytes[..len]);
+    }
+
+    // ---- from_utf16le_lossy ----
+
+    #[kani::proof]
+    #[kani::unwind(6)]
+    fn check_from_utf16le_lossy() {
+        let bytes: [u8; 8] = kani::any();
+        let len: usize = kani::any();
+        kani::assume(len <= 8);
+        let _ = String::from_utf16le_lossy(&bytes[..len]);
+    }
+
+    // ---- from_utf16be ----
+
+    #[kani::proof]
+    #[kani::unwind(6)]
+    fn check_from_utf16be() {
+        let bytes: [u8; 8] = kani::any();
+        let len: usize = kani::any();
+        kani::assume(len <= 8);
+        let _ = String::from_utf16be(&bytes[..len]);
+    }
+
+    // ---- from_utf16be_lossy ----
+
+    #[kani::proof]
+    #[kani::unwind(6)]
+    fn check_from_utf16be_lossy() {
+        let bytes: [u8; 8] = kani::any();
+        let len: usize = kani::any();
+        kani::assume(len <= 8);
+        let _ = String::from_utf16be_lossy(&bytes[..len]);
+    }
+
+    // ---- pop ----
+
+    #[kani::proof]
+    #[kani::unwind(6)]
+    fn check_pop() {
+        let s = any_ascii_string::<4>();
+        let mut s = s;
+        let _ = s.pop();
+    }
+
+    // ---- remove ----
+
+    #[kani::proof]
+    #[kani::unwind(6)]
+    fn check_str_remove() {
+        let mut s = String::from("abcd");
+        let idx: usize = kani::any();
+        kani::assume(idx < s.len());
+        let _ = s.remove(idx);
+    }
+
+    // ---- remove_matches ----
+
+    #[kani::proof]
+    #[kani::unwind(6)]
+    fn check_remove_matches() {
+        let mut s = String::from("abca");
+        s.remove_matches('a');
+    }
+
+    // ---- retain ----
+
+    #[kani::proof]
+    #[kani::unwind(6)]
+    fn check_retain() {
+        let mut s = String::from("axbx");
+        s.retain(|c| c != 'x');
+    }
+
+    // ---- insert ----
+
+    #[kani::proof]
+    #[kani::unwind(6)]
+    fn check_insert() {
+        let mut s = any_ascii_string::<4>();
+        let len = s.len();
+        let idx: usize = kani::any();
+        kani::assume(idx <= len);
+        // Insert an ASCII char (valid UTF-8, 1-byte)
+        s.insert(idx, 'z');
+    }
+
+    // ---- insert_str ----
+
+    #[kani::proof]
+    #[kani::unwind(6)]
+    fn check_insert_str() {
+        let mut s = any_ascii_string::<4>();
+        let len = s.len();
+        let idx: usize = kani::any();
+        kani::assume(idx <= len);
+        s.insert_str(idx, "hi");
+    }
+
+    // ---- split_off ----
+
+    #[kani::proof]
+    #[kani::unwind(6)]
+    fn check_split_off() {
+        let mut s = any_ascii_string::<4>();
+        let len = s.len();
+        let at: usize = kani::any();
+        kani::assume(at <= len);
+        let _ = s.split_off(at);
+    }
+
+    // ---- drain ----
+
+    #[kani::proof]
+    #[kani::unwind(6)]
+    fn check_drain() {
+        let mut s = any_ascii_string::<4>();
+        let len = s.len();
+        let start: usize = kani::any();
+        let end: usize = kani::any();
+        kani::assume(start <= end);
+        kani::assume(end <= len);
+        // ASCII: every index is a char boundary
+        let _ = s.drain(start..end);
+    }
+
+    // ---- replace_range ----
+
+    #[kani::proof]
+    #[kani::unwind(6)]
+    fn check_replace_range() {
+        let mut s = any_ascii_string::<4>();
+        let len = s.len();
+        let start: usize = kani::any();
+        let end: usize = kani::any();
+        kani::assume(start <= end);
+        kani::assume(end <= len);
+        s.replace_range(start..end, "ok");
+    }
+
+    // ---- into_boxed_str ----
+
+    #[kani::proof]
+    #[kani::unwind(6)]
+    fn check_into_boxed_str() {
+        let s = any_ascii_string::<4>();
+        let _ = s.into_boxed_str();
+    }
+
+    // ---- leak ----
+
+    #[kani::proof]
+    #[kani::unwind(6)]
+    fn check_leak() {
+        let s = any_ascii_string::<4>();
+        let _ = s.leak();
+    }
+}