diff --git a/library/core/src/slice/sort/shared/smallsort.rs b/library/core/src/slice/sort/shared/smallsort.rs
index e555fce440872..61a8edeec4975 100644
--- a/library/core/src/slice/sort/shared/smallsort.rs
+++ b/library/core/src/slice/sort/shared/smallsort.rs
@@ -1,7 +1,13 @@
 //! This module contains a variety of sort implementations that are optimized for small lengths.
 
+use safety::{ensures, requires};
+
+#[cfg(kani)]
+use crate::kani;
 use crate::mem::{self, ManuallyDrop, MaybeUninit};
 use crate::slice::sort::shared::FreezeMarker;
+#[cfg(kani)]
+use crate::ub_checks;
 use crate::{hint, intrinsics, ptr, slice};
 
 // It's important to differentiate between SMALL_SORT_THRESHOLD performance for
@@ -196,12 +202,17 @@ const SMALL_SORT_NETWORK_SCRATCH_LEN: usize = SMALL_SORT_NETWORK_THRESHOLD;
 /// within this limit.
 const MAX_STACK_ARRAY_SIZE: usize = 4096;
 
+#[cfg_attr(kani, crate::kani::modifies(v))]
+#[ensures(|_| v.len() == old(v.len()))]
 fn small_sort_fallback<T, F: FnMut(&T, &T) -> bool>(v: &mut [T], is_less: &mut F) {
     if v.len() >= 2 {
         insertion_sort_shift_left(v, 1, is_less);
     }
 }
 
