diff --git a/library/core/src/slice/sort/shared/smallsort.rs b/library/core/src/slice/sort/shared/smallsort.rs
index 09f898309bd65..2cad5826ecf25 100644
--- a/library/core/src/slice/sort/shared/smallsort.rs
+++ b/library/core/src/slice/sort/shared/smallsort.rs
@@ -3,6 +3,10 @@
 use crate::mem::{self, ManuallyDrop, MaybeUninit};
 use crate::slice::sort::shared::FreezeMarker;
 use crate::{intrinsics, ptr, slice};
+use safety::{ensures, requires};
+
+#[cfg(kani)]
+use crate::kani;
 
 // It's important to differentiate between SMALL_SORT_THRESHOLD performance for
 // small slices and small-sort performance sorting small sub-slices as part of
@@ -539,6 +543,16 @@ where
 ///
 /// # Safety
 /// begin < tail and p must be valid and initialized for all begin <= p <= tail.
+#[requires(begin.addr() < tail.addr() && {
+    let len = tail.addr() - begin.addr() - 1;
+    let is_less: &mut F = unsafe { mem::transmute(&is_less) };
+    (0..len).into_iter().all(|i| is_less(&*begin.add(i), &*begin.add(i + 1)))
+})]
+#[ensures(|_| {
+    let len = tail.addr() - begin.addr();
+    let is_less: &mut F = unsafe { mem::transmute(&is_less) };
+    (0..len).into_iter().all(|i| is_less(&*begin.add(i), &*begin.add(i + 1)))
+})]
 unsafe fn insert_tail<T, F: FnMut(&T, &T) -> bool>(begin: *mut T, tail: *mut T, is_less: &mut F) {
     // SAFETY: see individual comments.
     unsafe {
@@ -556,7 +570,13 @@ unsafe fn insert_tail<T, F: FnMut(&T, &T) -> bool>(begin: *mut T, tail: *mut T,
         let tmp = ManuallyDrop::new(tail.read());
         let mut gap_guard = CopyOnDrop { src: &*tmp, dst: tail, len: 1 };
 
-        loop {
+        #[safety::loop_invariant(
+            sift.addr() >= begin.addr() && sift.addr() < tail.addr()
+        )]
+        // FIXME: This was `loop` but kani's loop contract doesn't support `loop`.
+        // Once it is supported, replace `while true` with the original `loop`
+        #[allow(while_true)]
+        while true {
             // SAFETY: we move sift into the gap (which is valid), and point the
             // gap guard destination at sift, ensuring that if a panic occurs the
             // gap is once again filled.
@@ -577,6 +597,14 @@ unsafe fn insert_tail<T, F: FnMut(&T, &T) -> bool>(begin: *mut T, tail: *mut T,
 }
 
 /// Sort `v` assuming `v[..offset]` is already sorted.
+#[requires(offset != 0 && offset <= v.len() && {
+    let is_less: &mut F = unsafe { mem::transmute(&is_less) };
+    v[..offset].is_sorted_by(|a, b| is_less(a, b))
+})]
+#[ensures(|_| {
+    let is_less: &mut F = unsafe { mem::transmute(&is_less) };
+    v.is_sorted_by(|a, b| is_less(a, b))
+})]
 pub fn insertion_sort_shift_left<T, F: FnMut(&T, &T) -> bool>(
     v: &mut [T],
     offset: usize,
@@ -596,6 +624,9 @@ pub fn insertion_sort_shift_left<T, F: FnMut(&T, &T) -> bool>(
         let v_base = v.as_mut_ptr();
         let v_end = v_base.add(len);
         let mut tail = v_base.add(offset);
+        #[safety::loop_invariant(
+            tail.addr() > v_base.addr() && tail.addr() <= v_end.addr()
+        )]
         while tail != v_end {
             // SAFETY: v_base and tail are both valid pointers to elements, and
             // v_base < tail since we checked offset != 0.
@@ -870,3 +901,57 @@ pub(crate) const fn has_efficient_in_place_swap<T>() -> bool {
     // Heuristic that holds true on all tested 64-bit capable architectures.
     mem::size_of::<T>() <= 8 // mem::size_of::<u64>()
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+
+    const MAX_SLICE_LEN: usize = SMALL_SORT_GENERAL_THRESHOLD;
+
+    #[kani::proof]
+    pub fn check_swap_if_less() {
+        let mut array: [u8; MAX_SLICE_LEN] = kani::any();
+        let a_pos = kani::any_where(|x: &usize| *x < MAX_SLICE_LEN);
+        let b_pos = kani::any_where(|x: &usize| *x < MAX_SLICE_LEN);
+        let mut is_less = |x: &u8, y: &u8| x < y;
+        let expected = {
+            let mut array = array.clone();
+            let a: u8 = array[a_pos];
+            let b: u8 = array[b_pos];
+            if is_less(&b, &a) {
+                array[a_pos] = b;
+                array[b_pos] = a;
+            }
+            array
+        };
+        unsafe {
+            swap_if_less(array.as_mut_ptr(), a_pos, b_pos, &mut is_less);
+        }
+        kani::assert(array == expected, "Swapped slice is different from the expectation");
+    }
+
+    #[kani::proof_for_contract(insert_tail)]
+    #[kani::unwind(17)]
+    pub fn check_insert_tail() {
+        let mut array: [u8; 17] = kani::any();
+        let tail = kani::any_where(|x: &usize| *x < 17);
+        let mut is_less = |x: &u8, y: &u8| x < y;
+        unsafe {
+            let begin = array.as_mut_ptr();
+            let tail = begin.add(tail);
+            insert_tail(begin, tail, &mut is_less);
+        }
+    }
+
+    #[kani::proof_for_contract(insertion_sort_shift_left)]
+    #[kani::stub_verified(insert_tail)]
+    #[kani::unwind(17)]
+    pub fn check_insertion_sort_shift_left() {
+        let mut array: [u8; 17] = kani::any();
+        let slice_len = kani::any_where(|x: &usize| *x != 0 && *x <= 17);
+        let offset = kani::any();
+        let mut is_less = |x: &u8, y: &u8| x < y;
+        insertion_sort_shift_left(&mut array[..slice_len], offset, &mut is_less);
+    }
+}