diff --git a/library/core/src/slice/ascii.rs b/library/core/src/slice/ascii.rs
index 3d5702992f52f..9809b063c589e 100644
--- a/library/core/src/slice/ascii.rs
+++ b/library/core/src/slice/ascii.rs
@@ -68,6 +68,11 @@ impl [u8] {
         let mut a = self;
         let mut b = other;
 
+        #[cfg_attr(kani, kani::loop_invariant(
+            a.len() <= self.len() && b.len() <= other.len() &&
+            (a.len() == 0 || self.as_ptr().wrapping_add(self.len()-a.len()) == a.as_ptr()) &&
+            (b.len() == 0 || other.as_ptr().wrapping_add(other.len()-b.len()) == b.as_ptr())
+        ))]
         while let ([first_a, rest_a @ ..], [first_b, rest_b @ ..]) = (a, b) {
             if first_a.eq_ignore_ascii_case(&first_b) {
                 a = rest_a;
@@ -160,6 +165,10 @@ impl [u8] {
         let mut bytes = self;
         // Note: A pattern matching based approach (instead of indexing) allows
         // making the function const.
+        #[cfg_attr(kani, kani::loop_invariant(
+            bytes.len() <= self.len() &&
+            (bytes.len() == 0 || self.as_ptr().wrapping_add(self.len()-bytes.len()) == bytes.as_ptr())
+        ))]
         while let [first, rest @ ..] = bytes {
             if first.is_ascii_whitespace() {
                 bytes = rest;
@@ -189,6 +198,10 @@ impl [u8] {
         let mut bytes = self;
         // Note: A pattern matching based approach (instead of indexing) allows
         // making the function const.
+        #[cfg_attr(kani, kani::loop_invariant(
+            bytes.len() <= self.len() &&
+            (bytes.len() == 0 || self.as_ptr() == bytes.as_ptr())
+        ))]
         while let [rest @ .., last] = bytes {
             if last.is_ascii_whitespace() {
                 bytes = rest;
@@ -338,6 +351,12 @@ impl<'a> fmt::Debug for EscapeAscii<'a> {
 #[doc(hidden)]
 #[inline]
 pub const fn is_ascii_simple(mut bytes: &[u8]) -> bool {
+    #[cfg(kani)]
+    let on_entry_bytes = bytes;
+    #[cfg_attr(kani, kani::loop_invariant(
+            bytes.len() <= on_entry_bytes.len() &&
+            (bytes.len() == 0 || bytes.as_ptr() == on_entry_bytes.as_ptr())
+    ))]
     while let [rest @ .., last] = bytes {
         if !last.is_ascii() {
             break;
@@ -426,10 +445,10 @@ const fn is_ascii(s: &[u8]) -> bool {
             // Read subsequent words until the last aligned word, excluding the last
             // aligned word by itself to be done in tail check later, to ensure that
             // tail is always one `usize` at most to extra branch `byte_pos == len`.
-            #[safety::loop_invariant(byte_pos <= len
+            #[cfg_attr(kani, kani::loop_invariant(byte_pos <= len
                                     && byte_pos >= offset_to_aligned
                                     && word_ptr.addr() >= start.addr() + offset_to_aligned
-                                    && byte_pos == word_ptr.addr() - start.addr())]
+                                    && byte_pos == word_ptr.addr() - start.addr()))]
             while byte_pos < len - USIZE_SIZE {
                 // Sanity check that the read is in bounds
                 debug_assert!(byte_pos + USIZE_SIZE <= len);
@@ -477,7 +496,7 @@ const fn is_ascii(bytes: &[u8]) -> bool {
 
     let mut i = 0;
 
-    #[safety::loop_invariant(i <= bytes.len())]
+    #[cfg_attr(kani, kani::loop_invariant(i <= bytes.len()))]
     while i + CHUNK_SIZE <= bytes.len() {
         let chunk_end = i + CHUNK_SIZE;
 
@@ -486,7 +505,7 @@ const fn is_ascii(bytes: &[u8]) -> bool {
         // ASCII bytes are less than 128 (0x80), so their most significant
         // bit is unset.
         let mut count = 0;
-        #[safety::loop_invariant(i <= chunk_end && chunk_end - i <= CHUNK_SIZE && i - (chunk_end - CHUNK_SIZE) >= count as usize)]
+        #[cfg_attr(kani, kani::loop_invariant(i <= chunk_end && chunk_end - i <= CHUNK_SIZE && i - (chunk_end - CHUNK_SIZE) >= count as usize))]
         while i < chunk_end {
             count += bytes[i].is_ascii() as u8;
             i += 1;
@@ -500,7 +519,7 @@ const fn is_ascii(bytes: &[u8]) -> bool {
 
     // Process the remaining `bytes.len() % N` bytes.
     let mut is_ascii = true;
-    #[safety::loop_invariant(i <= bytes.len())]
+    #[cfg_attr(kani, kani::loop_invariant(i <= bytes.len()))]
     while i < bytes.len() {
         is_ascii &= bytes[i].is_ascii();
         i += 1;
@@ -536,4 +555,29 @@ pub mod verify {
             }
         }
     }
+
+    #[kani::proof]
+    pub fn check_trim_ascii_start() {
+        let a: [u8; 100] = kani::any();
+        let _ret = a.trim_ascii_start();
+    }
+
+    #[kani::proof]
+    pub fn check_eq_ignore_ascii_case() {
+        let a: [u8; 100] = kani::any();
+        let b: [u8; 100] = kani::any();
+        let _ret = a.eq_ignore_ascii_case(b.as_slice());
+    }
+
+    #[kani::proof]
+    fn check_is_ascii_simple() {
+        let mut bytes: [u8; 100] = kani::any();
+        let _ret = is_ascii_simple(bytes.as_slice());
+    }
+
+    #[kani::proof]
+    fn check_trim_ascii_end() {
+        let mut a: [u8; 100] = kani::any();
+        let _ret = a.trim_ascii_end();
+    }
 }