diff --git a/library/core/src/hint.rs b/library/core/src/hint.rs
index c72eeb9a9c976..a06ffde6ed9b2 100644
--- a/library/core/src/hint.rs
+++ b/library/core/src/hint.rs
@@ -4,6 +4,10 @@
 //!
 //! Hints may be compile time or runtime.
 
+use safety::requires;
+
+#[cfg(kani)]
+use crate::kani;
 use crate::mem::MaybeUninit;
 use crate::{intrinsics, ub_checks};
 
@@ -99,6 +103,7 @@ use crate::{intrinsics, ub_checks};
 #[stable(feature = "unreachable", since = "1.27.0")]
 #[rustc_const_stable(feature = "const_unreachable_unchecked", since = "1.57.0")]
 #[track_caller]
+#[requires(false)]
 pub const unsafe fn unreachable_unchecked() -> ! {
     ub_checks::assert_unsafe_precondition!(
         check_language_ub,
@@ -198,6 +203,7 @@ pub const unsafe fn unreachable_unchecked() -> ! {
 #[doc(alias = "assume")]
 #[stable(feature = "hint_assert_unchecked", since = "1.81.0")]
 #[rustc_const_stable(feature = "hint_assert_unchecked", since = "1.81.0")]
+#[requires(cond)]
 pub const unsafe fn assert_unchecked(cond: bool) {
     // SAFETY: The caller promised `cond` is true.
     unsafe {
diff --git a/library/core/src/iter/adapters/step_by.rs b/library/core/src/iter/adapters/step_by.rs
index 2d0f210420317..32604a07ca40c 100644
--- a/library/core/src/iter/adapters/step_by.rs
+++ b/library/core/src/iter/adapters/step_by.rs
@@ -1,7 +1,10 @@
 use crate::intrinsics;
 use crate::iter::{TrustedLen, TrustedRandomAccess, from_fn};
+#[cfg(kani)]
+use crate::kani;
 use crate::num::NonZero;
 use crate::ops::{Range, Try};
+use crate::ub_checks::Invariant;
 
 /// An iterator for stepping iterators by a custom amount.
 ///
@@ -29,6 +32,13 @@ pub struct StepBy<I> {
     first_take: bool,
 }
 
+#[unstable(feature = "ub_checks", issue = "none")]
+impl<I> Invariant for StepBy<I> {
+    fn is_safe(&self) -> bool {
+        self.step_minus_one < usize::MAX
+    }
+}
+
 impl<I> StepBy<I> {
     #[inline]
     pub(in crate::iter) fn new(iter: I, step: usize) -> StepBy<I> {
diff --git a/library/core/src/ops/index_range.rs b/library/core/src/ops/index_range.rs
index 507fa9460bea6..2a347ded448f0 100644
--- a/library/core/src/ops/index_range.rs
+++ b/library/core/src/ops/index_range.rs
@@ -1,4 +1,8 @@
+use safety::requires;
+
 use crate::iter::{FusedIterator, TrustedLen};
+#[cfg(kani)]
+use crate::kani;
 use crate::num::NonZero;
 use crate::ops::{NeverShortCircuit, Try};
 use crate::ub_checks;
@@ -20,6 +24,7 @@ impl IndexRange {
     /// - `start <= end`
     #[inline]
     #[track_caller]
+    #[requires(start <= end)]
     pub(crate) const unsafe fn new_unchecked(start: usize, end: usize) -> Self {
         ub_checks::assert_unsafe_precondition!(
             check_library_ub,
@@ -54,6 +59,8 @@ impl IndexRange {
     /// # Safety
     /// - Can only be called when `start < end`, aka when `len > 0`.
     #[inline]
+    #[requires(self.start < self.end)]
+    #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn next_unchecked(&mut self) -> usize {
         debug_assert!(self.start < self.end);
 
@@ -66,6 +73,8 @@ impl IndexRange {
     /// # Safety
     /// - Can only be called when `start < end`, aka when `len > 0`.
     #[inline]
+    #[requires(self.start < self.end)]
+    #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn next_back_unchecked(&mut self) -> usize {
         debug_assert!(self.start < self.end);
 
@@ -225,3 +234,34 @@ impl ExactSizeIterator for IndexRange {
 unsafe impl TrustedLen for IndexRange {}
 
 impl FusedIterator for IndexRange {}
+#[cfg(kani)]
+mod verify {
+    use super::*;
+    #[kani::proof_for_contract(IndexRange::new_unchecked)]
+    fn proof_for_index_range_new_unchecked() {
+        let start = kani::any::<usize>();
+        let end = kani::any::<usize>();
+
+        unsafe { IndexRange::new_unchecked(start, end) };
+    }
+
+    #[kani::proof_for_contract(IndexRange::next_unchecked)]
+    fn proof_for_index_range_next_unchecked() {
+        let start = kani::any::<usize>();
+        let end = kani::any::<usize>();
+
+        let mut range = unsafe { IndexRange::new_unchecked(start, end) };
+
+        unsafe { range.next_unchecked() };
+    }
+
+    #[kani::proof_for_contract(IndexRange::next_back_unchecked)]
+    fn proof_for_index_range_next_back_unchecked() {
+        let start = kani::any::<usize>();
+        let end = kani::any::<usize>();
+
+        let mut range = unsafe { IndexRange::new_unchecked(start, end) };
+
+        unsafe { range.next_back_unchecked() };
+    }
+}
diff --git a/library/std/src/sync/mpmc/context.rs b/library/std/src/sync/mpmc/context.rs
index 6b2f4cb6ffd29..e6eb6b9cace03 100644
--- a/library/std/src/sync/mpmc/context.rs
+++ b/library/std/src/sync/mpmc/context.rs
@@ -1,5 +1,11 @@
 //! Thread-local channel context.
 
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+use core::kani;
+
+use safety::requires;
+
 use super::select::Selected;
 use super::waker::current_thread_id;
 use crate::cell::Cell;
@@ -116,6 +122,7 @@ impl Context {
     /// # Safety
     /// This may only be called from the thread this `Context` belongs to.
     #[inline]
+    #[requires(self.thread_id() == current_thread_id())]
     pub unsafe fn wait_until(&self, deadline: Option<Instant>) -> Selected {
         loop {
             // Check whether an operation has been selected.