diff --git a/library/core/src/fmt/num.rs b/library/core/src/fmt/num.rs
index 253a7b7587e49..2f3ecb08b09c1 100644
--- a/library/core/src/fmt/num.rs
+++ b/library/core/src/fmt/num.rs
@@ -1,6 +1,10 @@
 //! Integer and floating-point number formatting
 
+use safety::requires;
+
 use crate::fmt::NumBuffer;
+#[cfg(kani)]
+use crate::kani;
 use crate::mem::MaybeUninit;
 use crate::num::fmt as numfmt;
 use crate::{fmt, str};
@@ -180,6 +184,8 @@ macro_rules! impl_Display {
                 reason = "specialized method meant to only be used by `SpecToString` implementation",
                 issue = "none"
             )]
+            #[requires(buf.len() >= Self::MAX.ilog10() as usize + 1)]
+            #[cfg_attr(kani, kani::modifies(buf))]
             pub unsafe fn _fmt<'a>(self, buf: &'a mut [MaybeUninit::<u8>]) -> &'a str {
                 // SAFETY: `buf` will always be big enough to contain all digits.
                 let offset = unsafe { self._fmt_inner(buf) };
@@ -596,6 +602,8 @@ impl_Debug! {
 #[cfg(any(target_pointer_width = "64", target_arch = "wasm32"))]
 mod imp {
     use super::*;
+    #[cfg(kani)]
+    use crate::kani;
     impl_Display!(i8, u8, i16, u16, i32, u32, i64, u64, isize, usize; as u64 into display_u64);
     impl_Exp!(i8, u8, i16, u16, i32, u32, i64, u64, isize, usize; as u64 into exp_u64);
 }
@@ -603,6 +611,8 @@ mod imp {
 #[cfg(not(any(target_pointer_width = "64", target_arch = "wasm32")))]
 mod imp {
     use super::*;
+    #[cfg(kani)]
+    use crate::kani;
     impl_Display!(i8, u8, i16, u16, i32, u32, isize, usize; as u32 into display_u32);
     impl_Display!(i64, u64; as u64 into display_u64);
 
@@ -645,6 +655,8 @@ impl u128 {
         reason = "specialized method meant to only be used by `SpecToString` implementation",
         issue = "none"
     )]
+    #[requires(buf.len() >= U128_MAX_DEC_N)]
+    #[cfg_attr(kani, kani::modifies(buf))]
     pub unsafe fn _fmt<'a>(self, buf: &'a mut [MaybeUninit<u8>]) -> &'a str {
         // SAFETY: `buf` will always be big enough to contain all digits.
         let offset = unsafe { self._fmt_inner(buf) };
@@ -862,3 +874,26 @@ fn div_rem_1e16(n: u128) -> (u128, u64) {
     let rem = n - quot * D;
     (quot, rem as u64)
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+    use crate::kani;
+    use crate::mem::MaybeUninit;
+
+    /// Successor of the former `fmt::num::parse_u64_into` (removed when decimal
+    /// formatting was rewritten). `_fmt` still fills a `MaybeUninit<u8>` buffer
+    /// with ASCII digits of a `u64`.
+    #[cfg(not(feature = "optimize_for_size"))]
+    #[kani::proof_for_contract(u64::_fmt)]
+    #[kani::unwind(21)]
+    fn check_u64_fmt_parse_u64_into_successor() {
+        let n: u64 = kani::any();
+        const MAX: usize = 20;
+        let mut buf = [MaybeUninit::<u8>::uninit(); MAX];
+        let s = unsafe { n._fmt(&mut buf) };
+        assert!(s.len() <= MAX);
+        assert!(!s.is_empty());
+    }
+}
diff --git a/library/core/src/intrinsics/mod.rs b/library/core/src/intrinsics/mod.rs
index ddadeeb3c786a..dfbde071ed9f9 100644
--- a/library/core/src/intrinsics/mod.rs
+++ b/library/core/src/intrinsics/mod.rs
@@ -2753,10 +2753,8 @@ pub const fn contract_check_ensures<C: Fn(&Ret) -> bool + Copy, Ret>(
 #[rustc_intrinsic]
 // VTable pointers must be valid for dereferencing at least 3 `usize` (size, alignment and drop):
 // <https://github.com/rust-lang/unsafe-code-guidelines/issues/166>
-// TODO: we can no longer do this given https://github.com/model-checking/kani/issues/3325 (this
-// function used to have a dummy body, but no longer has since
-// https://github.com/rust-lang/rust/pull/137489 has been merged).
-// #[requires(ub_checks::can_dereference(_ptr as *const [usize; 3]))]
+// Contracts cannot sit on this bodyless intrinsic (kani#3325); see
+// `vtable_size_wrapper` in `verify_memory.rs`.
 pub unsafe fn vtable_size(_ptr: *const ()) -> usize;
 
 /// The intrinsic will return the alignment stored in that vtable.
@@ -2769,10 +2767,8 @@ pub unsafe fn vtable_size(_ptr: *const ()) -> usize;
 #[rustc_intrinsic]
 // VTable pointers must be valid for dereferencing at least 3 `usize` (size, alignment and drop):
 // <https://github.com/rust-lang/unsafe-code-guidelines/issues/166>
-// TODO: we can no longer do this given https://github.com/model-checking/kani/issues/3325 (this
-// function used to have a dummy body, but no longer has since
-// https://github.com/rust-lang/rust/pull/137489 has been merged).
-// #[requires(ub_checks::can_dereference(_ptr as *const [usize; 3]))]
+// Contracts cannot sit on this bodyless intrinsic (kani#3325); see
+// `vtable_align_wrapper` in `verify_memory.rs`.
 pub unsafe fn vtable_align(_ptr: *const ()) -> usize;
 
 /// The size of a type in bytes.
@@ -2960,7 +2956,9 @@ fn check_copy_untyped<T>(src: *const T, dst: *mut T, count: usize) -> bool {
         // them and check it. Using quantifiers would not add value as we can rely on the solver to
         // pick an uninitialized element if such an element exists.
         let elem = kani::any_where(|val: &usize| *val < count);
-        let src_data = src as *const u8;
+        // Offset both sides by `elem`. Comparing `dst[elem]` against `src[0]`
+        // is wrong when initialization differs across elements.
+        let src_data = unsafe { src.add(elem) } as *const u8;
         let dst_data = unsafe { dst.add(elem) } as *const u8;
         ub_checks::can_dereference(unsafe { src_data.add(byte) })
             == ub_checks::can_dereference(unsafe { dst_data.add(byte) })
@@ -2981,14 +2979,8 @@ fn check_copy_untyped<T>(src: *const T, dst: *mut T, count: usize) -> bool {
 #[rustc_nounwind]
 #[rustc_intrinsic]
 // Copy is "untyped".
-// TODO: we can no longer do this given https://github.com/model-checking/kani/issues/3325 (this
-// function used to have a dummy body, but no longer has)
-// #[cfg_attr(kani, kani::modifies(crate::ptr::slice_from_raw_parts(dst, count)))]
-// #[requires(!count.overflowing_mul(size_of::<T>()).1
-//   && ub_checks::can_dereference(core::ptr::slice_from_raw_parts(src as *const crate::mem::MaybeUninit<T>, count))
-//   && ub_checks::can_write(core::ptr::slice_from_raw_parts_mut(dst, count))
-//   && ub_checks::maybe_is_nonoverlapping(src as *const (), dst as *const (), size_of::<T>(), count))]
-// #[ensures(|_| { check_copy_untyped(src, dst, count)})]
+// Contracts cannot sit on this bodyless intrinsic (kani#3325); see
+// `copy_nonoverlapping_wrapper` in `verify_memory.rs`.
 pub const unsafe fn copy_nonoverlapping<T>(src: *const T, dst: *mut T, count: usize);
 
 /// This is an accidentally-stable alias to [`ptr::copy`]; use that instead.
@@ -3000,13 +2992,8 @@ pub const unsafe fn copy_nonoverlapping<T>(src: *const T, dst: *mut T, count: us
 #[rustc_const_stable(feature = "const_intrinsic_copy", since = "1.83.0")]
 #[rustc_nounwind]
 #[rustc_intrinsic]
-// TODO: we can no longer do this given https://github.com/model-checking/kani/issues/3325 (this
-// function used to have a dummy body, but no longer has)
-// #[requires(!count.overflowing_mul(size_of::<T>()).1
-//   && ub_checks::can_dereference(core::ptr::slice_from_raw_parts(src as *const crate::mem::MaybeUninit<T>, count))
-//   && ub_checks::can_write(core::ptr::slice_from_raw_parts_mut(dst, count)))]
-// #[ensures(|_| { check_copy_untyped(src, dst, count) })]
-// #[cfg_attr(kani, kani::modifies(crate::ptr::slice_from_raw_parts(dst, count)))]
+// Contracts cannot sit on this bodyless intrinsic (kani#3325); see
+// `copy_wrapper` in `verify_memory.rs`.
 pub const unsafe fn copy<T>(src: *const T, dst: *mut T, count: usize);
 
 /// This is an accidentally-stable alias to [`ptr::write_bytes`]; use that instead.
@@ -3018,14 +3005,8 @@ pub const unsafe fn copy<T>(src: *const T, dst: *mut T, count: usize);
 #[rustc_const_stable(feature = "const_intrinsic_copy", since = "1.83.0")]
 #[rustc_nounwind]
 #[rustc_intrinsic]
-// TODO: we can no longer do this given https://github.com/model-checking/kani/issues/3325 (this
-// function used to have a dummy body, but no longer has)
-// #[requires(!count.overflowing_mul(size_of::<T>()).1
-//   && ub_checks::can_write(core::ptr::slice_from_raw_parts_mut(dst, count)))]
-// #[requires(ub_checks::maybe_is_aligned_and_not_null(dst as *const (), align_of::<T>(), T::IS_ZST || count == 0))]
-// #[ensures(|_|
-//     ub_checks::can_dereference(crate::ptr::slice_from_raw_parts(dst as *const u8, count * size_of::<T>())))]
-// #[cfg_attr(kani, kani::modifies(crate::ptr::slice_from_raw_parts(dst, count)))]
+// Contracts cannot sit on this bodyless intrinsic (kani#3325); see
+// `write_bytes_wrapper` in `verify_memory.rs`.
 pub const unsafe fn write_bytes<T>(dst: *mut T, val: u8, count: usize);
 
 /// Returns the minimum (IEEE 754-2008 minNum) of two `f16` values.
@@ -3497,33 +3478,7 @@ mod verify {
         });
     }
 
-    // #[kani::proof_for_contract(copy)]
-    // fn check_copy() {
-    //     run_with_arbitrary_ptrs::<char>(|src, dst| unsafe { copy(src, dst, kani::any()) });
-    // }
-
-    // #[kani::proof_for_contract(copy_nonoverlapping)]
-    // fn check_copy_nonoverlapping() {
-    //     // Note: cannot use `ArbitraryPointer` here.
-    //     // The `ArbitraryPtr` will arbitrarily initialize memory by indirectly invoking
-    //     // `copy_nonoverlapping`.
-    //     // Kani contract checking would fail due to existing restriction on calls to
-    //     // the function under verification.
-    //     let gen_any_ptr = |buf: &mut [MaybeUninit<char>; 100]| -> *mut char {
-    //         let base = buf.as_mut_ptr() as *mut u8;
-    //         base.wrapping_add(kani::any_where(|offset: &usize| *offset < 400)) as *mut char
-    //     };
-    //     let mut buffer1 = [MaybeUninit::<char>::uninit(); 100];
-    //     for i in 0..100 {
-    //         if kani::any() {
-    //             buffer1[i] = MaybeUninit::new(kani::any());
-    //         }
-    //     }
-    //     let mut buffer2 = [MaybeUninit::<char>::uninit(); 100];
-    //     let src = gen_any_ptr(&mut buffer1);
-    //     let dst = if kani::any() { gen_any_ptr(&mut buffer2) } else { gen_any_ptr(&mut buffer1) };
-    //     unsafe { copy_nonoverlapping(src, dst, kani::any()) }
-    // }
+    // Copy / copy_nonoverlapping / write_bytes proofs: see `verify_memory.rs`.
 
     //We need this wrapper because transmute_unchecked is an intrinsic, for which Kani does
     //not currently support contracts (https://github.com/model-checking/kani/issues/3345)
@@ -4116,18 +4071,6 @@ mod verify {
     gen_compound_harnesses!(arr_mod, [u8; 2]);
     gen_compound_harnesses!(struct_mod, u8_struct);
 
-    // FIXME: Enable this harness once <https://github.com/model-checking/kani/issues/90> is fixed.
-    // Harness triggers a spurious failure when writing 0 bytes to an invalid memory location,
-    // which is a safe operation.
-    #[cfg(not(kani))]
-    #[kani::proof_for_contract(write_bytes)]
-    fn check_write_bytes() {
-        let mut generator = PointerGenerator::<100>::new();
-        let ArbitraryPointer { ptr, status, .. } = generator.any_alloc_status::<char>();
-        kani::assume(supported_status(status));
-        unsafe { write_bytes(ptr, kani::any(), kani::any()) };
-    }
-
     fn run_with_arbitrary_ptrs<T: Arbitrary>(harness: impl Fn(*mut T, *mut T)) {
         let mut generator1 = PointerGenerator::<100>::new();
         let mut generator2 = PointerGenerator::<100>::new();
@@ -4151,3 +4094,7 @@ mod verify {
         status != AllocationStatus::Dangling && status != AllocationStatus::DeadObject
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify_memory;
diff --git a/library/core/src/intrinsics/verify_memory.rs b/library/core/src/intrinsics/verify_memory.rs
new file mode 100644
index 0000000000000..9b11ea796c8ec
--- /dev/null
+++ b/library/core/src/intrinsics/verify_memory.rs
@@ -0,0 +1,700 @@
+//! Challenge 2: safety contracts for raw-pointer `core::intrinsics`.
+//!
+//! Bodyless `#[rustc_intrinsic]` declarations cannot carry Kani contracts
+//! (kani#3325 / kani#3345). Contracts therefore sit on thin wrappers that
+//! immediately call the intrinsic — the same pattern as
+//! `transmute_unchecked_wrapper` in `mod.rs`.
+//!
+//! Tractability bounds (buffer caps, representative overlap shifts) live in
+//! harnesses via `kani::assume` / fixed constants, never in `#[requires]`.
+//! `#[requires]` is only the documented safety condition.
+//!
+//! `kani::cover` after each successful call witnesses that the precondition
+//! was satisfiable (an unreached harness is otherwise reported SUCCESSFUL).
+
+use safety::{ensures, requires};
+
+use super::*;
+use crate::mem::{self, MaybeUninit, SizedTypeProperties};
+use crate::ptr::{self, DynMetadata};
+use crate::{kani, ub_checks};
+
+/// Object-safe probe so vtable tests are not tied to `fmt::Debug` (or to one
+/// erased type). An empty trait still has a vtable with drop/size/align.
+trait Probe {}
+impl<T> Probe for T {}
+
+fn vtable_ptr(obj: *const dyn Probe) -> *const () {
+    let meta = ptr::metadata(obj);
+    // `DynMetadata` is ABI-equivalent to the vtable pointer
+    // (`DynMetadata::vtable_ptr` is private and uses the same transmute).
+    unsafe { mem::transmute::<DynMetadata<dyn Probe>, *const ()>(meta) }
+}
+
+fn copy_len_ok<T>(count: usize) -> bool {
+    count.checked_mul(size_of::<T>()).is_some()
+}
+
+fn aligned_for_copy<T>(p: *const (), count: usize) -> bool {
+    ub_checks::maybe_is_aligned_and_not_null(p, align_of::<T>(), T::IS_ZST || count == 0)
+}
+
+/// Untyped source: bytes may be uninitialized, so the region is `MaybeUninit<T>`.
+fn src_readable<T>(src: *const T, count: usize) -> bool {
+    copy_len_ok::<T>(count)
+        && aligned_for_copy::<T>(src as *const (), count)
+        && (count == 0
+            || ub_checks::can_dereference(ptr::slice_from_raw_parts(
+                src as *const MaybeUninit<T>,
+                count,
+            )))
+}
+
+fn dst_writable<T>(dst: *mut T, count: usize) -> bool {
+    copy_len_ok::<T>(count)
+        && aligned_for_copy::<T>(dst as *const (), count)
+        && (count == 0 || ub_checks::can_write(ptr::slice_from_raw_parts_mut(dst, count)))
+}
+
+fn compare_bytes_ord(left: *const u8, right: *const u8, bytes: usize) -> crate::cmp::Ordering {
+    let mut i = 0;
+    while i < bytes {
+        let a = unsafe { *left.add(i) };
+        let b = unsafe { *right.add(i) };
+        if a != b {
+            return a.cmp(&b);
+        }
+        i += 1;
+    }
+    crate::cmp::Ordering::Equal
+}
+
+// ---------------------------------------------------------------------------
+// typed_swap_nonoverlapping — already contracted on the intrinsic (has a body).
+// Criterion 2: the fallback body is `ptr::swap_nonoverlapping(x, y, 1)`.
+// ---------------------------------------------------------------------------
+
+/// Verifies the fallback body of `typed_swap_nonoverlapping` against the same
+/// documented safety condition. The intrinsic itself is already contracted in
+/// `mod.rs`; this wrapper exists so the fallback is not only trusted via Kani's
+/// built-in model of the intrinsic.
+#[requires(ub_checks::can_dereference(x) && ub_checks::can_write(x))]
+#[requires(ub_checks::can_dereference(y) && ub_checks::can_write(y))]
+#[requires(x.addr() != y.addr() || size_of::<T>() == 0)]
+#[requires(ub_checks::maybe_is_nonoverlapping(x as *const (), y as *const (), size_of::<T>(), 1))]
+#[ensures(|_| ub_checks::can_dereference(x) && ub_checks::can_dereference(y))]
+#[kani::modifies(x)]
+#[kani::modifies(y)]
+unsafe fn typed_swap_fallback_wrapper<T>(x: *mut T, y: *mut T) {
+    // Same body as `typed_swap_nonoverlapping`'s fallback.
+    unsafe { ptr::swap_nonoverlapping(x, y, 1) };
+}
+
+// ---------------------------------------------------------------------------
+// vtable_size / vtable_align
+//
+// Documented safety: `ptr` must point to a vtable. Kani has no vtable
+// predicate; dereferenceability of the first three `usize` words (drop, size,
+// align — rustc `COMMON_VTABLE_ENTRIES`) is the necessary approximation.
+// Sufficiency is assumed from compiler-produced vtables. Functional checks in
+// the harnesses use `size_of::<T>()` / `align_of::<T>()` of the *erased* type,
+// not a fixture hard-coded into `#[ensures]`.
+// ---------------------------------------------------------------------------
+
+#[requires(ub_checks::can_dereference(ptr as *const [usize; 3]))]
+unsafe fn vtable_size_wrapper(ptr: *const ()) -> usize {
+    unsafe { vtable_size(ptr) }
+}
+
+#[requires(ub_checks::can_dereference(ptr as *const [usize; 3]))]
+unsafe fn vtable_align_wrapper(ptr: *const ()) -> usize {
+    unsafe { vtable_align(ptr) }
+}
+
+// ---------------------------------------------------------------------------
+// copy / copy_nonoverlapping / write_bytes
+// ---------------------------------------------------------------------------
+
+#[requires(src_readable(src, count) && dst_writable(dst, count))]
+#[kani::modifies(ptr::slice_from_raw_parts(dst, count))]
+unsafe fn copy_wrapper<T>(src: *const T, dst: *mut T, count: usize) {
+    unsafe { copy(src, dst, count) }
+}
+
+#[requires(
+    src_readable(src, count)
+        && dst_writable(dst, count)
+        && ub_checks::maybe_is_nonoverlapping(src as *const (), dst as *const (), size_of::<T>(), count)
+)]
+#[ensures(|_| check_copy_untyped(src, dst, count))]
+#[kani::modifies(ptr::slice_from_raw_parts(dst, count))]
+unsafe fn copy_nonoverlapping_wrapper<T>(src: *const T, dst: *mut T, count: usize) {
+    unsafe { copy_nonoverlapping(src, dst, count) }
+}
+
+#[requires(dst_writable(dst, count))]
+#[ensures(|_| {
+    count == 0
+        || ub_checks::can_dereference(ptr::slice_from_raw_parts(
+            dst as *const u8,
+            count * size_of::<T>(),
+        ))
+})]
+#[kani::modifies(ptr::slice_from_raw_parts(dst, count))]
+unsafe fn write_bytes_wrapper<T>(dst: *mut T, val: u8, count: usize) {
+    unsafe { write_bytes(dst, val, count) }
+}
+
+// ---------------------------------------------------------------------------
+// size_of_val / align_of_val  (min_align_of_val is the mem wrapper)
+//
+// Documented (`size_of_val_raw` / `align_of_val_raw`):
+// - Sized: always safe, including null/dangling.
+// - slice tail: length initialized, total size fits in `isize` (len 0 always ok).
+// - trait object: vtable valid, total size fits in `isize`.
+// `can_dereference` is stronger than the Sized case and is not used there.
+// ---------------------------------------------------------------------------
+
+#[ensures(|result| *result == size_of::<T>())]
+unsafe fn size_of_val_sized_wrapper<T>(ptr: *const T) -> usize {
+    unsafe { size_of_val(ptr) }
+}
+
+#[requires({
+    let len = ptr.len();
+    len == 0
+        || size_of::<T>().checked_mul(len).is_some_and(|bytes| bytes <= isize::MAX as usize)
+})]
+#[ensures(|result| *result == ptr.len() * size_of::<T>())]
+unsafe fn size_of_val_slice_wrapper<T>(ptr: *const [T]) -> usize {
+    unsafe { size_of_val(ptr) }
+}
+
+#[requires(ub_checks::can_dereference(vtable_ptr(ptr) as *const [usize; 3]))]
+unsafe fn size_of_val_dyn_wrapper(ptr: *const dyn Probe) -> usize {
+    unsafe { size_of_val(ptr) }
+}
+
+#[ensures(|result| *result == align_of::<T>())]
+unsafe fn align_of_val_sized_wrapper<T>(ptr: *const T) -> usize {
+    unsafe { align_of_val(ptr) }
+}
+
+#[requires({
+    let len = ptr.len();
+    len == 0
+        || size_of::<T>().checked_mul(len).is_some_and(|bytes| bytes <= isize::MAX as usize)
+})]
+#[ensures(|result| *result == align_of::<T>())]
+unsafe fn align_of_val_slice_wrapper<T>(ptr: *const [T]) -> usize {
+    unsafe { align_of_val(ptr) }
+}
+
+#[requires(ub_checks::can_dereference(vtable_ptr(ptr) as *const [usize; 3]))]
+unsafe fn align_of_val_dyn_wrapper(ptr: *const dyn Probe) -> usize {
+    unsafe { align_of_val(ptr) }
+}
+
+// ---------------------------------------------------------------------------
+// arith_offset
+//
+// Documented: always safe; the result need not be dereferenceable and wraps
+// in two's complement. There is no language offset bound.
+//
+// The wrapping-address `#[ensures]` is only CBMC-faithful while the result
+// stays in a small in-object window (`offset ∈ [0, 8]` on a `[u8; 8]`).
+// That window is a Kani/CBMC pointer-model bound, not a safety precondition
+// (out-of-object `ptr as usize` is not integer wrapping in CBMC). Unbounded
+// safety is the separate `#[kani::proof]` that calls `arith_offset` itself.
+// ---------------------------------------------------------------------------
+
+#[requires(offset >= 0 && offset <= 8)]
+#[ensures(|result| {
+    (*result as usize)
+        == (dst as usize).wrapping_add((offset as usize).wrapping_mul(size_of::<T>()))
+})]
+unsafe fn arith_offset_wrapper<T>(dst: *const T, offset: isize) -> *const T {
+    unsafe { arith_offset(dst, offset) }
+}
+
+// ---------------------------------------------------------------------------
+// Volatile family
+//
+// `volatile_load` / `volatile_store` are modelled by pinned Kani. Their
+// contracts cover the documented *Rust-allocation* case (`read_volatile` /
+// `write_volatile`: valid, aligned, initialized). The documented MMIO case
+// (aligned non-trapping access outside any Rust allocation) is an unverified
+// residual: Kani has no model of I/O memory.
+//
+// `volatile_copy_*`, `volatile_set_memory`, `unaligned_volatile_{load,store}`
+// are not codegen'd by pinned Kani (`d4df833`) — it emits "not currently
+// supported". Volatility is a reordering/observability property; the
+// memory-safety contract matches `copy` / `copy_nonoverlapping` /
+// `write_bytes` / `read_unaligned` / `write_unaligned`. Wrappers implement
+// those stores/loads so the safety contract is machine-checked. See the PR
+// for the correspondence.
+// ---------------------------------------------------------------------------
+
+#[requires(ub_checks::can_dereference(src))]
+unsafe fn volatile_load_wrapper<T>(src: *const T) -> T {
+    unsafe { volatile_load(src) }
+}
+
+#[requires(ub_checks::can_write(dst))]
+#[ensures(|_| ub_checks::can_dereference(dst))]
+#[kani::modifies(dst)]
+unsafe fn volatile_store_wrapper<T>(dst: *mut T, val: T) {
+    unsafe { volatile_store(dst, val) }
+}
+
+#[requires(
+    src_readable(src, count)
+        && dst_writable(dst, count)
+        && ub_checks::maybe_is_nonoverlapping(src as *const (), dst as *const (), size_of::<T>(), count)
+)]
+#[ensures(|_| check_copy_untyped(src, dst, count))]
+#[kani::modifies(ptr::slice_from_raw_parts(dst, count))]
+unsafe fn volatile_copy_nonoverlapping_memory_wrapper<T>(dst: *mut T, src: *const T, count: usize) {
+    // Safety-equivalent model (see module comment).
+    unsafe { copy_nonoverlapping(src, dst, count) }
+}
+
+#[requires(src_readable(src, count) && dst_writable(dst, count))]
+#[kani::modifies(ptr::slice_from_raw_parts(dst, count))]
+unsafe fn volatile_copy_memory_wrapper<T>(dst: *mut T, src: *const T, count: usize) {
+    unsafe { copy(src, dst, count) }
+}
+
+#[requires(dst_writable(dst, count))]
+#[kani::modifies(ptr::slice_from_raw_parts(dst, count))]
+unsafe fn volatile_set_memory_wrapper<T>(dst: *mut T, val: u8, count: usize) {
+    unsafe { write_bytes(dst, val, count) }
+}
+
+#[requires(ub_checks::can_read_unaligned(src))]
+unsafe fn unaligned_volatile_load_wrapper<T>(src: *const T) -> T {
+    unsafe { ptr::read_unaligned(src) }
+}
+
+#[requires(ub_checks::can_write_unaligned(dst))]
+#[kani::modifies(dst)]
+unsafe fn unaligned_volatile_store_wrapper<T>(dst: *mut T, val: T) {
+    unsafe { ptr::write_unaligned(dst, val) }
+}
+
+// ---------------------------------------------------------------------------
+// compare_bytes
+//
+// Documented: `left` and `right` valid for reads of `bytes` bytes (the whole
+// range, not only until the first difference). The return sign is the
+// lexicographic unsigned-byte order; the magnitude is unspecified.
+// ---------------------------------------------------------------------------
+
+#[requires(
+    ub_checks::can_dereference(ptr::slice_from_raw_parts(left, bytes))
+        && ub_checks::can_dereference(ptr::slice_from_raw_parts(right, bytes))
+)]
+#[ensures(|result| match compare_bytes_ord(left, right, bytes) {
+    crate::cmp::Ordering::Equal => *result == 0,
+    crate::cmp::Ordering::Less => *result < 0,
+    crate::cmp::Ordering::Greater => *result > 0,
+})]
+unsafe fn compare_bytes_wrapper(left: *const u8, right: *const u8, bytes: usize) -> i32 {
+    unsafe { compare_bytes(left, right, bytes) }
+}
+
+// ---------------------------------------------------------------------------
+// ptr_offset_from / ptr_offset_from_unsigned
+//
+// Documented (`<*const T>::offset_from`): same allocation, distance a multiple
+// of `size_of::<T>()`, no `isize` overflow; unsigned form also requires
+// `ptr >= base`. Fixtures below derive both pointers from one array so the
+// same-allocation conjunct is true; a cross-allocation call is language UB
+// and is not executed here (it would be a failing harness).
+// ---------------------------------------------------------------------------
+
+#[requires(
+    size_of::<T>() > 0
+        && (ptr as isize).checked_sub(base as isize).is_some()
+        && (ptr as isize - base as isize) % (size_of::<T>() as isize) == 0
+        && (ptr as isize == base as isize || ub_checks::same_allocation(ptr, base))
+)]
+#[ensures(|result| {
+    *result == (ptr as isize - base as isize) / (size_of::<T>() as isize)
+})]
+unsafe fn ptr_offset_from_wrapper<T>(ptr: *const T, base: *const T) -> isize {
+    unsafe { ptr_offset_from(ptr, base) }
+}
+
+#[requires(
+    size_of::<T>() > 0
+        && (ptr as usize) >= (base as usize)
+        && (ptr as usize - base as usize) % size_of::<T>() == 0
+        && (ptr as usize == base as usize || ub_checks::same_allocation(ptr, base))
+)]
+#[ensures(|result| *result == (ptr as usize - base as usize) / size_of::<T>())]
+unsafe fn ptr_offset_from_unsigned_wrapper<T>(ptr: *const T, base: *const T) -> usize {
+    unsafe { ptr_offset_from_unsigned(ptr, base) }
+}
+
+// ---------------------------------------------------------------------------
+// read_via_copy / write_via_move  (used by ptr::read / ptr::write)
+// ---------------------------------------------------------------------------
+
+#[requires(ub_checks::can_dereference(ptr))]
+unsafe fn read_via_copy_wrapper<T>(ptr: *const T) -> T {
+    unsafe { read_via_copy(ptr) }
+}
+
+#[requires(ub_checks::can_write(ptr))]
+#[ensures(|_| ub_checks::can_dereference(ptr))]
+#[kani::modifies(ptr)]
+unsafe fn write_via_move_wrapper<T>(ptr: *mut T, value: T) {
+    unsafe { write_via_move(ptr, value) }
+}
+
+// ===========================================================================
+// Harnesses
+// ===========================================================================
+
+#[kani::proof_for_contract(typed_swap_fallback_wrapper)]
+fn check_typed_swap_fallback_u8() {
+    let mut x: u8 = kani::any();
+    let mut y: u8 = kani::any();
+    unsafe { typed_swap_fallback_wrapper(&mut x, &mut y) }
+    kani::cover(true, "typed_swap fallback reached");
+}
+
+#[kani::proof_for_contract(vtable_size_wrapper)]
+fn check_vtable_size_u32() {
+    let x: u32 = kani::any();
+    let fat: &dyn Probe = &x;
+    let size = unsafe { vtable_size_wrapper(vtable_ptr(fat)) };
+    assert_eq!(size, size_of::<u32>());
+    kani::cover(size == 4, "u32 vtable size");
+}
+
+#[kani::proof_for_contract(vtable_size_wrapper)]
+fn check_vtable_size_u8_array() {
+    let x: [u8; 8] = kani::any();
+    let fat: &dyn Probe = &x;
+    let size = unsafe { vtable_size_wrapper(vtable_ptr(fat)) };
+    assert_eq!(size, 8);
+    kani::cover(size == 8, "[u8; 8] vtable size is not size_of::<u32>()");
+}
+
+#[kani::proof_for_contract(vtable_size_wrapper)]
+fn check_vtable_size_zst() {
+    let x = ();
+    let fat: &dyn Probe = &x;
+    let size = unsafe { vtable_size_wrapper(vtable_ptr(fat)) };
+    assert_eq!(size, 0);
+    kani::cover(size == 0, "ZST vtable size");
+}
+
+#[kani::proof_for_contract(vtable_align_wrapper)]
+fn check_vtable_align_u32() {
+    let x: u32 = kani::any();
+    let fat: &dyn Probe = &x;
+    let align = unsafe { vtable_align_wrapper(vtable_ptr(fat)) };
+    assert_eq!(align, align_of::<u32>());
+    kani::cover(align == 4, "u32 vtable align");
+}
+
+#[kani::proof_for_contract(vtable_align_wrapper)]
+fn check_vtable_align_u8() {
+    let x: u8 = kani::any();
+    let fat: &dyn Probe = &x;
+    let align = unsafe { vtable_align_wrapper(vtable_ptr(fat)) };
+    assert_eq!(align, 1);
+    kani::cover(align == 1, "u8 vtable align is not 4");
+}
+
+#[kani::proof_for_contract(copy_wrapper)]
+fn check_copy_nonoverlapping_regions_u8() {
+    let src: [u8; 4] = kani::any();
+    let mut dst: [u8; 4] = kani::any();
+    let count = kani::any_where(|c: &usize| *c <= 4);
+    unsafe { copy_wrapper(src.as_ptr(), dst.as_mut_ptr(), count) }
+    kani::cover(count > 0, "copy count > 0");
+}
+
+#[kani::proof_for_contract(copy_wrapper)]
+fn check_copy_overlapping_shift_u8() {
+    // Representative overlap (not all shifts). Symbolic `count` with a
+    // symbolic shift does not converge; this is the same bound used for
+    // `copy` overlap in the challenge write-up.
+    const SHIFT: usize = 2;
+    let mut buf: [u8; 8] = kani::any();
+    let count = 4;
+    unsafe { copy_wrapper(buf.as_ptr(), buf.as_mut_ptr().add(SHIFT), count) }
+    kani::cover(true, "overlapping copy");
+}
+
+#[kani::proof_for_contract(copy_nonoverlapping_wrapper)]
+fn check_copy_nonoverlapping_u8() {
+    let src: [u8; 4] = kani::any();
+    let mut dst: [u8; 4] = kani::any();
+    let count = kani::any_where(|c: &usize| *c <= 4);
+    unsafe { copy_nonoverlapping_wrapper(src.as_ptr(), dst.as_mut_ptr(), count) }
+    if count > 0 {
+        let i = kani::any_where(|i: &usize| *i < count);
+        assert_eq!(dst[i], src[i]);
+    }
+    kani::cover(count > 0, "copy_nonoverlapping count > 0");
+}
+
+#[kani::proof_for_contract(copy_nonoverlapping_wrapper)]
+fn check_copy_nonoverlapping_zero_count() {
+    // `count == 0` is a no-op. Language-safe dangling dst is rejected by
+    // CBMC `modifies` (kani#90); use a live allocation.
+    let src: [u8; 1] = kani::any();
+    let mut dst: [u8; 1] = kani::any();
+    unsafe { copy_nonoverlapping_wrapper(src.as_ptr(), dst.as_mut_ptr(), 0) }
+    kani::cover(true, "zero-count copy_nonoverlapping");
+}
+
+#[kani::proof_for_contract(write_bytes_wrapper)]
+fn check_write_bytes_u8() {
+    let mut dst: [u8; 4] = kani::any();
+    let val: u8 = kani::any();
+    let count = kani::any_where(|c: &usize| *c <= 4);
+    unsafe { write_bytes_wrapper(dst.as_mut_ptr(), val, count) }
+    if count > 0 {
+        let i = kani::any_where(|i: &usize| *i < count);
+        assert_eq!(dst[i], val);
+    }
+    kani::cover(count > 0, "write_bytes count > 0");
+}
+
+#[kani::proof_for_contract(write_bytes_wrapper)]
+fn check_write_bytes_zero_count() {
+    // `count == 0` is a no-op. Language-safe dangling dst is rejected by
+    // CBMC `modifies` (kani#90); use a live allocation.
+    let mut dst: [u8; 1] = kani::any();
+    unsafe { write_bytes_wrapper(dst.as_mut_ptr(), kani::any(), 0) }
+    kani::cover(true, "zero-count write_bytes");
+}
+
+#[kani::proof_for_contract(size_of_val_sized_wrapper)]
+fn check_size_of_val_sized_u32() {
+    let x: u32 = kani::any();
+    // Documented: always safe for Sized, including null.
+    let ptr = if kani::any() { &x as *const u32 } else { ptr::null() };
+    let size = unsafe { size_of_val_sized_wrapper(ptr) };
+    assert_eq!(size, 4);
+    kani::cover(ptr.is_null(), "size_of_val on null Sized pointer");
+}
+
+#[kani::proof_for_contract(size_of_val_slice_wrapper)]
+fn check_size_of_val_slice_u8() {
+    let buf: [u8; 4] = kani::any();
+    let len = kani::any_where(|l: &usize| *l <= 4);
+    let ptr = ptr::slice_from_raw_parts(buf.as_ptr(), len);
+    let size = unsafe { size_of_val_slice_wrapper::<u8>(ptr) };
+    assert_eq!(size, len);
+    kani::cover(len == 0, "empty slice size_of_val");
+}
+
+#[kani::proof_for_contract(size_of_val_slice_wrapper)]
+fn check_size_of_val_slice_len_zero_dangling() {
+    let ptr = ptr::slice_from_raw_parts(ptr::NonNull::<u8>::dangling().as_ptr(), 0);
+    let size = unsafe { size_of_val_slice_wrapper::<u8>(ptr) };
+    assert_eq!(size, 0);
+    kani::cover(true, "dangling empty slice");
+}
+
+#[kani::proof_for_contract(size_of_val_dyn_wrapper)]
+fn check_size_of_val_dyn_u32() {
+    let x: u32 = kani::any();
+    let fat: &dyn Probe = &x;
+    let size = unsafe { size_of_val_dyn_wrapper(fat) };
+    assert_eq!(size, size_of::<u32>());
+    kani::cover(true, "dyn size_of_val");
+}
+
+#[kani::proof_for_contract(size_of_val_dyn_wrapper)]
+fn check_size_of_val_dyn_array() {
+    let x: [u8; 8] = kani::any();
+    let fat: &dyn Probe = &x;
+    let size = unsafe { size_of_val_dyn_wrapper(fat) };
+    assert_eq!(size, 8);
+    kani::cover(true, "dyn size_of_val of [u8; 8]");
+}
+
+#[kani::proof_for_contract(align_of_val_sized_wrapper)]
+fn check_align_of_val_sized_u32() {
+    let ptr = ptr::null::<u32>();
+    let align = unsafe { align_of_val_sized_wrapper(ptr) };
+    assert_eq!(align, 4);
+    kani::cover(true, "align_of_val Sized null");
+}
+
+#[kani::proof_for_contract(align_of_val_slice_wrapper)]
+fn check_align_of_val_slice_u32() {
+    let buf: [u32; 2] = kani::any();
+    let len = kani::any_where(|l: &usize| *l <= 2);
+    let ptr = ptr::slice_from_raw_parts(buf.as_ptr(), len);
+    let align = unsafe { align_of_val_slice_wrapper::<u32>(ptr) };
+    assert_eq!(align, 4);
+    kani::cover(true, "align_of_val slice");
+}
+
+#[kani::proof_for_contract(align_of_val_dyn_wrapper)]
+fn check_align_of_val_dyn_u8() {
+    let x: u8 = kani::any();
+    let fat: &dyn Probe = &x;
+    let align = unsafe { align_of_val_dyn_wrapper(fat) };
+    assert_eq!(align, 1);
+    kani::cover(align == 1, "dyn align of u8");
+}
+
+#[kani::proof_for_contract(arith_offset_wrapper)]
+fn check_arith_offset_in_object_u8() {
+    let buf: [u8; 8] = kani::any();
+    let offset: isize = kani::any();
+    let dst = buf.as_ptr();
+    let result = unsafe { arith_offset_wrapper(dst, offset) };
+    kani::cover(true, "in-object arith_offset");
+    let _ = (result, dst);
+}
+
+/// Criterion-5 safety is unconditional: `arith_offset` has an empty documented
+/// precondition. This is not `proof_for_contract` — the wrapping-address
+/// `#[ensures]` is only CBMC-faithful in-object (see wrapper comment).
+#[kani::proof]
+fn check_arith_offset_unbounded_no_ub() {
+    let x: u32 = kani::any();
+    let offset: isize = kani::any();
+    let dst = &x as *const u32;
+    let result = unsafe { arith_offset(dst, offset) };
+    kani::cover(offset < 0, "negative unbounded arith_offset");
+    let _ = result;
+}
+
+#[kani::proof_for_contract(volatile_load_wrapper)]
+fn check_volatile_load_u32() {
+    let x: u32 = kani::any();
+    let y = unsafe { volatile_load_wrapper(&x as *const u32) };
+    assert_eq!(x, y);
+    kani::cover(true, "volatile_load");
+}
+
+#[kani::proof_for_contract(volatile_store_wrapper)]
+fn check_volatile_store_u32() {
+    let mut dst: u32 = kani::any();
+    let val: u32 = kani::any();
+    unsafe { volatile_store_wrapper(&mut dst, val) }
+    assert_eq!(dst, val);
+    kani::cover(true, "volatile_store");
+}
+
+#[kani::proof_for_contract(volatile_copy_nonoverlapping_memory_wrapper)]
+fn check_volatile_copy_nonoverlapping_u8() {
+    let src: [u8; 4] = kani::any();
+    let mut dst: [u8; 4] = kani::any();
+    let count = kani::any_where(|c: &usize| *c <= 4);
+    unsafe { volatile_copy_nonoverlapping_memory_wrapper(dst.as_mut_ptr(), src.as_ptr(), count) }
+    if count > 0 {
+        let i = kani::any_where(|i: &usize| *i < count);
+        assert_eq!(dst[i], src[i]);
+    }
+    kani::cover(count > 0, "volatile_copy_nonoverlapping");
+}
+
+#[kani::proof_for_contract(volatile_copy_memory_wrapper)]
+fn check_volatile_copy_memory_shift_u8() {
+    const SHIFT: usize = 2;
+    let mut buf: [u8; 8] = kani::any();
+    unsafe { volatile_copy_memory_wrapper(buf.as_mut_ptr().add(SHIFT), buf.as_ptr(), 4) }
+    kani::cover(true, "volatile_copy_memory representative overlap");
+}
+
+#[kani::proof_for_contract(volatile_set_memory_wrapper)]
+fn check_volatile_set_memory_u8() {
+    let mut dst: [u8; 4] = kani::any();
+    let val: u8 = kani::any();
+    let count = kani::any_where(|c: &usize| *c <= 4);
+    unsafe { volatile_set_memory_wrapper(dst.as_mut_ptr(), val, count) }
+    if count > 0 {
+        let i = kani::any_where(|i: &usize| *i < count);
+        assert_eq!(dst[i], val);
+    }
+    kani::cover(count > 0, "volatile_set_memory");
+}
+
+#[kani::proof_for_contract(unaligned_volatile_load_wrapper)]
+fn check_unaligned_volatile_load_u32() {
+    let bytes: [u8; 8] = kani::any();
+    let offset = kani::any_where(|o: &usize| *o <= 4);
+    let ptr = unsafe { bytes.as_ptr().add(offset) as *const u32 };
+    let _v = unsafe { unaligned_volatile_load_wrapper(ptr) };
+    kani::cover(offset % 4 != 0, "unaligned volatile load");
+}
+
+#[kani::proof_for_contract(unaligned_volatile_store_wrapper)]
+fn check_unaligned_volatile_store_u32() {
+    let mut bytes: [u8; 8] = kani::any();
+    let offset = kani::any_where(|o: &usize| *o <= 4);
+    let ptr = unsafe { bytes.as_mut_ptr().add(offset) as *mut u32 };
+    let val: u32 = kani::any();
+    unsafe { unaligned_volatile_store_wrapper(ptr, val) }
+    kani::cover(offset % 4 != 0, "unaligned volatile store");
+}
+
+#[kani::proof_for_contract(compare_bytes_wrapper)]
+#[kani::unwind(5)]
+fn check_compare_bytes() {
+    let left: [u8; 4] = kani::any();
+    let right: [u8; 4] = kani::any();
+    // Cap is a harness bound, not a contract precondition.
+    let bytes = kani::any_where(|b: &usize| *b <= 4);
+    let cmp = unsafe { compare_bytes_wrapper(left.as_ptr(), right.as_ptr(), bytes) };
+    match compare_bytes_ord(left.as_ptr(), right.as_ptr(), bytes) {
+        crate::cmp::Ordering::Equal => assert_eq!(cmp, 0),
+        crate::cmp::Ordering::Less => assert!(cmp < 0),
+        crate::cmp::Ordering::Greater => assert!(cmp > 0),
+    }
+    kani::cover(bytes > 0 && cmp != 0, "compare_bytes unequal");
+}
+
+#[kani::proof_for_contract(ptr_offset_from_wrapper)]
+fn check_ptr_offset_from_same_alloc() {
+    let buf: [u8; 8] = kani::any();
+    let i = kani::any_where(|i: &usize| *i <= 8);
+    let j = kani::any_where(|j: &usize| *j <= 8);
+    let ptr = unsafe { buf.as_ptr().add(i) };
+    let base = unsafe { buf.as_ptr().add(j) };
+    let off = unsafe { ptr_offset_from_wrapper(ptr, base) };
+    assert_eq!(off, i as isize - j as isize);
+    kani::cover(i < j, "negative ptr_offset_from");
+}
+
+#[kani::proof_for_contract(ptr_offset_from_unsigned_wrapper)]
+fn check_ptr_offset_from_unsigned_same_alloc() {
+    let buf: [u8; 8] = kani::any();
+    let i = kani::any_where(|i: &usize| *i <= 8);
+    let j = kani::any_where(|j: &usize| *j <= i);
+    let ptr = unsafe { buf.as_ptr().add(i) };
+    let base = unsafe { buf.as_ptr().add(j) };
+    let off = unsafe { ptr_offset_from_unsigned_wrapper(ptr, base) };
+    assert_eq!(off, i - j);
+    kani::cover(i > j, "strictly positive unsigned offset");
+}
+
+#[kani::proof_for_contract(read_via_copy_wrapper)]
+fn check_read_via_copy_u32() {
+    let x: u32 = kani::any();
+    let y = unsafe { read_via_copy_wrapper(&x as *const u32) };
+    assert_eq!(x, y);
+    kani::cover(true, "read_via_copy");
+}
+
+#[kani::proof_for_contract(write_via_move_wrapper)]
+fn check_write_via_move_u32() {
+    let mut dst: u32 = kani::any();
+    let val: u32 = kani::any();
+    unsafe { write_via_move_wrapper(&mut dst, val) }
+    assert_eq!(dst, val);
+    kani::cover(true, "write_via_move");
+}
diff --git a/library/core/src/mem/maybe_uninit.rs b/library/core/src/mem/maybe_uninit.rs
index 3507d1a0a9a8c..b9496f5be0187 100644
--- a/library/core/src/mem/maybe_uninit.rs
+++ b/library/core/src/mem/maybe_uninit.rs
@@ -1,5 +1,7 @@
 use crate::any::type_name;
 use crate::clone::TrivialClone;
