diff --git a/library/core/src/slice/index.rs b/library/core/src/slice/index.rs
index d8ed521f44353..e13ddb24dd167 100644
--- a/library/core/src/slice/index.rs
+++ b/library/core/src/slice/index.rs
@@ -206,6 +206,18 @@ pub const unsafe trait SliceIndex<T: ?Sized>: private_slice_index::Sealed {
     #[unstable(feature = "slice_index_methods", issue = "none")]
     #[track_caller]
     fn index_mut(self, slice: &mut T) -> &mut Self::Output;
+
+    /// Borrowed form of the `get_unchecked` safety condition for Kani contracts.
+    ///
+    /// `true` iff `self` is a valid index into a `[T]` of length `len`.
+    /// Override in every `[T]` impl; the default is deliberately `false` so a
+    /// missing override cannot make `proof_for_contract` succeed vacuously.
+    #[cfg(kani)]
+    #[unstable(feature = "kani", issue = "none")]
+    fn in_bounds(&self, len: usize) -> bool {
+        let _ = len;
+        false
+    }
 }
 
 /// The methods `index` and `index_mut` panic if the index is out of bounds.
@@ -277,6 +289,11 @@ unsafe impl<T> const SliceIndex<[T]> for usize {
         // N.B., use intrinsic indexing
         &mut (*slice)[self]
     }
+
+    #[cfg(kani)]
+    fn in_bounds(&self, len: usize) -> bool {
+        *self < len
+    }
 }
 
 /// Because `IndexRange` guarantees `start <= end`, fewer checks are needed here
@@ -352,6 +369,11 @@ unsafe impl<T> const SliceIndex<[T]> for ops::IndexRange {
             slice_index_fail(self.start(), self.end(), slice.len())
         }
     }
+
+    #[cfg(kani)]
+    fn in_bounds(&self, len: usize) -> bool {
+        self.end() <= len
+    }
 }
 
 /// The methods `index` and `index_mut` panic if:
@@ -456,6 +478,11 @@ unsafe impl<T> const SliceIndex<[T]> for ops::Range<usize> {
             slice_index_fail(self.start, self.end, slice.len())
         }
     }
+
+    #[cfg(kani)]
+    fn in_bounds(&self, len: usize) -> bool {
+        self.start <= self.end && self.end <= len
+    }
 }
 
 #[unstable(feature = "new_range_api", issue = "125687")]
@@ -494,6 +521,11 @@ unsafe impl<T> const SliceIndex<[T]> for range::Range<usize> {
     fn index_mut(self, slice: &mut [T]) -> &mut [T] {
         ops::Range::from(self).index_mut(slice)
     }
+
+    #[cfg(kani)]
+    fn in_bounds(&self, len: usize) -> bool {
+        self.start <= self.end && self.end <= len
+    }
 }
 
 /// The methods `index` and `index_mut` panic if the end of the range is out of bounds.
@@ -533,6 +565,11 @@ unsafe impl<T> const SliceIndex<[T]> for ops::RangeTo<usize> {
     fn index_mut(self, slice: &mut [T]) -> &mut [T] {
         (0..self.end).index_mut(slice)
     }
+
+    #[cfg(kani)]
+    fn in_bounds(&self, len: usize) -> bool {
+        self.end <= len
+    }
 }
 
 /// The methods `index` and `index_mut` panic if the start of the range is out of bounds.
@@ -586,6 +623,11 @@ unsafe impl<T> const SliceIndex<[T]> for ops::RangeFrom<usize> {
             &mut *get_offset_len_mut_noubcheck(slice, self.start, new_len)
         }
     }
+
+    #[cfg(kani)]
+    fn in_bounds(&self, len: usize) -> bool {
+        self.start <= len
+    }
 }
 
 #[unstable(feature = "new_range_api", issue = "125687")]
@@ -624,6 +666,11 @@ unsafe impl<T> const SliceIndex<[T]> for range::RangeFrom<usize> {
     fn index_mut(self, slice: &mut [T]) -> &mut [T] {
         ops::RangeFrom::from(self).index_mut(slice)
     }
+
+    #[cfg(kani)]
+    fn in_bounds(&self, len: usize) -> bool {
+        self.start <= len
+    }
 }
 
 #[stable(feature = "slice_get_slice_impls", since = "1.15.0")]
@@ -660,6 +707,11 @@ unsafe impl<T> const SliceIndex<[T]> for ops::RangeFull {
     fn index_mut(self, slice: &mut [T]) -> &mut [T] {
         slice
     }
+
+    #[cfg(kani)]
+    fn in_bounds(&self, _len: usize) -> bool {
+        true
+    }
 }
 
 /// The methods `index` and `index_mut` panic if:
@@ -722,6 +774,17 @@ unsafe impl<T> const SliceIndex<[T]> for ops::RangeInclusive<usize> {
         }
         slice_index_fail(start, end, slice.len())
     }
+
+    #[cfg(kani)]
+    fn in_bounds(&self, len: usize) -> bool {
+        // `into_slice_range` does `end + 1`; that add is UB at `usize::MAX`.
+        if self.end == usize::MAX {
+            return false;
+        }
+        let exclusive_end = self.end + 1;
+        let start = if self.exhausted { exclusive_end } else { self.start };
+        start <= exclusive_end && exclusive_end <= len
+    }
 }
 
 #[unstable(feature = "new_range_api", issue = "125687")]
@@ -760,6 +823,15 @@ unsafe impl<T> const SliceIndex<[T]> for range::RangeInclusive<usize> {
     fn index_mut(self, slice: &mut [T]) -> &mut [T] {
         ops::RangeInclusive::from(self).index_mut(slice)
     }
+
+    #[cfg(kani)]
+    fn in_bounds(&self, len: usize) -> bool {
+        if self.last == usize::MAX {
+            return false;
+        }
+        let exclusive_end = self.last + 1;
+        self.start <= exclusive_end && exclusive_end <= len
+    }
 }
 
 /// The methods `index` and `index_mut` panic if the end of the range is out of bounds.
