diff --git a/library/alloctests/tests/sort/known_good_stable_sort.rs b/library/alloctests/tests/sort/known_good_stable_sort.rs
index 2df891462538d..bc40f3874847b 100644
--- a/library/alloctests/tests/sort/known_good_stable_sort.rs
+++ b/library/alloctests/tests/sort/known_good_stable_sort.rs
@@ -4,9 +4,18 @@
 //
 // Based on https://github.com/voultapher/tiny-sort-rs.
 
+#![feature(ub_checks)]
 use alloc::alloc::{Layout, alloc, dealloc};
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+use core::kani;
+#[allow(unused_imports)]
+#[unstable(feature = "ub_checks", issue = "none")]
+use core::ub_checks::*;
 use std::ptr;
 
+use safety::requires;
+
 /// Sort `v` preserving initial order of equal elements.
 ///
 /// - Guaranteed O(N * log(N)) worst case perf
@@ -48,6 +57,7 @@ fn stable_sort<T, F: FnMut(&T, &T) -> bool>(v: &mut [T], mut is_less: F) {
 ///
 /// SAFETY: The caller has to ensure that len is > 0 and that T is not a ZST.
 #[inline(never)]
+#[requires(len > 0 && size_of::<T>() > 0)]
 unsafe fn mergesort_main<T, F: FnMut(&T, &T) -> bool>(v: &mut [T], is_less: &mut F) {
     // While it would be nice to have a merge implementation that only requires N / 2 auxiliary
     // memory. Doing so would make the merge implementation significantly more complex and
@@ -66,6 +76,7 @@ unsafe fn mergesort_main<T, F: FnMut(&T, &T) -> bool>(v: &mut [T], is_less: &mut
 ///
 /// Buffer as pointed to by `scratch` must have space for `v.len()` writes. And must not alias `v`.
 #[inline(always)]
+#[requires(can_dereference(scratch_ptr) && !same_allocation(scratch_ptr, v.as_ptr()))]
 unsafe fn mergesort_core<T, F: FnMut(&T, &T) -> bool>(
     v: &mut [T],
     scratch_ptr: *mut T,
@@ -97,6 +108,7 @@ unsafe fn mergesort_core<T, F: FnMut(&T, &T) -> bool>(
 /// SAFETY: The caller must ensure that `scratch_ptr` is valid for `v.len()` writes. And that mid is
 /// in-bounds.
 #[inline(always)]
+#[requires(mid <= len && can_dereference(scratch_ptr) && !same_allocation(scratch_ptr, v.as_ptr()))]
 unsafe fn merge<T, F>(v: &mut [T], scratch_ptr: *mut T, is_less: &mut F, mid: usize)
 where
     F: FnMut(&T, &T) -> bool,
@@ -143,6 +155,7 @@ where
 }
 
 // SAFETY: The caller has to ensure that Option is Some, UB otherwise.
+#[requires(opt_val.is_some())]
 unsafe fn unwrap_unchecked<T>(opt_val: Option<T>) -> T {
     match opt_val {
         Some(val) => val,
@@ -165,6 +178,7 @@ struct BufGuard<T> {
 
 impl<T> BufGuard<T> {
     // SAFETY: The caller has to ensure that len is not 0 and that T is not a ZST.
+    #[requires(len > 0 && size_of::<T>() > 0)]
     unsafe fn new(len: usize) -> Self {
         debug_assert!(len > 0 && size_of::<T>() > 0);
 
diff --git a/library/core/src/array/ascii.rs b/library/core/src/array/ascii.rs
index 792a57e3fa25c..6bc96d143ea4c 100644
--- a/library/core/src/array/ascii.rs
+++ b/library/core/src/array/ascii.rs
@@ -1,4 +1,8 @@
+use safety::requires;
+
 use crate::ascii;
+#[cfg(kani)]
+use crate::kani;
 
 impl<const N: usize> [u8; N] {
     /// Converts this array of bytes into an array of ASCII characters,
@@ -36,6 +40,7 @@ impl<const N: usize> [u8; N] {
     #[unstable(feature = "ascii_char", issue = "110998")]
     #[must_use]
     #[inline]
+    #[requires(self.iter().all(|&b| b <= 127))]
     pub const unsafe fn as_ascii_unchecked(&self) -> &[ascii::Char; N] {
         let byte_ptr: *const [u8; N] = self;
         let ascii_ptr = byte_ptr as *const [ascii::Char; N];
@@ -43,3 +48,25 @@ impl<const N: usize> [u8; N] {
         unsafe { &*ascii_ptr }
     }
 }
+#[cfg(kani)]
+mod verify {
+    use super::*;
+
+    #[cfg(kani)]
+    #[kani::proof_for_contract(<[u8; 4]>::as_ascii_unchecked)]
+    #[kani::unwind(10)]
+    fn proof_for_as_ascii_unchecked() {
+        // Create a small array of bytes that are all ASCII (0-127)
+        let mut bytes = [0u8; 4];
+
+        // Fill the array with arbitrary ASCII bytes
+        for i in 0..4 {
+            bytes[i] = kani::any::<u8>() & 0x7F; // Ensure value is in range 0-127
+        }
+
+        // The precondition self.iter().all(|&b| b <= 127) is automatically assumed by Kani
+
+        // Call the function - if preconditions are met, this should not cause undefined behavior
+        unsafe { bytes.as_ascii_unchecked() };
+    }
+}
diff --git a/library/core/src/array/drain.rs b/library/core/src/array/drain.rs
index 5fadf907b6219..6545ebebed425 100644
--- a/library/core/src/array/drain.rs
+++ b/library/core/src/array/drain.rs
@@ -1,4 +1,8 @@
+use safety::requires;
+
 use crate::iter::{TrustedLen, UncheckedIterator};
+#[cfg(kani)]
+use crate::kani;
 use crate::mem::ManuallyDrop;
 use crate::ptr::drop_in_place;
 use crate::slice;
@@ -66,6 +70,7 @@ impl<T> ExactSizeIterator for Drain<'_, T> {
 unsafe impl<T> TrustedLen for Drain<'_, T> {}
 
 impl<T> UncheckedIterator for Drain<'_, T> {
+    #[requires(self.0.len() > 0)]
     unsafe fn next_unchecked(&mut self) -> T {
         // SAFETY: `Drain` is 1:1 with the inner iterator, so if the caller promised
         // that there's an element left, the inner iterator has one too.
diff --git a/library/core/src/fmt/rt.rs b/library/core/src/fmt/rt.rs
index fb858a0572612..ecd08eaef8f1d 100644
--- a/library/core/src/fmt/rt.rs
+++ b/library/core/src/fmt/rt.rs
@@ -6,9 +6,14 @@
 //!
 //! Do not modify them without understanding the consequences for the format_args!() macro.
 
+use safety::requires;
+
 use super::*;
 use crate::hint::unreachable_unchecked;
+#[cfg(kani)]
+use crate::kani;
 use crate::ptr::NonNull;
+use crate::ub_checks::Invariant;
 
 #[lang = "format_placeholder"]
 #[derive(Copy, Clone)]
@@ -161,6 +166,7 @@ impl Argument<'_> {
     ///
     /// This argument must actually be a placeholder argument.
     #[inline]
+    #[requires(matches!(self.ty, ArgumentType::Placeholder { .. }))]
     pub(super) unsafe fn fmt(&self, f: &mut Formatter<'_>) -> Result {
         match self.ty {
             // SAFETY:
@@ -228,6 +234,7 @@ impl<'a> Arguments<'a> {
     /// const _: () = if false { panic!("a {:1}", "a") };
     /// ```
     #[inline]
+    #[requires(pieces.len() >= fmt.len())]
     pub unsafe fn new_v1_formatted(
         pieces: &'a [&'static str],
         args: &'a [rt::Argument<'a>],
diff --git a/library/core/src/iter/adapters/map.rs b/library/core/src/iter/adapters/map.rs
index c738b8cda957b..bf9f0c48fec3b 100644
--- a/library/core/src/iter/adapters/map.rs
+++ b/library/core/src/iter/adapters/map.rs
@@ -204,6 +204,7 @@ where
     I: UncheckedIterator,
     F: FnMut(I::Item) -> B,
 {
+    #[requires(self.iter.size_hint().0 > 0)]
     unsafe fn next_unchecked(&mut self) -> B {
         // SAFETY: `Map` is 1:1 with the inner iterator, so if the caller promised
         // that there's an element left, the inner iterator has one too.
diff --git a/library/core/src/iter/adapters/map_windows.rs b/library/core/src/iter/adapters/map_windows.rs
index 0dada9eb6aacf..536251a137da0 100644
--- a/library/core/src/iter/adapters/map_windows.rs
+++ b/library/core/src/iter/adapters/map_windows.rs
@@ -1,5 +1,6 @@
 use crate::iter::FusedIterator;
 use crate::mem::MaybeUninit;
+use crate::ub_checks::Invariant;
 use crate::{fmt, ptr};
 
 /// An iterator over the mapped windows of another iterator.
@@ -289,3 +290,10 @@ where
         Self { f: self.f.clone(), inner: self.inner.clone() }
     }
 }
+
+#[unstable(feature = "ub_checks", issue = "none")]
+impl<T, const N: usize> Invariant for Buffer<T, N> {
+    fn is_safe(&self) -> bool {
+        self.start + N <= 2 * N
+    }
+}
diff --git a/library/core/src/iter/traits/unchecked_iterator.rs b/library/core/src/iter/traits/unchecked_iterator.rs
index ae4bfcad4e68f..ee94f7191349e 100644
--- a/library/core/src/iter/traits/unchecked_iterator.rs
+++ b/library/core/src/iter/traits/unchecked_iterator.rs
@@ -1,4 +1,8 @@
+use safety::requires;
+
 use crate::iter::TrustedLen;
+#[cfg(kani)]
+use crate::kani;
 
 /// [`TrustedLen`] cannot have methods, so this allows augmenting it.
 ///
@@ -27,6 +31,8 @@ pub(crate) trait UncheckedIterator: TrustedLen {
     /// point you might want to implement this manually instead.
     #[unstable(feature = "trusted_len_next_unchecked", issue = "37572")]
     #[inline]
+    #[requires(self.size_hint().0 > 0)]
+    #[cfg_attr(kani, kani::modifies(self))]
     unsafe fn next_unchecked(&mut self) -> Self::Item {
         let opt = self.next();
         // SAFETY: The caller promised that we're not empty, and