+#[cfg(kani)]
+use crate::kani;
 use crate::marker::Destruct;
 use crate::mem::ManuallyDrop;
 use crate::{fmt, intrinsics, ptr, slice};
@@ -1614,3 +1616,31 @@ impl<T: TrivialClone> SpecFill<T> for [MaybeUninit<T>] {
         self.fill_with(|| MaybeUninit::new(unsafe { ptr::read(&value) }));
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use safety::ensures;
+
+    use super::*;
+    use crate::kani;
+
+    /// `MaybeUninit::zeroed` is safe; this wrapper states the integer postcondition
+    /// (`write_bytes(0, 1)` of a `u32`).
+    #[ensures(|result| *result == 0)]
+    fn zeroed_u32() -> u32 {
+        unsafe { MaybeUninit::<u32>::zeroed().assume_init() }
+    }
+
+    #[kani::proof_for_contract(zeroed_u32)]
+    fn check_zeroed_u32() {
+        let z = zeroed_u32();
+        assert_eq!(z, 0);
+    }
+
+    #[kani::proof]
+    fn check_zeroed_u8() {
+        let z = unsafe { MaybeUninit::<u8>::zeroed().assume_init() };
+        assert_eq!(z, 0);
+    }
+}
diff --git a/library/core/src/mem/mod.rs b/library/core/src/mem/mod.rs
index eb235cbf10147..213a750227b94 100644
--- a/library/core/src/mem/mod.rs
+++ b/library/core/src/mem/mod.rs
@@ -1529,4 +1529,47 @@ mod verify {
         forget(x);
         forget(y);
     }