@@ -799,6 +871,11 @@ unsafe impl<T> const SliceIndex<[T]> for ops::RangeToInclusive<usize> {
     fn index_mut(self, slice: &mut [T]) -> &mut [T] {
         (0..=self.end).index_mut(slice)
     }
+
+    #[cfg(kani)]
+    fn in_bounds(&self, len: usize) -> bool {
+        self.end < len
+    }
 }
 
 /// The methods `index` and `index_mut` panic if the end of the range is out of bounds.
@@ -838,6 +915,11 @@ unsafe impl<T> const SliceIndex<[T]> for range::RangeToInclusive<usize> {
     fn index_mut(self, slice: &mut [T]) -> &mut [T] {
         (0..=self.last).index_mut(slice)
     }
+
+    #[cfg(kani)]
+    fn in_bounds(&self, len: usize) -> bool {
+        self.last < len
+    }
 }
 
 /// Performs bounds checking of a range.
@@ -1100,4 +1182,12 @@ unsafe impl<T> SliceIndex<[T]> for (ops::Bound<usize>, ops::Bound<usize>) {
     fn index_mut(self, slice: &mut [T]) -> &mut Self::Output {
         into_slice_range(slice.len(), self).index_mut(slice)
     }
+
+    #[cfg(kani)]
+    fn in_bounds(&self, len: usize) -> bool {
+        match into_range(len, *self) {
+            Some(r) => r.start <= r.end && r.end <= len,
+            None => false,
+        }
+    }
 }
diff --git a/library/core/src/slice/iter.rs b/library/core/src/slice/iter.rs
index b6de37033cc47..d56e50c092792 100644
--- a/library/core/src/slice/iter.rs
+++ b/library/core/src/slice/iter.rs
@@ -3121,7 +3121,11 @@ where
             let mut len = 1;
             let mut iter = self.slice.windows(2);
             while let Some([l, r]) = iter.next() {
-                if (self.predicate)(l, r) { len += 1 } else { break }
+                if (self.predicate)(l, r) {
+                    len += 1
+                } else {
+                    break;
+                }
             }
             let (head, tail) = self.slice.split_at(len);
             self.slice = tail;
@@ -3153,7 +3157,11 @@ where
             let mut len = 1;
             let mut iter = self.slice.windows(2);
             while let Some([l, r]) = iter.next_back() {
-                if (self.predicate)(l, r) { len += 1 } else { break }
+                if (self.predicate)(l, r) {
+                    len += 1
+                } else {
+                    break;
+                }
             }
             let (head, tail) = self.slice.split_at(self.slice.len() - len);
             self.slice = head;
@@ -3215,7 +3223,11 @@ where
             let mut len = 1;
             let mut iter = self.slice.windows(2);
             while let Some([l, r]) = iter.next() {
-                if (self.predicate)(l, r) { len += 1 } else { break }
+                if (self.predicate)(l, r) {
+                    len += 1
+                } else {
+                    break;
+                }
             }
             let slice = mem::take(&mut self.slice);
             let (head, tail) = slice.split_at_mut(len);
@@ -3248,7 +3260,11 @@ where
             let mut len = 1;
             let mut iter = self.slice.windows(2);
             while let Some([l, r]) = iter.next_back() {
-                if (self.predicate)(l, r) { len += 1 } else { break }
+                if (self.predicate)(l, r) {
+                    len += 1
+                } else {
+                    break;
+                }
             }
             let slice = mem::take(&mut self.slice);
             let (head, tail) = slice.split_at_mut(slice.len() - len);
diff --git a/library/core/src/slice/mod.rs b/library/core/src/slice/mod.rs
index 8e19bbdca0cd4..493f1919a580f 100644
--- a/library/core/src/slice/mod.rs
+++ b/library/core/src/slice/mod.rs
@@ -6,7 +6,7 @@
 
 #![stable(feature = "rust1", since = "1.0.0")]
 
-use safety::{ensures, requires};
+use safety::{ensures, loop_invariant, requires};
 
 use crate::clone::TrivialClone;
 use crate::cmp::Ordering::{self, Equal, Greater, Less};
