diff --git a/library/core/src/str/lossy.rs b/library/core/src/str/lossy.rs
index e7677c8317a9f..d6786eff487f3 100644
--- a/library/core/src/str/lossy.rs
+++ b/library/core/src/str/lossy.rs
@@ -4,6 +4,9 @@ use crate::fmt;
 use crate::fmt::{Formatter, Write};
 use crate::iter::FusedIterator;
 
+#[cfg(kani)]
+use crate::kani;
+
 impl [u8] {
     /// Creates an iterator over the contiguous valid UTF-8 ranges of this
     /// slice, and the non-UTF-8 fragments in between.
@@ -204,6 +207,12 @@ impl<'a> Iterator for Utf8Chunks<'a> {
 
         let mut i = 0;
         let mut valid_up_to = 0;
+        // TODO: remove `LEN` and use `self.source.len()` directly once
+        // fix the issue that Kani loop contracts doesn't support `self`.
+        // Tracked in https://github.com/model-checking/kani/issues/3700
+        #[cfg(kani)]
+        let LEN = self.source.len();
+        #[safety::loop_invariant(i <= LEN && valid_up_to == i)]
         while i < self.source.len() {
             // SAFETY: `i < self.source.len()` per previous line.
             // For some reason the following are both significantly slower:
@@ -296,3 +305,31 @@ impl fmt::Debug for Utf8Chunks<'_> {
         f.debug_struct("Utf8Chunks").field("source", &self.debug()).finish()
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+pub mod verify {
+    use super::*;
+
+    #[kani::proof]
+    pub fn check_next() {
+        if kani::any() {
+            // TODO: ARR_SIZE can be `std::usize::MAX` with cbmc argument
+            // `--arrays-uf-always`
+            const ARR_SIZE: usize = 1000;
+            let mut x: [u8; ARR_SIZE] = kani::any();
+            let mut xs = kani::slice::any_slice_of_array_mut(&mut x);
+            let mut chunks = xs.utf8_chunks();
+            unsafe {
+                chunks.next();
+            }
+        } else {
+            let ptr = kani::any_where::<usize, _>(|val| *val != 0) as *const u8;
+            kani::assume(ptr.is_aligned());
+            unsafe {
+                let mut chunks = crate::slice::from_raw_parts(ptr, 0).utf8_chunks();
+                chunks.next();
+            }
+        }
+    }
+}
diff --git a/library/core/src/str/pattern.rs b/library/core/src/str/pattern.rs
index 665c9fc67d01e..f0b767ae2d4e9 100644
--- a/library/core/src/str/pattern.rs
+++ b/library/core/src/str/pattern.rs
@@ -43,6 +43,12 @@ use crate::convert::TryInto as _;
 use crate::slice::memchr;
 use crate::{cmp, fmt};
 
+#[cfg(all(target_arch = "x86_64", any(kani, target_feature = "sse2")))]
+use safety::{loop_invariant, requires};
+
+#[cfg(kani)]
+use crate::kani;
+
 // Pattern
 
 /// A string pattern.
@@ -1905,8 +1911,9 @@ fn simd_contains(needle: &str, haystack: &str) -> Option<bool> {
 /// # Safety
 ///
 /// Both slices must have the same length.
-#[cfg(all(target_arch = "x86_64", target_feature = "sse2"))] // only called on x86
+#[cfg(all(target_arch = "x86_64", any(kani, target_feature = "sse2")))] // only called on x86
 #[inline]
+#[requires(x.len() == y.len())]
 unsafe fn small_slice_eq(x: &[u8], y: &[u8]) -> bool {
     debug_assert_eq!(x.len(), y.len());
     // This function is adapted from
@@ -1951,6 +1958,11 @@ unsafe fn small_slice_eq(x: &[u8], y: &[u8]) -> bool {
     unsafe {
         let (mut px, mut py) = (x.as_ptr(), y.as_ptr());
         let (pxend, pyend) = (px.add(x.len() - 4), py.add(y.len() - 4));
+        #[loop_invariant(crate::ub_checks::same_allocation(x.as_ptr(), px)
+        && crate::ub_checks::same_allocation(y.as_ptr(), py)
+        && px.addr() >= x.as_ptr().addr()
+        && py.addr() >= y.as_ptr().addr()
+        && px.addr() - x.as_ptr().addr() == py.addr() - y.as_ptr().addr())]
         while px < pxend {
             let vx = (px as *const u32).read_unaligned();
             let vy = (py as *const u32).read_unaligned();
@@ -1965,3 +1977,50 @@ unsafe fn small_slice_eq(x: &[u8], y: &[u8]) -> bool {
         vx == vy
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+pub mod verify {
+    use super::*;
+
+    #[cfg(all(kani, target_arch = "x86_64"))] // only called on x86
+    #[kani::proof]
+    #[kani::unwind(4)]
+    pub fn check_small_slice_eq() {
+        // TODO: ARR_SIZE can be `std::usize::MAX` with cbmc argument
+        // `--arrays-uf-always`
+        const ARR_SIZE: usize = 1000;
+        let x: [u8; ARR_SIZE] = kani::any();
+        let y: [u8; ARR_SIZE] = kani::any();
+        let xs = kani::slice::any_slice_of_array(&x);
+        let ys = kani::slice::any_slice_of_array(&y);
+        kani::assume(xs.len() == ys.len());
+        unsafe {
+            small_slice_eq(xs, ys);
+        }
+    }
+
+    /* This harness check `small_slice_eq` with dangling pointer to slice
+       with zero size. Kani finds safety issue of `small_slice_eq` in this
+       harness and hence the proof will fail.
+
+    #[cfg(all(kani, target_arch = "x86_64"))] // only called on x86
+    #[kani::proof]
+    #[kani::unwind(4)]
+    pub fn check_small_slice_eq_empty() {
+        let ptr_x = kani::any_where::<usize, _>(|val| *val != 0) as *const u8;
+        let ptr_y = kani::any_where::<usize, _>(|val| *val != 0) as *const u8;
+        kani::assume(ptr_x.is_aligned());
+        kani::assume(ptr_y.is_aligned());
+        assert_eq!(
+            unsafe {
+                small_slice_eq(
+                    crate::slice::from_raw_parts(ptr_x, 0),
+                    crate::slice::from_raw_parts(ptr_y, 0),
+                )
+            },
+            true
+        );
+    }
+    */
+}