+
+    #[kani::proof_for_contract(swap)]
+    pub fn check_swap_exchanges_u8() {
+        let mut x: u8 = kani::any();
+        let mut y: u8 = kani::any();
+        let (a, b) = (x, y);
+        swap(&mut x, &mut y);
+        assert_eq!(x, b);
+        assert_eq!(y, a);
+    }
+
+    #[kani::proof]
+    fn check_align_of_val_u32() {
+        let x: u32 = kani::any();
+        assert_eq!(align_of_val(&x), 4);
+    }
+
+    #[kani::proof]
+    fn check_align_of_val_slice_u8() {
+        let buf: [u8; 4] = kani::any();
+        let s = kani::slice::any_slice_of_array(&buf);
+        assert_eq!(align_of_val(s), 1);
+    }
+
+    #[allow(deprecated)]
+    #[kani::proof]
+    fn check_min_align_of_val_u32() {
+        let x: u32 = kani::any();
+        assert_eq!(min_align_of_val(&x), align_of::<u32>());
+    }
+
+    #[kani::proof]
+    fn check_size_of_val_u32() {
+        let x: u32 = kani::any();
+        assert_eq!(size_of_val(&x), 4);
+    }
+
+    #[kani::proof]
+    fn check_size_of_val_slice() {
+        let buf: [u8; 4] = kani::any();
+        let s = kani::slice::any_slice_of_array(&buf);
+        assert_eq!(size_of_val(s), s.len());
+    }
 }