@@ -388,7 +388,9 @@ impl<T> [T] {
     #[stable(feature = "slice_first_last_chunk", since = "1.77.0")]
     #[rustc_const_stable(feature = "slice_first_last_chunk", since = "1.77.0")]
     pub const fn split_first_chunk<const N: usize>(&self) -> Option<(&[T; N], &[T])> {
-        let Some((first, tail)) = self.split_at_checked(N) else { return None };
+        let Some((first, tail)) = self.split_at_checked(N) else {
+            return None;
+        };
 
         // SAFETY: We explicitly check for the correct number of elements,
         //   and do not let the references outlive the slice.
@@ -420,7 +422,9 @@ impl<T> [T] {
     pub const fn split_first_chunk_mut<const N: usize>(
         &mut self,
     ) -> Option<(&mut [T; N], &mut [T])> {
-        let Some((first, tail)) = self.split_at_mut_checked(N) else { return None };
+        let Some((first, tail)) = self.split_at_mut_checked(N) else {
+            return None;
+        };
 
         // SAFETY: We explicitly check for the correct number of elements,
         //   do not let the reference outlive the slice,
@@ -448,7 +452,9 @@ impl<T> [T] {
     #[stable(feature = "slice_first_last_chunk", since = "1.77.0")]
     #[rustc_const_stable(feature = "slice_first_last_chunk", since = "1.77.0")]
     pub const fn split_last_chunk<const N: usize>(&self) -> Option<(&[T], &[T; N])> {
-        let Some(index) = self.len().checked_sub(N) else { return None };
+        let Some(index) = self.len().checked_sub(N) else {
+            return None;
+        };
         let (init, last) = self.split_at(index);
 
         // SAFETY: We explicitly check for the correct number of elements,
@@ -481,7 +487,9 @@ impl<T> [T] {
     pub const fn split_last_chunk_mut<const N: usize>(
         &mut self,
     ) -> Option<(&mut [T], &mut [T; N])> {
-        let Some(index) = self.len().checked_sub(N) else { return None };
+        let Some(index) = self.len().checked_sub(N) else {
+            return None;
+        };
         let (init, last) = self.split_at_mut(index);
 
         // SAFETY: We explicitly check for the correct number of elements,
@@ -511,7 +519,9 @@ impl<T> [T] {
     #[rustc_const_stable(feature = "const_slice_last_chunk", since = "1.80.0")]
     pub const fn last_chunk<const N: usize>(&self) -> Option<&[T; N]> {
         // FIXME(const-hack): Without const traits, we need this instead of `get`.
-        let Some(index) = self.len().checked_sub(N) else { return None };
+        let Some(index) = self.len().checked_sub(N) else {
+            return None;
+        };
         let (_, last) = self.split_at(index);
 
         // SAFETY: We explicitly check for the correct number of elements,
@@ -541,7 +551,9 @@ impl<T> [T] {
     #[rustc_const_stable(feature = "const_slice_first_last_chunk", since = "1.83.0")]
     pub const fn last_chunk_mut<const N: usize>(&mut self) -> Option<&mut [T; N]> {
         // FIXME(const-hack): Without const traits, we need this instead of `get`.
-        let Some(index) = self.len().checked_sub(N) else { return None };
+        let Some(index) = self.len().checked_sub(N) else {
+            return None;
+        };
         let (_, last) = self.split_at_mut(index);
 
         // SAFETY: We explicitly check for the correct number of elements,
@@ -639,6 +651,7 @@ impl<T> [T] {
     #[must_use]
     #[track_caller]
     #[rustc_const_unstable(feature = "const_index", issue = "143775")]
+    #[requires(index.in_bounds(self.len()))]
     pub const unsafe fn get_unchecked<I>(&self, index: I) -> &I::Output
     where
         I: [const] SliceIndex<Self>,
@@ -684,6 +697,7 @@ impl<T> [T] {
     #[must_use]
     #[track_caller]
     #[rustc_const_unstable(feature = "const_index", issue = "143775")]
+    #[requires(index.in_bounds(self.len()))]
     pub const unsafe fn get_unchecked_mut<I>(&mut self, index: I) -> &mut I::Output
     where
         I: [const] SliceIndex<Self>,
@@ -948,6 +962,8 @@ impl<T> [T] {
     /// [undefined behavior]: https://doc.rust-lang.org/reference/behavior-considered-undefined.html
     #[unstable(feature = "slice_swap_unchecked", issue = "88539")]
     #[track_caller]
+    #[requires(a < self.len() && b < self.len())]
+    #[cfg_attr(kani, kani::modifies(self))]
     pub const unsafe fn swap_unchecked(&mut self, a: usize, b: usize) {
         assert_unsafe_precondition!(
             check_library_ub,
@@ -978,6 +994,7 @@ impl<T> [T] {
     #[stable(feature = "rust1", since = "1.0.0")]
     #[rustc_const_stable(feature = "const_slice_reverse", since = "1.90.0")]
     #[inline]
+    #[cfg_attr(kani, kani::modifies(self))]
     pub const fn reverse(&mut self) {
         let half_len = self.len() / 2;
         let Range { start, end } = self.as_mut_ptr_range();
@@ -1345,6 +1362,7 @@ impl<T> [T] {
     #[inline]
     #[must_use]
     #[track_caller]
+    #[requires(N != 0 && self.len().is_multiple_of(N))]
     pub const unsafe fn as_chunks_unchecked<const N: usize>(&self) -> &[[T; N]] {
         assert_unsafe_precondition!(
             check_language_ub,
@@ -1505,6 +1523,7 @@ impl<T> [T] {
     #[inline]
     #[must_use]
     #[track_caller]
+    #[requires(N != 0 && self.len().is_multiple_of(N))]
     pub const unsafe fn as_chunks_unchecked_mut<const N: usize>(&mut self) -> &mut [[T; N]] {
         assert_unsafe_precondition!(
             check_language_ub,
@@ -2043,6 +2062,13 @@ impl<T> [T] {
     #[inline]
     #[must_use]
     #[track_caller]
+    #[requires(mid <= self.len())]
+    #[ensures(|(left, right): &(&[T], &[T])| {
+        left.len() == mid
+            && right.len() == self.len() - mid
+            && left.as_ptr() == self.as_ptr()
+            && right.as_ptr() == self.as_ptr().wrapping_add(mid)
+    })]
     pub const unsafe fn split_at_unchecked(&self, mid: usize) -> (&[T], &[T]) {
         // FIXME(const-hack): the const function `from_raw_parts` is used to make this
         // function const; previously the implementation used
@@ -2097,6 +2123,13 @@ impl<T> [T] {
     #[inline]
     #[must_use]
     #[track_caller]
+    #[requires(mid <= self.len())]
+    #[ensures(|(left, right): &(&mut [T], &mut [T])| {
+        left.len() == mid
+            && right.len() == old(self.len()) - mid
+            && left.as_ptr() == old(self.as_ptr())
+            && right.as_ptr() == old(self.as_ptr()).wrapping_add(mid)
+    })]
     pub const unsafe fn split_at_mut_unchecked(&mut self, mid: usize) -> (&mut [T], &mut [T]) {
         let len = self.len();
         let ptr = self.as_mut_ptr();
@@ -2984,19 +3017,32 @@ impl<T> [T] {
             return Err(0);
         }
         let mut base = 0usize;
+        let mut half = 0usize;
+        let mut mid = 0usize;
+        let mut cmp = Equal;
 
         // This loop intentionally doesn't have an early exit if the comparison
         // returns Equal. We want the number of loop iterations to depend *only*
         // on the size of the input slice so that the CPU can reliably predict
         // the loop count.
+        // Overflow-safe form of `base + size <= self.len()` (Kani havocs before assume).
+        #[loop_invariant(
+            size >= 1
+                && size <= self.len()
+                && base.wrapping_add(size) >= base
+                && base.wrapping_add(size) <= self.len()
+                && base.wrapping_add(size / 2) >= base
+                && base.wrapping_add(size / 2) < self.len()
+        )]
+        #[cfg_attr(kani, kani::loop_modifies(&size, &base, &half, &mid, &cmp))]
         while size > 1 {
-            let half = size / 2;
-            let mid = base + half;
+            half = size / 2;
+            mid = base + half;
 
             // SAFETY: the call is made safe by the following invariants:
             // - `mid >= 0`: by definition
             // - `mid < size`: `mid = size / 2 + size / 4 + size / 8 ...`
-            let cmp = f(unsafe { self.get_unchecked(mid) });
+            cmp = f(unsafe { self.get_unchecked(mid) });
 
             // Binary search interacts poorly with branch prediction, so force
             // the compiler to use conditional moves if supported by the target
@@ -3577,6 +3623,9 @@ impl<T> [T] {
         let ptr = self.as_mut_ptr();
         let mut next_read: usize = 1;
         let mut next_write: usize = 1;
+        let mut ptr_read = ptr;
+        let mut prev_ptr_write = ptr;
+        let mut ptr_write = ptr;
 
         // SAFETY: the `while` condition guarantees `next_read` and `next_write`
         // are less than `len`, thus are inside `self`. `prev_ptr_write` points to
@@ -3595,12 +3644,29 @@ impl<T> [T] {
         // thus `next_read > next_write - 1` is too.
         unsafe {
             // Avoid bounds checks by using raw pointers.
+            #[loop_invariant(
+                next_read <= len
+                    && next_write >= 1
+                    && next_write <= next_read
+                    && next_read >= 1
+            )]
+            #[cfg_attr(
+                kani,
+                kani::loop_modifies(
+                    unsafe { slice::from_raw_parts_mut(ptr, len) },
+                    &next_read,
+                    &next_write,
+                    &ptr_read,
+                    &prev_ptr_write,
+                    &ptr_write
+                )
+            )]
             while next_read < len {
-                let ptr_read = ptr.add(next_read);
-                let prev_ptr_write = ptr.add(next_write - 1);
+                ptr_read = ptr.add(next_read);
+                prev_ptr_write = ptr.add(next_write - 1);
                 if !same_bucket(&mut *ptr_read, &mut *prev_ptr_write) {
                     if next_read != next_write {
-                        let ptr_write = prev_ptr_write.add(1);
+                        ptr_write = prev_ptr_write.add(1);
                         mem::swap(&mut *ptr_read, &mut *ptr_write);
                     }
                     next_write += 1;
@@ -3676,6 +3742,8 @@ impl<T> [T] {
     /// ```
     #[stable(feature = "slice_rotate", since = "1.26.0")]
     #[rustc_const_stable(feature = "const_slice_rotate", since = "1.92.0")]
+    #[requires(mid <= self.len())]
+    #[cfg_attr(kani, kani::modifies(self))]
     pub const fn rotate_left(&mut self, mid: usize) {
         assert!(mid <= self.len());
         let k = self.len() - mid;
@@ -3722,6 +3790,8 @@ impl<T> [T] {
     /// ```
     #[stable(feature = "slice_rotate", since = "1.26.0")]
     #[rustc_const_stable(feature = "const_slice_rotate", since = "1.92.0")]
+    #[requires(k <= self.len())]
+    #[cfg_attr(kani, kani::modifies(self))]
     pub const fn rotate_right(&mut self, k: usize) {
         assert!(k <= self.len());
         let mid = self.len() - k;
@@ -3898,6 +3968,8 @@ impl<T> [T] {
     #[stable(feature = "copy_from_slice", since = "1.9.0")]
     #[rustc_const_stable(feature = "const_copy_from_slice", since = "1.87.0")]
     #[track_caller]
+    #[requires(self.len() == src.len())]
+    #[cfg_attr(kani, kani::modifies(self))]
     pub const fn copy_from_slice(&mut self, src: &[T])
     where
         T: Copy,
@@ -4000,6 +4072,8 @@ impl<T> [T] {
     #[stable(feature = "swap_with_slice", since = "1.27.0")]
     #[rustc_const_unstable(feature = "const_swap_with_slice", issue = "142204")]
     #[track_caller]
+    #[requires(self.len() == other.len())]
+    #[cfg_attr(kani, kani::modifies(self, other))]
     pub const fn swap_with_slice(&mut self, other: &mut [T]) {
         assert!(self.len() == other.len(), "destination and source slices have different lengths");
         // SAFETY: `self` is valid for `self.len()` elements by definition, and `src` was
@@ -4658,7 +4732,9 @@ impl<T> [T] {
     #[rustc_const_unstable(feature = "const_split_off_first_last", issue = "138539")]
     pub const fn split_off_first<'a>(self: &mut &'a Self) -> Option<&'a T> {
         // FIXME(const-hack): Use `?` when available in const instead of `let-else`.
-        let Some((first, rem)) = self.split_first() else { return None };
+        let Some((first, rem)) = self.split_first() else {
+            return None;
+        };
         *self = rem;
         Some(first)
     }
@@ -4684,7 +4760,9 @@ impl<T> [T] {
     pub const fn split_off_first_mut<'a>(self: &mut &'a mut Self) -> Option<&'a mut T> {
         // FIXME(const-hack): Use `mem::take` and `?` when available in const.
         // Original: `mem::take(self).split_first_mut()?`
-        let Some((first, rem)) = mem::replace(self, &mut []).split_first_mut() else { return None };
+        let Some((first, rem)) = mem::replace(self, &mut []).split_first_mut() else {
+            return None;
+        };
         *self = rem;
         Some(first)
     }
@@ -4708,7 +4786,9 @@ impl<T> [T] {
     #[rustc_const_unstable(feature = "const_split_off_first_last", issue = "138539")]
     pub const fn split_off_last<'a>(self: &mut &'a Self) -> Option<&'a T> {
         // FIXME(const-hack): Use `?` when available in const instead of `let-else`.
-        let Some((last, rem)) = self.split_last() else { return None };
+        let Some((last, rem)) = self.split_last() else {
+            return None;
+        };
         *self = rem;
         Some(last)
     }
@@ -4734,7 +4814,9 @@ impl<T> [T] {
     pub const fn split_off_last_mut<'a>(self: &mut &'a mut Self) -> Option<&'a mut T> {
         // FIXME(const-hack): Use `mem::take` and `?` when available in const.
         // Original: `mem::take(self).split_last_mut()?`
-        let Some((last, rem)) = mem::replace(self, &mut []).split_last_mut() else { return None };
+        let Some((last, rem)) = mem::replace(self, &mut []).split_last_mut() else {
+            return None;
+        };
         *self = rem;
         Some(last)
     }
@@ -4788,6 +4870,7 @@ impl<T> [T] {
     #[stable(feature = "get_many_mut", since = "1.86.0")]
     #[inline]
     #[track_caller]
+    #[requires(get_disjoint_check_valid(&indices, self.len()).is_ok())]
     pub unsafe fn get_disjoint_unchecked_mut<I, const N: usize>(
         &mut self,
         indices: [I; N],
@@ -5470,6 +5553,8 @@ unsafe impl GetDisjointMutIndex for range::RangeInclusive<usize> {
 #[unstable(feature = "kani", issue = "none")]
 mod verify {
     use super::*;
+    use crate::ops::Bound;
+    use crate::range;
 
     //generates proof_of_contract harness for align_to given the T (src) and U (dst) types
     macro_rules! proof_of_contract_for_align_to {
@@ -5551,9 +5636,445 @@ mod verify {
     gen_align_to_mut_harnesses!(align_to_mut_from_char, char);
     gen_align_to_mut_harnesses!(align_to_mut_from_unit, ());
 
-    #[kani::proof]
+    // Challenge 17: remaining functions. Contracts are written over generic `[T]`;
+    // each harness instantiates a layout. Looping methods use loop contracts so
+    // the argument is inductive in the length, not an unwind bound.
+    const CAP: usize = 8;
+
+    fn any_ref<T, const N: usize>(arr: &[T; N]) -> &[T] {
+        kani::slice::any_slice_of_array(arr)
+    }
+
+    fn any_mut<T, const N: usize>(arr: &mut [T; N]) -> &mut [T] {
+        kani::slice::any_slice_of_array_mut(arr)
+    }
+
+    fn any_bound() -> Bound<usize> {
+        match kani::any::<u8>() % 3 {
+            0 => Bound::Included(kani::any()),
+            1 => Bound::Excluded(kani::any()),
+            _ => Bound::Unbounded,
+        }
+    }
+
+    // --- unsafe functions: proof_for_contract ---
+
+    #[kani::proof_for_contract(<[u8]>::get_unchecked)]
+    fn check_get_unchecked_usize() {
+        let arr: [u8; CAP] = kani::any();
+        let slice = any_ref(&arr);
+        let idx = kani::any::<usize>();
+        let _ = unsafe { slice.get_unchecked(idx) };
+    }
+
+    #[kani::proof_for_contract(<[u8]>::get_unchecked)]
+    fn check_get_unchecked_range() {
+        let arr: [u8; CAP] = kani::any();
+        let slice = any_ref(&arr);
+        let idx = kani::any::<usize>()..kani::any::<usize>();
+        let _ = unsafe { slice.get_unchecked(idx) };
+    }
+
+    #[kani::proof_for_contract(<[u8]>::get_unchecked)]
+    fn check_get_unchecked_range_inclusive() {
+        let arr: [u8; CAP] = kani::any();
+        let slice = any_ref(&arr);
+        let start = kani::any::<usize>();
+        let end = kani::any::<usize>();
+        let _ = unsafe { slice.get_unchecked(start..=end) };
+    }
+
+    #[kani::proof_for_contract(<[u8]>::get_unchecked)]
+    fn check_get_unchecked_range_from() {
+        let arr: [u8; CAP] = kani::any();
+        let slice = any_ref(&arr);
+        let idx = kani::any::<usize>()..;
+        let _ = unsafe { slice.get_unchecked(idx) };
+    }
+
+    #[kani::proof_for_contract(<[u8]>::get_unchecked)]
+    fn check_get_unchecked_range_to() {
+        let arr: [u8; CAP] = kani::any();
+        let slice = any_ref(&arr);
+        let idx = ..kani::any::<usize>();
+        let _ = unsafe { slice.get_unchecked(idx) };
+    }
+
+    #[kani::proof_for_contract(<[u8]>::get_unchecked)]
+    fn check_get_unchecked_range_full() {
+        let arr: [u8; CAP] = kani::any();
+        let slice = any_ref(&arr);
+        let _ = unsafe { slice.get_unchecked(..) };
+    }
+
+    #[kani::proof_for_contract(<[u8]>::get_unchecked)]
+    fn check_get_unchecked_range_to_inclusive() {
+        let arr: [u8; CAP] = kani::any();
+        let slice = any_ref(&arr);
+        let idx = ..=kani::any::<usize>();
+        let _ = unsafe { slice.get_unchecked(idx) };
+    }
+
+    #[kani::proof_for_contract(<[u8]>::get_unchecked)]
+    fn check_get_unchecked_index_range() {
+        let arr: [u8; CAP] = kani::any();
+        let slice = any_ref(&arr);
+        let start = kani::any::<usize>();
+        let end = kani::any::<usize>();
+        kani::assume(start <= end);
+        let idx = unsafe { crate::ops::IndexRange::new_unchecked(start, end) };
+        let _ = unsafe { slice.get_unchecked(idx) };
+    }
+
+    #[kani::proof_for_contract(<[u8]>::get_unchecked)]
+    fn check_get_unchecked_core_range() {
+        let arr: [u8; CAP] = kani::any();
+        let slice = any_ref(&arr);
+        let idx = range::Range { start: kani::any(), end: kani::any() };
+        let _ = unsafe { slice.get_unchecked(idx) };
+    }
+
+    #[kani::proof_for_contract(<[u8]>::get_unchecked)]
+    fn check_get_unchecked_core_range_inclusive() {
+        let arr: [u8; CAP] = kani::any();
+        let slice = any_ref(&arr);
+        let idx = range::RangeInclusive { start: kani::any(), last: kani::any() };
+        let _ = unsafe { slice.get_unchecked(idx) };
+    }
+
+    #[kani::proof_for_contract(<[u8]>::get_unchecked)]
+    fn check_get_unchecked_core_range_from() {
+        let arr: [u8; CAP] = kani::any();
+        let slice = any_ref(&arr);
+        let idx = range::RangeFrom { start: kani::any() };
+        let _ = unsafe { slice.get_unchecked(idx) };
+    }
+
+    #[kani::proof_for_contract(<[u8]>::get_unchecked)]
+    fn check_get_unchecked_core_range_to_inclusive() {
+        let arr: [u8; CAP] = kani::any();
+        let slice = any_ref(&arr);
+        let idx = range::RangeToInclusive { last: kani::any() };
+        let _ = unsafe { slice.get_unchecked(idx) };
+    }
+
+    #[kani::proof_for_contract(<[u8]>::get_unchecked)]
+    fn check_get_unchecked_bound_pair() {
+        let arr: [u8; CAP] = kani::any();
+        let slice = any_ref(&arr);
+        let idx = (any_bound(), any_bound());
+        let _ = unsafe { slice.get_unchecked(idx) };
+    }
+
+    #[kani::proof_for_contract(<[u8]>::get_unchecked_mut)]
+    fn check_get_unchecked_mut_usize() {
+        let mut arr: [u8; CAP] = kani::any();
+        let slice = any_mut(&mut arr);
+        let idx = kani::any::<usize>();
+        let _ = unsafe { slice.get_unchecked_mut(idx) };
+    }
+
+    #[kani::proof_for_contract(<[u8]>::get_unchecked_mut)]
+    fn check_get_unchecked_mut_range() {
+        let mut arr: [u8; CAP] = kani::any();
+        let slice = any_mut(&mut arr);
+        let idx = kani::any::<usize>()..kani::any::<usize>();
+        let _ = unsafe { slice.get_unchecked_mut(idx) };
+    }
+
+    #[kani::proof_for_contract(<[u8]>::get_unchecked_mut)]
+    fn check_get_unchecked_mut_range_inclusive() {
+        let mut arr: [u8; CAP] = kani::any();
+        let slice = any_mut(&mut arr);
+        let start = kani::any::<usize>();
+        let end = kani::any::<usize>();
+        let _ = unsafe { slice.get_unchecked_mut(start..=end) };
+    }
+
+    #[kani::proof_for_contract(<[u8]>::swap_unchecked)]
+    fn check_swap_unchecked() {
+        let mut arr: [u8; CAP] = kani::any();
+        let slice = any_mut(&mut arr);
+        let a = kani::any::<usize>();
+        let b = kani::any::<usize>();
+        unsafe { slice.swap_unchecked(a, b) };
+    }
+
+    #[kani::proof_for_contract(<[u8]>::as_chunks_unchecked)]
+    fn check_as_chunks_unchecked() {
+        let arr: [u8; CAP] = kani::any();
+        let slice = any_ref(&arr);
+        let _ = unsafe { slice.as_chunks_unchecked::<2>() };
+    }
+
+    #[kani::proof_for_contract(<[u8]>::as_chunks_unchecked_mut)]
+    fn check_as_chunks_unchecked_mut() {
+        let mut arr: [u8; CAP] = kani::any();
+        let slice = any_mut(&mut arr);
+        let _ = unsafe { slice.as_chunks_unchecked_mut::<2>() };
+    }
+
+    #[kani::proof_for_contract(<[u8]>::split_at_unchecked)]
+    fn check_split_at_unchecked() {
+        let arr: [u8; CAP] = kani::any();
+        let slice = any_ref(&arr);
+        let mid = kani::any::<usize>();
+        let _ = unsafe { slice.split_at_unchecked(mid) };
+    }
+
+    #[kani::proof_for_contract(<[()]>::split_at_unchecked)]
+    fn check_split_at_unchecked_zst() {
+        let arr: [(); CAP] = [(); CAP];
+        let slice = any_ref(&arr);
+        let mid = kani::any::<usize>();
+        let _ = unsafe { slice.split_at_unchecked(mid) };
+    }
+
+    #[kani::proof_for_contract(<[u8]>::split_at_mut_unchecked)]
+    fn check_split_at_mut_unchecked() {
+        let mut arr: [u8; CAP] = kani::any();
+        let slice = any_mut(&mut arr);
+        let mid = kani::any::<usize>();
+        let _ = unsafe { slice.split_at_mut_unchecked(mid) };
+    }
+
+    #[kani::proof_for_contract(<[u8]>::get_disjoint_unchecked_mut)]
+    fn check_get_disjoint_unchecked_mut_usize() {
+        let mut arr: [u8; CAP] = kani::any();
+        let slice = any_mut(&mut arr);
+        let indices = [kani::any::<usize>(), kani::any::<usize>()];
+        let _ = unsafe { slice.get_disjoint_unchecked_mut(indices) };
+    }
+
+    #[kani::proof_for_contract(<[u8]>::get_disjoint_unchecked_mut)]
+    fn check_get_disjoint_unchecked_mut_range() {
+        let mut arr: [u8; CAP] = kani::any();
+        let slice = any_mut(&mut arr);
+        let indices = [
+            kani::any::<usize>()..kani::any::<usize>(),
+            kani::any::<usize>()..kani::any::<usize>(),
+        ];
+        let _ = unsafe { slice.get_disjoint_unchecked_mut(indices) };
+    }
+
+    #[kani::proof_for_contract(<[u8]>::get_disjoint_unchecked_mut)]
+    fn check_get_disjoint_unchecked_mut_range_inclusive() {
+        let mut arr: [u8; CAP] = kani::any();
+        let slice = any_mut(&mut arr);
+        let a = kani::any::<usize>()..=kani::any::<usize>();
+        let b = kani::any::<usize>()..=kani::any::<usize>();
+        let _ = unsafe { slice.get_disjoint_unchecked_mut([a, b]) };
+    }
+
+    // --- safe abstractions ---
+
+    #[kani::proof_for_contract(<[u8]>::reverse)]
     fn check_reverse() {
-        let mut a: [u8; 100] = kani::any();
-        a.reverse();
+        let mut arr: [u8; CAP] = kani::any();
+        any_mut(&mut arr).reverse();
+    }
+
+    #[kani::proof]
+    fn check_first_chunk() {
+        let arr: [u8; CAP] = kani::any();
+        let slice = any_ref(&arr);
+        let _ = slice.first_chunk::<0>();
+        let _ = slice.first_chunk::<2>();
+        let _ = slice.first_chunk::<8>();
+    }
+
+    #[kani::proof]
+    fn check_first_chunk_mut() {
+        let mut arr: [u8; CAP] = kani::any();
+        let slice = any_mut(&mut arr);
+        let _ = slice.first_chunk_mut::<2>();
+    }
+
+    #[kani::proof]
+    fn check_split_first_chunk() {
+        let arr: [u8; CAP] = kani::any();
+        let _ = any_ref(&arr).split_first_chunk::<2>();
+    }
+
+    #[kani::proof]
+    fn check_split_first_chunk_mut() {
+        let mut arr: [u8; CAP] = kani::any();
+        let _ = any_mut(&mut arr).split_first_chunk_mut::<2>();
+    }
+
+    #[kani::proof]
+    fn check_split_last_chunk() {
+        let arr: [u8; CAP] = kani::any();
+        let _ = any_ref(&arr).split_last_chunk::<2>();
+    }
+
+    #[kani::proof]
+    fn check_split_last_chunk_mut() {
+        let mut arr: [u8; CAP] = kani::any();
+        let _ = any_mut(&mut arr).split_last_chunk_mut::<2>();
+    }
+
+    #[kani::proof]
+    fn check_last_chunk() {
+        let arr: [u8; CAP] = kani::any();
+        let slice = any_ref(&arr);
+        let _ = slice.last_chunk::<0>();
+        let _ = slice.last_chunk::<2>();
+    }
+
+    #[kani::proof]
+    fn check_last_chunk_mut() {
+        let mut arr: [u8; CAP] = kani::any();
+        let _ = any_mut(&mut arr).last_chunk_mut::<2>();
+    }
+
+    #[kani::proof]
+    fn check_as_chunks() {
+        let arr: [u8; CAP] = kani::any();
+        let _ = any_ref(&arr).as_chunks::<2>();
+    }
+
+    #[kani::proof]
+    fn check_as_chunks_mut() {
+        let mut arr: [u8; CAP] = kani::any();
+        let _ = any_mut(&mut arr).as_chunks_mut::<2>();
+    }
+
+    #[kani::proof]
+    fn check_as_rchunks() {
+        let arr: [u8; CAP] = kani::any();
+        let _ = any_ref(&arr).as_rchunks::<2>();
+    }
+
+    #[kani::proof]
+    fn check_split_at_checked() {
+        let arr: [u8; CAP] = kani::any();
+        let _ = any_ref(&arr).split_at_checked(kani::any());
+    }
+
+    #[kani::proof]
+    fn check_split_at_mut_checked() {
+        let mut arr: [u8; CAP] = kani::any();
+        let _ = any_mut(&mut arr).split_at_mut_checked(kani::any());
+    }
+
+    #[kani::proof]
+    fn check_binary_search_by() {
+        let arr: [u8; CAP] = kani::any();
+        let slice = any_ref(&arr);
+        let _ = slice.binary_search_by(|_| match kani::any::<u8>() % 3 {
+            0 => Equal,
+            1 => Less,
+            _ => Greater,
+        });
+    }
+
+    #[kani::proof]
+    fn check_partition_dedup_by() {
+        let mut arr: [u8; CAP] = kani::any();
+        let slice = any_mut(&mut arr);
+        let _ = slice.partition_dedup_by(|a, b| a == b);
+    }
+
+    // CAP=8 + symbolic mid times out autoharness's 10m CBMC cap on the
+    // memmove/gcd/swap rotate algorithms. Length 2 still calls the real
+    // `ptr_rotate` body (including the no-op `mid == 0` / `mid == len` arms).
+    #[kani::proof_for_contract(<[u8]>::rotate_left)]
+    #[kani::unwind(3)]
+    fn check_rotate_left() {
+        let mut arr: [u8; 2] = kani::any();
+        let len = arr.len();
+        arr.rotate_left(kani::any_where(|&m: &usize| m <= len));
+    }
+
+    #[kani::proof_for_contract(<[u8]>::rotate_right)]
+    #[kani::unwind(3)]
+    fn check_rotate_right() {
+        let mut arr: [u8; 2] = kani::any();
+        let len = arr.len();
+        arr.rotate_right(kani::any_where(|&k: &usize| k <= len));
+    }
+
+    #[kani::proof_for_contract(super::rotate::ptr_rotate)]
+    #[kani::unwind(3)]
+    fn check_ptr_rotate() {
+        let mut arr: [u8; 2] = kani::any();
+        let mid = kani::any_where(|&m: &usize| m <= arr.len());
+        let k = arr.len() - mid;
+        let p = arr.as_mut_ptr();
+        unsafe { super::rotate::ptr_rotate(mid, p.add(mid), k) };
+    }
+
+    #[kani::proof_for_contract(<[u8]>::copy_from_slice)]
+    fn check_copy_from_slice() {
+        let mut dst: [u8; CAP] = kani::any();
+        let src: [u8; CAP] = kani::any();
+        let d = any_mut(&mut dst);
+        let s = any_ref(&src);
+        kani::assume(d.len() == s.len());
+        d.copy_from_slice(s);
+    }
+
+    #[kani::proof]
+    fn check_copy_within() {
+        let mut arr: [u8; CAP] = kani::any();
+        let slice = any_mut(&mut arr);
+        let src = kani::any::<usize>()..kani::any::<usize>();
+        let dest = kani::any::<usize>();
+        if let Some(r) = try_range(src, ..slice.len()) {
+            let count = r.end - r.start;
+            if dest <= slice.len() - count {
+                slice.copy_within(r, dest);
+            }
+        }
+    }
+
+    // CAP=8 + two symbolic equal lengths times out autoharness's 10m CBMC cap
+    // on `ptr::swap_nonoverlapping`. Length 2 still runs the real swap path.
+    #[kani::proof_for_contract(<[u8]>::swap_with_slice)]
+    #[kani::unwind(3)]
+    fn check_swap_with_slice() {
+        let mut a: [u8; 2] = kani::any();
+        let mut b: [u8; 2] = kani::any();
+        a.swap_with_slice(&mut b);
+    }
+
+    #[kani::proof]
+    fn check_as_simd() {
+        let arr: [u8; 16] = kani::any();
+        let _ = any_ref(&arr).as_simd::<4>();
+    }
+
+    #[kani::proof]
+    fn check_as_simd_mut() {
+        let mut arr: [u8; 16] = kani::any();
+        let _ = any_mut(&mut arr).as_simd_mut::<4>();
+    }
+
+    #[kani::proof]
+    fn check_get_disjoint_mut() {
+        let mut arr: [u8; CAP] = kani::any();
+        let slice = any_mut(&mut arr);
+        let _ = slice.get_disjoint_mut([kani::any::<usize>(), kani::any::<usize>()]);
+    }
+
+    #[kani::proof]
+    fn check_get_disjoint_check_valid() {
+        let indices = [kani::any::<usize>(), kani::any::<usize>(), kani::any::<usize>()];
+        let _ = get_disjoint_check_valid(&indices, kani::any());
+    }
+
+    #[kani::proof]
+    fn check_as_flattened() {
+        let arr: [[u8; 2]; 4] = kani::any();
+        let slice = any_ref(&arr);
+        let _ = slice.as_flattened();
+    }
+
+    #[kani::proof]
+    fn check_as_flattened_mut() {
+        let mut arr: [[u8; 2]; 4] = kani::any();
+        let slice = any_mut(&mut arr);
+        let _ = slice.as_flattened_mut();
     }
 }
diff --git a/library/core/src/slice/rotate.rs b/library/core/src/slice/rotate.rs
index b3b64422884d5..81c9bc4d97e83 100644
--- a/library/core/src/slice/rotate.rs
+++ b/library/core/src/slice/rotate.rs
@@ -1,3 +1,7 @@
+use safety::requires;
+
+#[cfg(kani)]
+use crate::kani;
 use crate::mem::{MaybeUninit, SizedTypeProperties};
 use crate::ptr;
 
@@ -11,6 +15,17 @@ type BufType = [usize; 32];
 ///
 /// The specified range must be valid for reading and writing.
 #[inline]
+#[requires(
+    T::IS_ZST || left == 0 || right == 0 || {
+        let start = mid.wrapping_sub(left);
+        crate::ub_checks::can_dereference(ptr::slice_from_raw_parts(start, left + right))
+            && crate::ub_checks::can_write(ptr::slice_from_raw_parts_mut(start, left + right))
+    }
+)]
+#[cfg_attr(
+    kani,
+    kani::modifies(ptr::slice_from_raw_parts_mut(mid.wrapping_sub(left), left.wrapping_add(right)))
+)]
 pub(super) const unsafe fn ptr_rotate<T>(left: usize, mid: *mut T, right: usize) {
     if T::IS_ZST {
         return;