+#[requires(v.len() <= SMALL_SORT_GENERAL_THRESHOLD)]
+#[cfg_attr(kani, crate::kani::modifies(v))]
+#[ensures(|_| v.len() == old(v.len()))]
 fn small_sort_general<T: FreezeMarker, F: FnMut(&T, &T) -> bool>(v: &mut [T], is_less: &mut F) {
     let mut stack_array = MaybeUninit::<[T; SMALL_SORT_GENERAL_SCRATCH_LEN]>::uninit();
 
@@ -217,6 +228,9 @@ fn small_sort_general<T: FreezeMarker, F: FnMut(&T, &T) -> bool>(v: &mut [T], is
     small_sort_general_with_scratch(v, scratch, is_less);
 }
 
+#[requires(v.len() < 2 || scratch.len() >= v.len() + 16)]
+#[cfg_attr(kani, crate::kani::modifies(v))]
+#[ensures(|_| v.len() == old(v.len()))]
 fn small_sort_general_with_scratch<T: FreezeMarker, F: FnMut(&T, &T) -> bool>(
     v: &mut [T],
     scratch: &mut [MaybeUninit<T>],
@@ -308,6 +322,9 @@ impl<T> Drop for CopyOnDrop<T> {
     }
 }
 
+#[requires(v.len() <= SMALL_SORT_NETWORK_SCRATCH_LEN)]
+#[cfg_attr(kani, crate::kani::modifies(v))]
+#[ensures(|_| v.len() == old(v.len()))]
 fn small_sort_network<T, F>(v: &mut [T], is_less: &mut F)
 where
     T: FreezeMarker,
@@ -383,6 +400,14 @@ where
 /// types. `is_less` could be a huge function and we want to give the compiler an option to
 /// not inline this function. For the same reasons that this function is very perf critical
 /// it should be in the same module as the functions that use it.
+#[requires(a_pos != b_pos)]
+#[requires(ub_checks::can_dereference(v_base.wrapping_add(a_pos)))]
+#[requires(ub_checks::can_dereference(v_base.wrapping_add(b_pos)))]
+#[requires(ub_checks::can_write(v_base.wrapping_add(a_pos)))]
+#[requires(ub_checks::can_write(v_base.wrapping_add(b_pos)))]
+#[requires(ub_checks::same_allocation(v_base.wrapping_add(a_pos), v_base.wrapping_add(b_pos)))]
+#[cfg_attr(kani, crate::kani::modifies(v_base.wrapping_add(a_pos)))]
+#[cfg_attr(kani, crate::kani::modifies(v_base.wrapping_add(b_pos)))]
 unsafe fn swap_if_less<T, F>(v_base: *mut T, a_pos: usize, b_pos: usize, is_less: &mut F)
 where
     F: FnMut(&T, &T) -> bool,
@@ -539,6 +564,26 @@ where
 ///
 /// # Safety
 /// begin < tail and p must be valid and initialized for all begin <= p <= tail.
+#[requires(begin.addr() < tail.addr())]
+#[requires(
+    size_of::<T>() == 0
+        || (tail.addr() - begin.addr()).is_multiple_of(size_of::<T>())
+)]
+#[requires(ub_checks::can_dereference(ptr::slice_from_raw_parts(
+    begin,
+    if size_of::<T>() == 0 { 1 } else { (tail.addr() - begin.addr()) / size_of::<T>() + 1 }
+)))]
+#[requires(ub_checks::can_write(ptr::slice_from_raw_parts_mut(
+    begin,
+    if size_of::<T>() == 0 { 1 } else { (tail.addr() - begin.addr()) / size_of::<T>() + 1 }
+)))]
+#[cfg_attr(
+    kani,
+    crate::kani::modifies(ptr::slice_from_raw_parts_mut(
+        begin,
+        if size_of::<T>() == 0 { 1 } else { (tail.addr() - begin.addr()) / size_of::<T>() + 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 {
@@ -577,6 +622,9 @@ 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())]
+#[cfg_attr(kani, crate::kani::modifies(v))]
+#[ensures(|_| v.len() == old(v.len()))]
 pub fn insertion_sort_shift_left<T, F: FnMut(&T, &T) -> bool>(
     v: &mut [T],
     offset: usize,
@@ -609,6 +657,15 @@ pub fn insertion_sort_shift_left<T, F: FnMut(&T, &T) -> bool>(
 
 /// SAFETY: The caller MUST guarantee that `v_base` is valid for 4 reads and
 /// `dst` is valid for 4 writes. The result will be stored in `dst[0..4]`.
+#[requires(ub_checks::can_dereference(ptr::slice_from_raw_parts(v_base, 4)))]
+#[requires(ub_checks::can_write(ptr::slice_from_raw_parts_mut(dst, 4)))]
+#[cfg_attr(kani, crate::kani::modifies(ptr::slice_from_raw_parts_mut(dst, 4)))]
+#[ensures(|_| unsafe {
+    let is_less: &mut F = mem::transmute(&is_less);
+    !is_less(&*dst.add(1), &*dst)
+        && !is_less(&*dst.add(2), &*dst.add(1))
+        && !is_less(&*dst.add(3), &*dst.add(2))
+})]
 pub unsafe fn sort4_stable<T, F: FnMut(&T, &T) -> bool>(
     v_base: *const T,
     dst: *mut T,
@@ -861,7 +918,198 @@ fn panic_on_ord_violation() -> ! {
 }
 
 #[must_use]
+#[ensures(|result| *result == (size_of::<T>() <= 8))]
 pub(crate) const fn has_efficient_in_place_swap<T>() -> bool {
     // Heuristic that holds true on all tested 64-bit capable architectures.
     size_of::<T>() <= 8 // size_of::<u64>()
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    //! Challenge 8: memory-safety and sorting contracts for `smallsort`.
+    //!
+    //! Sorting is specified for `i8` / a `!Freeze` wrapper with the default
+    //! total order (tracking issue #56). Harnesses use `PROOF_LEN` so
+    //! sort9/sort13/len=32 do not run; those canceled Kani partitions 2 and 4.
+
+    use safety::{ensures, requires};
+
+    use super::*;
+    use crate::cell::Cell;
+    use crate::kani;
+
+    const PROOF_LEN: usize = 4;
+
+    fn is_sorted_slice<T: PartialOrd>(v: &[T]) -> bool {
+        let mut i = 0;
+        while i + 1 < v.len() {
+            if v[i] > v[i + 1] {
+                return false;
+            }
+            i += 1;
+        }
+        true
+    }
+
+    fn lt_i8(a: &i8, b: &i8) -> bool {
+        *a < *b
+    }
+
+    /// `Cell` makes this `!Freeze`, so the default (insertion) impl is selected.
+    struct NotFreeze {
+        key: i8,
+        _ni: Cell<u8>,
+    }
+
+    impl kani::Arbitrary for NotFreeze {
+        fn any() -> Self {
+            NotFreeze { key: kani::any(), _ni: Cell::new(0) }
+        }
+    }
+
+    fn lt_nf(a: &NotFreeze, b: &NotFreeze) -> bool {
+        a.key < b.key
+    }
+
+    fn nf_sorted(v: &[NotFreeze]) -> bool {
+        let mut i = 0;
+        while i + 1 < v.len() {
+            if v[i].key > v[i + 1].key {
+                return false;
+            }
+            i += 1;
+        }
+        true
+    }
+
+    #[kani::proof_for_contract(has_efficient_in_place_swap)]
+    fn check_has_efficient_in_place_swap_u8() {
+        assert!(has_efficient_in_place_swap::<u8>());
+    }
+
+    #[kani::proof_for_contract(has_efficient_in_place_swap)]
+    fn check_has_efficient_in_place_swap_u64() {
+        assert!(has_efficient_in_place_swap::<u64>());
+    }
+
+    #[kani::proof_for_contract(has_efficient_in_place_swap)]
+    fn check_has_efficient_in_place_swap_u128() {
+        assert!(!has_efficient_in_place_swap::<u128>());
+    }
+
+    #[kani::proof_for_contract(swap_if_less)]
+    fn check_swap_if_less() {
+        let mut arr: [i8; 4] = kani::any();
+        let a: usize = kani::any();
+        let b: usize = kani::any();
+        kani::assume(a < 4 && b < 4 && a != b);
+        unsafe {
+            swap_if_less(arr.as_mut_ptr(), a, b, &mut lt_i8);
+        }
+        kani::assert(arr[a] <= arr[b], "pair is ordered after swap_if_less");
+    }
+
+    #[kani::proof_for_contract(sort4_stable)]
+    fn check_sort4_stable() {
+        let src: [i8; 4] = kani::any();
+        let mut dst = [MaybeUninit::<i8>::uninit(); 4];
+        unsafe {
+            sort4_stable(src.as_ptr(), dst.as_mut_ptr() as *mut i8, &mut lt_i8);
+        }
+        let out = unsafe {
+            [dst[0].assume_init(), dst[1].assume_init(), dst[2].assume_init(), dst[3].assume_init()]
+        };
+        kani::assert(is_sorted_slice(&out), "sort4_stable output is sorted");
+    }
+
+    #[kani::proof_for_contract(insert_tail)]
+    #[kani::unwind(6)]
+    fn check_insert_tail() {
+        let mut arr: [i8; PROOF_LEN] = kani::any();
+        let tail_idx: usize = kani::any();
+        kani::assume(tail_idx > 0 && tail_idx < PROOF_LEN);
+        kani::assume(is_sorted_slice(&arr[..tail_idx]));
+        unsafe {
+            insert_tail(arr.as_mut_ptr(), arr.as_mut_ptr().add(tail_idx), &mut lt_i8);
+        }
+        kani::assert(is_sorted_slice(&arr[..=tail_idx]), "insert_tail keeps [begin, tail] sorted");
+    }
+
+    #[kani::proof_for_contract(insertion_sort_shift_left)]
+    #[kani::unwind(6)]
+    fn check_insertion_sort_shift_left() {
+        let mut arr: [i8; PROOF_LEN] = kani::any();
+        insertion_sort_shift_left(&mut arr, 1, &mut lt_i8);
+        kani::assert(is_sorted_slice(&arr), "insertion_sort_shift_left sorts");
+    }
+
+    /// Default `StableSmallSortTypeImpl::small_sort` (`!Freeze` → insertion).
+    #[requires(v.len() <= SMALL_SORT_FALLBACK_THRESHOLD)]
+    #[cfg_attr(kani, kani::modifies(v, scratch))]
+    #[ensures(|_| nf_sorted(v))]
+    fn stable_small_sort_default(v: &mut [NotFreeze], scratch: &mut [MaybeUninit<NotFreeze>]) {
+        <NotFreeze as StableSmallSortTypeImpl>::small_sort(v, scratch, &mut lt_nf);
+    }
+
+    /// Default `UnstableSmallSortTypeImpl::small_sort` (`!Freeze` → insertion).
+    #[requires(v.len() <= SMALL_SORT_FALLBACK_THRESHOLD)]
+    #[cfg_attr(kani, kani::modifies(v))]
+    #[ensures(|_| nf_sorted(v))]
+    fn unstable_small_sort_default(v: &mut [NotFreeze]) {
+        <NotFreeze as UnstableSmallSortTypeImpl>::small_sort(v, &mut lt_nf);
+    }
+
+    /// `UnstableSmallSortFreezeTypeImpl::small_sort` on `i8` (network, Copy+Freeze).
+    ///
+    /// The harness uses `PROOF_LEN` so `sort9`/`sort13`/merge are not entered.
+    #[requires(v.len() <= <i8 as UnstableSmallSortFreezeTypeImpl>::small_sort_threshold())]
+    #[cfg_attr(kani, kani::modifies(v))]
+    #[ensures(|_| is_sorted_slice(v))]
+    fn unstable_freeze_small_sort_i8(v: &mut [i8]) {
+        <i8 as UnstableSmallSortFreezeTypeImpl>::small_sort(v, &mut lt_i8);
+    }
+
+    /// Freeze `StableSmallSortTypeImpl::small_sort` on `i8` (general-with-scratch).
+    #[requires(v.len() <= SMALL_SORT_GENERAL_THRESHOLD)]
+    #[requires(v.len() < 2 || scratch.len() >= v.len() + 16)]
+    #[cfg_attr(kani, kani::modifies(v, scratch))]
+    #[ensures(|_| is_sorted_slice(v))]
+    fn stable_small_sort_i8(v: &mut [i8], scratch: &mut [MaybeUninit<i8>]) {
+        <i8 as StableSmallSortTypeImpl>::small_sort(v, scratch, &mut lt_i8);
+    }
+
+    #[kani::proof_for_contract(stable_small_sort_default)]
+    #[kani::unwind(6)]
+    fn check_stable_small_sort_default() {
+        let mut arr: [NotFreeze; PROOF_LEN] = kani::any();
+        let mut scratch = [MaybeUninit::<NotFreeze>::uninit(); 1];
+        stable_small_sort_default(&mut arr, &mut scratch);
+        kani::assert(nf_sorted(&arr), "stable default small_sort sorts");
+    }
+
+    #[kani::proof_for_contract(unstable_small_sort_default)]
+    #[kani::unwind(6)]
+    fn check_unstable_small_sort_default() {
+        let mut arr: [NotFreeze; PROOF_LEN] = kani::any();
+        unstable_small_sort_default(&mut arr);
+        kani::assert(nf_sorted(&arr), "unstable default small_sort sorts");
+    }
+
+    #[kani::proof_for_contract(unstable_freeze_small_sort_i8)]
+    #[kani::unwind(6)]
+    fn check_unstable_freeze_small_sort_i8() {
+        let mut arr: [i8; PROOF_LEN] = kani::any();
+        unstable_freeze_small_sort_i8(&mut arr);
+        kani::assert(is_sorted_slice(&arr), "unstable freeze small_sort sorts");
+    }
+
+    #[kani::proof_for_contract(stable_small_sort_i8)]
+    #[kani::unwind(6)]
+    fn check_stable_small_sort_i8() {
+        let mut arr: [i8; PROOF_LEN] = kani::any();
+        let mut scratch = [MaybeUninit::<i8>::uninit(); SMALL_SORT_GENERAL_SCRATCH_LEN];
+        stable_small_sort_i8(&mut arr, &mut scratch);
+        kani::assert(is_sorted_slice(&arr), "stable freeze small_sort sorts");
+    }
+}