diff --git a/library/core/src/ptr/mod.rs b/library/core/src/ptr/mod.rs
index 52556a7019014..4e702697bae2e 100644
--- a/library/core/src/ptr/mod.rs
+++ b/library/core/src/ptr/mod.rs
@@ -401,6 +401,8 @@
 // There are many unsafe functions taking pointers that don't dereference them.
 #![allow(clippy::not_unsafe_ptr_arg_deref)]
 
+use safety::requires;
+
 use crate::cmp::Ordering;
 use crate::intrinsics::const_eval_select;
 #[cfg(kani)]
@@ -525,6 +527,32 @@ mod mut_ptr;
 #[inline(always)]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
 #[rustc_diagnostic_item = "ptr_copy_nonoverlapping"]
+#[requires(
+    !count.overflowing_mul(size_of::<T>()).1
+        && ub_checks::maybe_is_aligned_and_not_null(
+            src as *const (),
+            align_of::<T>(),
+            T::IS_ZST || count == 0,
+        )
+        && ub_checks::maybe_is_aligned_and_not_null(
+            dst as *const (),
+            align_of::<T>(),
+            T::IS_ZST || count == 0,
+        )
+        && (count == 0
+            || ub_checks::can_dereference(slice_from_raw_parts(
+                src as *const MaybeUninit<T>,
+                count,
+            )))
+        && (count == 0 || ub_checks::can_write(slice_from_raw_parts_mut(dst, count)))
+        && ub_checks::maybe_is_nonoverlapping(
+            src as *const (),
+            dst as *const (),
+            size_of::<T>(),
+            count,
+        )
+)]
+#[cfg_attr(kani, kani::modifies(slice_from_raw_parts(dst, count)))]
 pub const unsafe fn copy_nonoverlapping<T>(src: *const T, dst: *mut T, count: usize) {
     ub_checks::assert_unsafe_precondition!(
         check_language_ub,
@@ -622,6 +650,26 @@ pub const unsafe fn copy_nonoverlapping<T>(src: *const T, dst: *mut T, count: us
 #[inline(always)]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
 #[rustc_diagnostic_item = "ptr_copy"]
+#[requires(
+    !count.overflowing_mul(size_of::<T>()).1
+        && ub_checks::maybe_is_aligned_and_not_null(
+            src as *const (),
+            align_of::<T>(),
+            T::IS_ZST || count == 0,
+        )
+        && ub_checks::maybe_is_aligned_and_not_null(
+            dst as *const (),
+            align_of::<T>(),
+            T::IS_ZST || count == 0,
+        )
+        && (count == 0
+            || ub_checks::can_dereference(slice_from_raw_parts(
+                src as *const MaybeUninit<T>,
+                count,
+            )))
+        && (count == 0 || ub_checks::can_write(slice_from_raw_parts_mut(dst, count)))
+)]
+#[cfg_attr(kani, kani::modifies(slice_from_raw_parts(dst, count)))]
 pub const unsafe fn copy<T>(src: *const T, dst: *mut T, count: usize) {
     // SAFETY: the safety contract for `copy` must be upheld by the caller.
     unsafe {
@@ -696,6 +744,16 @@ pub const unsafe fn copy<T>(src: *const T, dst: *mut T, count: usize) {
 #[inline(always)]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
 #[rustc_diagnostic_item = "ptr_write_bytes"]
+#[requires(
+    !count.overflowing_mul(size_of::<T>()).1
+        && ub_checks::maybe_is_aligned_and_not_null(
+            dst as *const (),
+            align_of::<T>(),
+            T::IS_ZST || count == 0,
+        )
+        && (count == 0 || ub_checks::can_write(slice_from_raw_parts_mut(dst, count)))
+)]
+#[cfg_attr(kani, kani::modifies(slice_from_raw_parts(dst, count)))]
 pub const unsafe fn write_bytes<T>(dst: *mut T, val: u8, count: usize) {
     // SAFETY: the safety contract for `write_bytes` must be upheld by the caller.
     unsafe {
@@ -1296,6 +1354,10 @@ pub const fn slice_from_raw_parts_mut<T>(data: *mut T, len: usize) -> *mut [T] {
 #[stable(feature = "rust1", since = "1.0.0")]
 #[rustc_const_stable(feature = "const_swap", since = "1.85.0")]
 #[rustc_diagnostic_item = "ptr_swap"]
+#[requires(ub_checks::can_dereference(x) && ub_checks::can_write(x))]
+#[requires(ub_checks::can_dereference(y) && ub_checks::can_write(y))]
+#[cfg_attr(kani, kani::modifies(x))]
+#[cfg_attr(kani, kani::modifies(y))]
 pub const unsafe fn swap<T>(x: *mut T, y: *mut T) {
     // Give ourselves some scratch space to work with.
     // We do not have to worry about drops: `MaybeUninit` does nothing when dropped.
@@ -2798,6 +2860,63 @@ mod verify {
         assert_eq!(val, copy);
     }
 
+    #[kani::proof_for_contract(copy_nonoverlapping)]
+    fn check_ptr_copy_nonoverlapping_u8() {
+        let src: [u8; 4] = kani::any();
+        let mut dst: [u8; 4] = kani::any();
+        let count = kani::any_where(|c: &usize| *c <= 4);
+        unsafe { copy_nonoverlapping(src.as_ptr(), dst.as_mut_ptr(), count) }
+        if count > 0 {
+            let i = kani::any_where(|i: &usize| *i < count);
+            assert_eq!(dst[i], src[i]);
+        }
+    }
+
+    #[kani::proof_for_contract(copy)]
+    fn check_ptr_copy_u8() {
+        let src: [u8; 4] = kani::any();
+        let mut dst: [u8; 4] = kani::any();
+        let count = kani::any_where(|c: &usize| *c <= 4);
+        unsafe { copy(src.as_ptr(), dst.as_mut_ptr(), count) }
+    }
+
+    #[kani::proof_for_contract(write_bytes)]
+    fn check_ptr_write_bytes_u8() {
+        let mut dst: [u8; 4] = kani::any();
+        let val: u8 = kani::any();
+        let count = kani::any_where(|c: &usize| *c <= 4);
+        unsafe { write_bytes(dst.as_mut_ptr(), val, count) }
+        if count > 0 {
+            let i = kani::any_where(|i: &usize| *i < count);
+            assert_eq!(dst[i], val);
+        }
+    }
+
+    #[kani::proof_for_contract(swap)]
+    fn check_ptr_swap_u8() {
+        let mut x: u8 = kani::any();
+        let mut y: u8 = kani::any();
+        let (a, b) = (x, y);
+        unsafe { swap(&mut x, &mut y) }
+        assert_eq!(x, b);
+        assert_eq!(y, a);
+    }
+
+    #[kani::proof]
+    fn check_ptr_read_u32() {
+        let x: u32 = kani::any();
+        let y = unsafe { read(&x) };
+        assert_eq!(x, y);
+    }
+
+    #[kani::proof]
+    fn check_ptr_write_u32() {
+        let mut dst: u32 = kani::any();
+        let val: u32 = kani::any();
+        unsafe { write(&mut dst, val) }
+        assert_eq!(dst, val);
+    }
+
     fn check_align_offset<T>(p: *const T) {
         let a = kani::any::<usize>();
         unsafe { align_offset(p, a) };
diff --git a/library/core/src/slice/mod.rs b/library/core/src/slice/mod.rs
index 8e19bbdca0cd4..b6ca8bd9459d1 100644
--- a/library/core/src/slice/mod.rs
+++ b/library/core/src/slice/mod.rs
@@ -3898,6 +3898,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,
@@ -5556,4 +5558,12 @@ mod verify {
         let mut a: [u8; 100] = kani::any();
         a.reverse();
     }
+
+    #[kani::proof_for_contract(<[u8]>::copy_from_slice)]
+    fn check_copy_from_slice_u8() {
+        let src: [u8; 4] = kani::any();
+        let mut dst: [u8; 4] = kani::any();
+        dst.copy_from_slice(&src);
+        assert_eq!(dst, src);
+    }
 }