diff --git a/library/alloc/src/boxed.rs b/library/alloc/src/boxed.rs
index f426345f9fc62..98109f479981c 100644
--- a/library/alloc/src/boxed.rs
+++ b/library/alloc/src/boxed.rs
@@ -190,6 +190,8 @@ use core::error::{self, Error};
 use core::fmt;
 use core::future::Future;
 use core::hash::{Hash, Hasher};
+#[cfg(kani)]
+use core::kani;
 use core::marker::{PhantomData, Tuple, Unsize};
 #[cfg(not(no_global_oom_handling))]
 use core::mem::MaybeUninit;
@@ -203,6 +205,23 @@ use core::ops::{Residual, Try};
 use core::pin::{Pin, PinSafePointer};
 use core::ptr::{self, NonNull};
 use core::task::{Context, Poll};
+#[cfg(kani)]
+use core::ub_checks;
+
+use safety::{ensures, requires};
+
+/// Kani-only: documented Box raw-pointer layout besides “valid `T`”.
+/// `can_dereference` covers alignment and the allocation; Box also forbids size > `isize::MAX`.
+/// Kani checks initialization only under `-Z uninit-checks`, which CI does not pass, so
+/// initialization stays a caller obligation, as does allocator provenance, which we cannot express.
+#[cfg(kani)]
+fn box_ptr_fits_box_layout<T: ?Sized>(ptr: *const T) -> bool {
+    ub_checks::can_dereference(ptr) && {
+        // SAFETY: `can_dereference` means `ptr` is a valid `T`, so size/align exist.
+        let layout = unsafe { Layout::for_value_raw(ptr) };
+        layout.size() <= isize::MAX as usize
+    }
+}
 
 #[cfg(not(no_global_oom_handling))]
 use crate::alloc::handle_alloc_error;
@@ -1276,6 +1295,14 @@ impl<T, A: Allocator> Box<mem::MaybeUninit<T>, A> {
     #[stable(feature = "new_uninit", since = "1.82.0")]
     #[rustc_const_unstable(feature = "const_heap", issue = "79597")]
     #[inline(always)]
+    // TODO: we can no longer attach this contract now that `assume_init` is a `const fn`:
+    // Kani's contract instrumentation fails with E0493 because the destructor of the owned
+    // `Box` receiver cannot be evaluated at compile time, see
+    // https://github.com/model-checking/kani/issues/4984. Until that works, the
+    // `check_assume_init_{i32,zst,bool}` harnesses in `mod verify` assume the precondition
+    // and assert the postcondition around each call.
+    // #[requires(ub_checks::can_dereference((&*self as *const mem::MaybeUninit<T>).cast::<T>()))]
+    // #[ensures(|result| ub_checks::can_dereference(&**result as *const T))]
     pub const unsafe fn assume_init(self) -> Box<T, A> {
         // This is used in the `vec!` macro, so we optimize for minimal IR generation
         // even in debug builds.
@@ -1346,6 +1373,13 @@ impl<T, A: Allocator> Box<[mem::MaybeUninit<T>], A> {
     /// ```
     #[stable(feature = "new_uninit", since = "1.82.0")]
     #[inline]
+    // SAFETY: every element must be a valid `T`. The contract casts `[MaybeUninit<T>]` to
+    // `[T]` and requires `can_dereference`, but Kani checks initialization only under
+    // `-Z uninit-checks`, which CI does not pass, so initialization stays the caller's obligation.
+    #[requires(ub_checks::can_dereference(
+        &*self as *const [mem::MaybeUninit<T>] as *const [T]
+    ))]
+    #[ensures(|result| ub_checks::can_dereference(&**result as *const [T]))]
     pub unsafe fn assume_init(self) -> Box<[T], A> {
         let (raw, alloc) = Box::into_raw_with_allocator(self);
         // SAFETY: Upheld by caller.
@@ -1401,6 +1435,11 @@ impl<T: ?Sized> Box<T> {
     #[stable(feature = "box_raw", since = "1.4.0")]
     #[inline]
     #[must_use = "call `drop(Box::from_raw(ptr))` if you intend to drop the `Box`"]
+    // Memory-layout contract: non-null, aligned, in-bounds, valid `T`,
+    // size ≤ isize::MAX (including ZST dangling pointers).
+    // Provenance/allocator identity is a caller obligation Kani cannot fully express.
+    #[requires(!raw.is_null() && box_ptr_fits_box_layout(raw))]
+    #[ensures(|result| (&**result) as *const T == raw as *const T)]
     pub unsafe fn from_raw(raw: *mut T) -> Self {
         // SAFETY: Upheld by caller.
         unsafe { Self::from_raw_in(raw, Global) }
@@ -1454,6 +1493,8 @@ impl<T: ?Sized> Box<T> {
     #[stable(feature = "box_vec_non_null", since = "1.99.0")]
     #[inline]
     #[must_use = "call `drop(Box::from_non_null(ptr))` if you intend to drop the `Box`"]
+    #[requires(box_ptr_fits_box_layout(ptr.as_ptr()))]
+    #[ensures(|result| (&**result) as *const T == ptr.as_ptr() as *const T)]
     pub unsafe fn from_non_null(ptr: NonNull<T>) -> Self {
         // SAFETY: Upheld by caller.
         unsafe { Self::from_raw(ptr.as_ptr()) }
@@ -1632,6 +1673,8 @@ impl<T: ?Sized, A: Allocator> Box<T, A> {
     /// [considerations for unsafe code]: self#considerations-for-unsafe-code
     #[stable(feature = "allocator_api", since = "1.100.0")]
     #[inline]
+    #[requires(!raw.is_null() && box_ptr_fits_box_layout(raw))]
+    #[ensures(|result| (&**result) as *const T == raw as *const T)]
     pub unsafe fn from_raw_in(raw: *mut T, alloc: A) -> Self {
         // SAFETY: Upheld by caller.
         Box(unsafe { BoxRaw::new_unchecked(raw) }, alloc)
@@ -1685,6 +1728,8 @@ impl<T: ?Sized, A: Allocator> Box<T, A> {
     /// [considerations for unsafe code]: self#considerations-for-unsafe-code
     #[stable(feature = "allocator_api", since = "1.100.0")]
     #[inline]
+    #[requires(box_ptr_fits_box_layout(raw.as_ptr()))]
+    #[ensures(|result| (&**result) as *const T == raw.as_ptr() as *const T)]
     pub unsafe fn from_non_null_in(raw: NonNull<T>, alloc: A) -> Self {
         // SAFETY: guaranteed by the caller.
         unsafe { Box::from_raw_in(raw.as_ptr(), alloc) }
@@ -2625,3 +2670,479 @@ impl<R: core::random::Rng + ?Sized, A: Allocator> core::random::Rng for Box<R, A
         (**self).fill_bytes(bytes)
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    #![allow(missing_docs)]
+
+    use core::marker::PhantomPinned;
+    use core::mem::MaybeUninit;
+    use core::pin::Pin;
+    use core::{kani, ptr};
+
+    use super::*;
+    use crate::alloc::Allocator;
+
+    const SLICE_CAP: usize = 2;
+
+    fn alloc_write<T>(value: T) -> *mut T {
+        let layout = Layout::new::<T>();
+        if layout.size() == 0 {
+            let ptr = NonNull::<T>::dangling().as_ptr();
+            unsafe { ptr::write(ptr, value) };
+            ptr
+        } else {
+            let ptr = Global.allocate(layout).expect("alloc").cast::<T>().as_ptr();
+            unsafe { ptr::write(ptr, value) };
+            ptr
+        }
+    }
+
+    /// Heap-allocate a `[u8]` without `Box::from` / `from_raw_in` (Kani
+    /// `proof_for_contract` allows only one top-level call to the contracted fn).
+    fn alloc_write_slice(data: &[u8]) -> *mut [u8] {
+        let len = data.len();
+        let ptr = if len == 0 {
+            NonNull::<u8>::dangling().as_ptr()
+        } else {
+            let layout = Layout::array::<u8>(len).expect("layout");
+            let ptr = Global.allocate(layout).expect("alloc").cast::<u8>().as_ptr();
+            unsafe { ptr::copy_nonoverlapping(data.as_ptr(), ptr, len) };
+            ptr
+        };
+        ptr::slice_from_raw_parts_mut(ptr, len)
+    }
+
+    /// Shows that the harness reaches both an empty and a full slice.
+    fn cover_slice_len(len: usize) {
+        kani::cover(len == 0, "empty slice");
+        kani::cover(len == SLICE_CAP, "slice of SLICE_CAP elements");
+    }
+
+    /// Shows that the assumed precondition does not rule out every execution.
+    fn cover_reached() {
+        kani::cover(true, "non-vacuity witness: reached with the precondition assumed");
+    }
+
+    // ---- required unsafe: assume_init (sized) ----
+    // `assume_init` is a `const fn` and cannot carry its contract under Kani (see the TODO
+    // on it), so these are plain proofs that mirror the contract: assume the precondition,
+    // call, then assert the postcondition. This follows the `transmute_unchecked` harnesses
+    // in `core::intrinsics::verify`, and `assume_init` is `transmute_unchecked(self)`. Each
+    // slot is written first, so the precondition also holds by construction.
+
+    fn assume_init_mirror<T>(slot: Box<MaybeUninit<T>>) -> Box<T> {
+        kani::assume(ub_checks::can_dereference((&*slot as *const MaybeUninit<T>).cast::<T>()));
+        let boxed = unsafe { slot.assume_init() };
+        assert!(ub_checks::can_dereference(&*boxed as *const T));
+        cover_reached();
+        boxed
+    }
+
+    #[kani::proof]
+    pub fn check_assume_init_i32() {
+        let value: i32 = kani::any();
+        let mut slot: Box<MaybeUninit<i32>> = Box::new_uninit();
+        (*slot).write(value);
+        let boxed = assume_init_mirror(slot);
+        assert!(*boxed == value);
+    }
+
+    #[kani::proof]
+    pub fn check_assume_init_zst() {
+        let mut slot: Box<MaybeUninit<()>> = Box::new_uninit();
+        (*slot).write(());
+        let boxed = assume_init_mirror(slot);
+        assert!(*boxed == ());
+    }
+
+    #[kani::proof]
+    pub fn check_assume_init_bool() {
+        let value: bool = kani::any();
+        let mut slot: Box<MaybeUninit<bool>> = Box::new_uninit();
+        (*slot).write(value);
+        let boxed = assume_init_mirror(slot);
+        assert!(*boxed == value);
+    }
+
+    // ---- required unsafe: assume_init (slice) ----
+
+    #[kani::proof_for_contract(Box::<[core::mem::MaybeUninit<T>], A>::assume_init)]
+    #[kani::unwind(4)]
+    pub fn check_assume_init_slice_u8() {
+        let len = kani::any_where(|n: &usize| *n <= SLICE_CAP);
+        let mut slot: Box<[MaybeUninit<u8>]> = Box::new_uninit_slice(len);
+        for i in 0..len {
+            slot[i].write(kani::any());
+        }
+        let boxed = unsafe { slot.assume_init() };
+        assert!(boxed.len() == len);
+        cover_slice_len(len);
+    }
+
+    #[kani::proof_for_contract(Box::<[core::mem::MaybeUninit<T>], A>::assume_init)]
+    #[kani::unwind(4)]
+    pub fn check_assume_init_slice_i32() {
+        let len = kani::any_where(|n: &usize| *n <= SLICE_CAP);
+        let mut slot: Box<[MaybeUninit<i32>]> = Box::new_uninit_slice(len);
+        for i in 0..len {
+            slot[i].write(kani::any());
+        }
+        let boxed = unsafe { slot.assume_init() };
+        assert!(boxed.len() == len);
+        cover_slice_len(len);
+    }
+
+    // ---- required unsafe: from_raw ----
+
+    #[kani::proof_for_contract(Box::<i32>::from_raw)]
+    pub fn check_from_raw_i32() {
+        let value: i32 = kani::any();
+        let ptr = Box::into_raw(Box::new(value));
+        let boxed = unsafe { Box::from_raw(ptr) };
+        assert!(*boxed == value);
+        cover_reached();
+    }
+
+    #[kani::proof_for_contract(Box::<()>::from_raw)]
+    pub fn check_from_raw_zst() {
+        let ptr = Box::into_raw(Box::new(()));
+        let _boxed = unsafe { Box::from_raw(ptr) };
+        cover_reached();
+    }
+
+    #[kani::proof_for_contract(Box::<[u8]>::from_raw)]
+    pub fn check_from_raw_slice() {
+        let data: [u8; SLICE_CAP] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&data);
+        let boxed: Box<[u8]> = Box::from(slice);
+        let len = boxed.len();
+        let ptr = Box::into_raw(boxed);
+        let boxed = unsafe { Box::<[u8]>::from_raw(ptr) };
+        assert!(boxed.len() == len);
+        cover_slice_len(len);
+    }
+
+    // ---- required unsafe: from_non_null ----
+
+    #[kani::proof_for_contract(Box::<i32>::from_non_null)]
+    pub fn check_from_non_null_i32() {
+        let value: i32 = kani::any();
+        let ptr = Box::into_non_null(Box::new(value));
+        let boxed = unsafe { Box::from_non_null(ptr) };
+        assert!(*boxed == value);
+        cover_reached();
+    }
+
+    #[kani::proof_for_contract(Box::<()>::from_non_null)]
+    pub fn check_from_non_null_zst() {
+        let ptr = Box::into_non_null(Box::new(()));
+        let _boxed = unsafe { Box::from_non_null(ptr) };
+        cover_reached();
+    }
+
+    #[kani::proof_for_contract(Box::<[u8]>::from_non_null)]
+    pub fn check_from_non_null_slice() {
+        let data: [u8; SLICE_CAP] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&data);
+        let boxed: Box<[u8]> = Box::from(slice);
+        let len = boxed.len();
+        let ptr = Box::into_non_null(boxed);
+        let boxed = unsafe { Box::<[u8]>::from_non_null(ptr) };
+        assert!(boxed.len() == len);
+        cover_slice_len(len);
+    }
+
+    // ---- required unsafe: from_raw_in ----
+    // Setup cannot go through Box::new_in / from_raw: those call from_raw_in.
+
+    #[kani::proof_for_contract(Box::<i32, Global>::from_raw_in)]
+    pub fn check_from_raw_in_i32() {
+        let value: i32 = kani::any();
+        let ptr = alloc_write(value);
+        let boxed = unsafe { Box::from_raw_in(ptr, Global) };
+        assert!(*boxed == value);
+        cover_reached();
+    }
+
+    #[kani::proof_for_contract(Box::<(), Global>::from_raw_in)]
+    pub fn check_from_raw_in_zst() {
+        let ptr = alloc_write(());
+        let _boxed = unsafe { Box::from_raw_in(ptr, Global) };
+        cover_reached();
+    }
+
+    #[kani::proof_for_contract(Box::<[u8], Global>::from_raw_in)]
+    pub fn check_from_raw_in_slice() {
+        let data: [u8; SLICE_CAP] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&data);
+        let len = slice.len();
+        let ptr = alloc_write_slice(slice);
+        let boxed = unsafe { Box::from_raw_in(ptr, Global) };
+        assert!(boxed.len() == len);
+        cover_slice_len(len);
+    }
+
+    // ---- required unsafe: from_non_null_in ----
+
+    #[kani::proof_for_contract(Box::<i32, Global>::from_non_null_in)]
+    pub fn check_from_non_null_in_i32() {
+        let value: i32 = kani::any();
+        let ptr = NonNull::new(alloc_write(value)).unwrap();
+        let boxed = unsafe { Box::from_non_null_in(ptr, Global) };
+        assert!(*boxed == value);
+        cover_reached();
+    }
+
+    #[kani::proof_for_contract(Box::<(), Global>::from_non_null_in)]
+    pub fn check_from_non_null_in_zst() {
+        let ptr = NonNull::new(alloc_write(())).unwrap();
+        let _boxed = unsafe { Box::from_non_null_in(ptr, Global) };
+        cover_reached();
+    }
+
+    #[kani::proof_for_contract(Box::<[u8], Global>::from_non_null_in)]
+    pub fn check_from_non_null_in_slice() {
+        let data: [u8; SLICE_CAP] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&data);
+        let len = slice.len();
+        let ptr = NonNull::new(alloc_write_slice(slice)).unwrap();
+        let boxed = unsafe { Box::from_non_null_in(ptr, Global) };
+        assert!(boxed.len() == len);
+        cover_slice_len(len);
+    }
+
+    // ---- safe functions with unsafe bodies ----
+
+    #[kani::proof]
+    pub fn check_new_in() {
+        let value: i32 = kani::any();
+        let boxed = Box::new_in(value, Global);
+        assert!(*boxed == value);
+    }
+
+    #[kani::proof]
+    pub fn check_try_new_in() {
+        let value: u8 = kani::any();
+        let boxed = Box::try_new_in(value, Global).expect("alloc");
+        assert!(*boxed == value);
+    }
+
+    #[kani::proof]
+    pub fn check_try_new_uninit_in() {
+        let value: i32 = kani::any();
+        let mut slot = Box::<i32>::try_new_uninit_in(Global).expect("alloc");
+        (*slot).write(value);
+        let boxed = unsafe { slot.assume_init() };
+        assert!(*boxed == value);
+    }
+
+    #[kani::proof]
+    pub fn check_try_new_zeroed_in() {
+        let slot = Box::<u32>::try_new_zeroed_in(Global).expect("alloc");
+        let boxed = unsafe { slot.assume_init() };
+        assert!(*boxed == 0);
+    }
+
+    #[kani::proof]
+    pub fn check_into_boxed_slice() {
+        let value: i32 = kani::any();
+        let slice = Box::into_boxed_slice(Box::new(value));
+        assert!(slice.len() == 1);
+        assert!(slice[0] == value);
+    }
+
+    #[kani::proof]
+    #[kani::unwind(4)]
+    pub fn check_new_uninit_slice() {
+        let len = kani::any_where(|n: &usize| *n <= SLICE_CAP);
+        let slot: Box<[MaybeUninit<i32>]> = Box::new_uninit_slice(len);
+        assert!(slot.len() == len);
+        cover_slice_len(len);
+    }
+
+    #[kani::proof]
+    #[kani::unwind(4)]
+    pub fn check_new_zeroed_slice() {
+        let len = kani::any_where(|n: &usize| *n <= SLICE_CAP);
+        let slot: Box<[MaybeUninit<u8>]> = Box::new_zeroed_slice(len);
+        let boxed = unsafe { slot.assume_init() };
+        for i in 0..len {
+            assert!(boxed[i] == 0);
+        }
+        cover_slice_len(len);
+    }
+
+    #[kani::proof]
+    #[kani::unwind(4)]
+    pub fn check_try_new_uninit_slice() {
+        let len = kani::any_where(|n: &usize| *n <= SLICE_CAP);
+        let slot = Box::<[i32]>::try_new_uninit_slice(len).expect("alloc");
+        assert!(slot.len() == len);
+        assert!(Box::<[u64]>::try_new_uninit_slice(usize::MAX).is_err());
+        cover_slice_len(len);
+    }
+
+    #[kani::proof]
+    #[kani::unwind(4)]
+    pub fn check_try_new_zeroed_slice() {
+        let len = kani::any_where(|n: &usize| *n <= SLICE_CAP);
+        let slot = Box::<[u8]>::try_new_zeroed_slice(len).expect("alloc");
+        let boxed = unsafe { slot.assume_init() };
+        assert!(boxed.len() == len);
+        for i in 0..len {
+            assert!(boxed[i] == 0);
+        }
+        assert!(Box::<[u64]>::try_new_zeroed_slice(usize::MAX).is_err());
+        cover_slice_len(len);
+    }
+
+    #[kani::proof]
+    pub fn check_into_array() {
+        // One element more than N, so the slice can be shorter or longer than N.
+        let data: [i32; SLICE_CAP + 1] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&data);
+        let boxed: Box<[i32]> = Box::from(slice);
+        let len = boxed.len();
+        kani::cover(len < SLICE_CAP, "slice shorter than N");
+        kani::cover(len == SLICE_CAP, "slice of length N");
+        kani::cover(len > SLICE_CAP, "slice longer than N");
+        match boxed.into_array::<SLICE_CAP>() {
+            Ok(_arr) => assert!(len == SLICE_CAP),
+            Err(_) => assert!(len != SLICE_CAP),
+        }
+    }
+
+    #[kani::proof]
+    #[kani::unwind(4)]
+    pub fn check_new_uninit_slice_in() {
+        let len = kani::any_where(|n: &usize| *n <= SLICE_CAP);
+        let slot: Box<[MaybeUninit<i32>], _> = Box::new_uninit_slice_in(len, Global);
+        assert!(slot.len() == len);
+        cover_slice_len(len);
+    }
+
+    #[kani::proof]
+    #[kani::unwind(4)]
+    pub fn check_new_zeroed_slice_in() {
+        let len = kani::any_where(|n: &usize| *n <= SLICE_CAP);
+        let slot: Box<[MaybeUninit<u8>], _> = Box::new_zeroed_slice_in(len, Global);
+        let boxed = unsafe { slot.assume_init() };
+        assert!(boxed.len() == len);
+        for i in 0..len {
+            assert!(boxed[i] == 0);
+        }
+        cover_slice_len(len);
+    }
+
+    #[kani::proof]
+    #[kani::unwind(4)]
+    pub fn check_try_new_uninit_slice_in() {
+        let len = kani::any_where(|n: &usize| *n <= SLICE_CAP);
+        let slot = Box::<[i32]>::try_new_uninit_slice_in(len, Global).expect("alloc");
+        assert!(slot.len() == len);
+        cover_slice_len(len);
+    }
+
+    #[kani::proof]
+    #[kani::unwind(4)]
+    pub fn check_try_new_zeroed_slice_in() {
+        let len = kani::any_where(|n: &usize| *n <= SLICE_CAP);
+        let slot = Box::<[u8]>::try_new_zeroed_slice_in(len, Global).expect("alloc");
+        assert!(slot.len() == len);
+        cover_slice_len(len);
+    }
+
+    #[kani::proof]
+    pub fn check_write() {
+        let value: i32 = kani::any();
+        let boxed = Box::write(Box::new_uninit(), value);
+        assert!(*boxed == value);
+    }
+
+    #[kani::proof]
+    pub fn check_into_non_null() {
+        let value: i32 = kani::any();
+        let ptr = Box::into_non_null(Box::new(value));
+        let boxed = unsafe { Box::from_non_null(ptr) };
+        assert!(*boxed == value);
+    }
+
+    #[kani::proof]
+    pub fn check_into_raw_with_allocator() {
+        let value: i32 = kani::any();
+        let (ptr, alloc) = Box::into_raw_with_allocator(Box::new_in(value, Global));
+        let boxed = unsafe { Box::from_raw_in(ptr, alloc) };
+        assert!(*boxed == value);
+    }
+
+    #[kani::proof]
+    pub fn check_into_non_null_with_allocator() {
+        let value: bool = kani::any();
+        let (ptr, alloc) = Box::into_non_null_with_allocator(Box::new_in(value, Global));
+        let boxed = unsafe { Box::from_non_null_in(ptr, alloc) };
+        assert!(*boxed == value);
+    }
+
+    #[kani::proof]
+    pub fn check_leak() {
+        let value: i32 = kani::any();
+        let leaked: &'static mut i32 = Box::leak(Box::new(value));
+        assert!(*leaked == value);
+        unsafe { drop(Box::from_raw(leaked as *mut i32)) };
+    }
+
+    #[kani::proof]
+    pub fn check_into_pin_unpin() {
+        let value: i32 = kani::any();
+        let pinned: Pin<Box<i32>> = Box::into_pin(Box::new(value));
+        assert!(*pinned == value);
+    }
+
+    #[kani::proof]
+    pub fn check_into_pin_not_unpin() {
+        struct Pinned(i32, PhantomPinned);
+        let value: i32 = kani::any();
+        let pinned = Box::into_pin(Box::new(Pinned(value, PhantomPinned)));
+        assert!(pinned.0 == value);
+    }
+
+    #[kani::proof]
+    pub fn check_drop_sized() {
+        drop(Box::new(kani::any::<i32>()));
+    }
+
+    #[kani::proof]
+    pub fn check_drop_zst() {
+        drop(Box::new(()));
+    }
+
+    #[kani::proof]
+    pub fn check_default_sized() {
+        let boxed: Box<i32> = Box::default();
+        assert!(*boxed == 0);
+    }
+
+    #[kani::proof]
+    pub fn check_default_str() {
+        let boxed: Box<str> = Box::default();
+        assert!(boxed.is_empty());
+    }
+
+    #[kani::proof]
+    pub fn check_clone_sized() {
+        let value: i32 = kani::any();
+        let boxed = Box::new(value);
+        let cloned = boxed.clone();
+        assert!(*cloned == value);
+        assert!((&*boxed as *const i32) != (&*cloned as *const i32));
+    }
+
+    #[kani::proof]
+    pub fn check_clone_str() {
+        let boxed: Box<str> = Box::from("ab");
+        let cloned = boxed.clone();
+        assert!(&*cloned == &*boxed);
+    }
+}
diff --git a/library/alloc/src/boxed/convert.rs b/library/alloc/src/boxed/convert.rs
index 526e8b18a8031..83bcc3fe1b0d1 100644
--- a/library/alloc/src/boxed/convert.rs
+++ b/library/alloc/src/boxed/convert.rs
@@ -2,8 +2,14 @@ use core::any::Any;
 use core::error::Error;
 #[cfg(not(no_global_oom_handling))]
 use core::fmt;
+#[cfg(kani)]
+use core::kani;
 use core::mem;
 use core::pin::Pin;
+#[cfg(kani)]
+use core::ub_checks;
+
+use safety::{ensures, requires};
 
 use crate::alloc::{Allocator, StaticAllocator};
 #[cfg(not(no_global_oom_handling))]
@@ -245,6 +251,7 @@ impl<T, const N: usize> From<[T; N]> for Box<[T]> {
 /// # Safety
 ///
 /// `boxed_slice.len()` must be exactly `N`.
+#[requires(boxed_slice.len() == N)]
 unsafe fn boxed_slice_as_array_unchecked<T, A: Allocator, const N: usize>(
     boxed_slice: Box<[T], A>,
 ) -> Box<[T; N], A> {
@@ -364,6 +371,8 @@ impl<A: Allocator> Box<dyn Any, A> {
     /// [`downcast`]: Self::downcast
     #[inline]
     #[unstable(feature = "downcast_unchecked", issue = "90850")]
+    #[requires(self.is::<T>())]
+    #[ensures(|result| ub_checks::can_dereference(&**result as *const T))]
     pub unsafe fn downcast_unchecked<T: Any>(self) -> Box<T, A> {
         debug_assert!(self.is::<T>());
         // SAFETY: Caller ensures the type is correct.
@@ -425,6 +434,8 @@ impl<A: Allocator> Box<dyn Any + Send, A> {
     /// [`downcast`]: Self::downcast
     #[inline]
     #[unstable(feature = "downcast_unchecked", issue = "90850")]
+    #[requires(self.is::<T>())]
+    #[ensures(|result| ub_checks::can_dereference(&**result as *const T))]
     pub unsafe fn downcast_unchecked<T: Any>(self) -> Box<T, A> {
         debug_assert!(self.is::<T>());
         // SAFETY: Caller ensures the type is correct.
@@ -486,6 +497,8 @@ impl<A: Allocator> Box<dyn Any + Send + Sync, A> {
     /// [`downcast`]: Self::downcast
     #[inline]
     #[unstable(feature = "downcast_unchecked", issue = "90850")]
+    #[requires(self.is::<T>())]
+    #[ensures(|result| ub_checks::can_dereference(&**result as *const T))]
     pub unsafe fn downcast_unchecked<T: Any>(self) -> Box<T, A> {
         debug_assert!(self.is::<T>());
         // SAFETY: Caller ensures the type is correct.
@@ -755,3 +768,228 @@ impl dyn Error + Send + Sync {
         })
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    #![allow(missing_docs)]
+
+    use core::any::Any;
+    use core::error::Error;
+    use core::{fmt, kani};
+
+    use super::boxed_slice_as_array_unchecked;
+    use crate::boxed::Box;
+    use crate::vec::Vec;
+
+    #[derive(Debug)]
+    struct ProbeError(i32);
+
+    impl fmt::Display for ProbeError {
+        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+            write!(f, "probe")
+        }
+    }
+
+    impl Error for ProbeError {}
+
+    #[derive(Debug)]
+    struct OtherError;
+
+    impl fmt::Display for OtherError {
+        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+            write!(f, "other")
+        }
+    }
+
+    impl Error for OtherError {}
+
+    // Clone but not Copy, so slice conversion exercises element cloning.
+    #[derive(Clone)]
+    struct CloneCell(u8);
+
+    /// Shows that the assumed precondition does not rule out every execution.
+    fn cover_reached() {
+        kani::cover(true, "non-vacuity witness: reached with the precondition assumed");
+    }
+
+    // The challenge table lists `<dyn Error>::downcast_unchecked`. That API
+    // does not exist: unchecked downcast lives on `Box<dyn Any (+ Send) (+ Sync)>`.
+    // Those impls sit in this module rather than in `Box`'s own, and Kani's
+    // contract resolver could not match such out-of-module impls until
+    // model-checking/kani#4778, which the pinned Kani includes. The target paths
+    // use the impl's generic name `A` and fully qualified auto traits, the
+    // spelling that fix matches.
+
+    #[kani::proof_for_contract(Box::<dyn core::any::Any + 'static, A>::downcast_unchecked::<i32>)]
+    pub fn check_downcast_unchecked_any() {
+        let value: i32 = kani::any();
+        let erased: Box<dyn Any> = Box::new(value);
+        let boxed = unsafe { erased.downcast_unchecked::<i32>() };
+        assert!(*boxed == value);
+        cover_reached();
+    }
+
+    #[kani::proof_for_contract(Box::<dyn core::any::Any + core::marker::Send + 'static, A>::downcast_unchecked::<i32>)]
+    pub fn check_downcast_unchecked_any_send() {
+        let value: i32 = kani::any();
+        let erased: Box<dyn Any + Send> = Box::new(value);
+        let boxed = unsafe { erased.downcast_unchecked::<i32>() };
+        assert!(*boxed == value);
+        cover_reached();
+    }
+
+    #[kani::proof_for_contract(Box::<dyn core::any::Any + core::marker::Send + core::marker::Sync + 'static, A>::downcast_unchecked::<bool>)]
+    pub fn check_downcast_unchecked_any_send_sync() {
+        let value: bool = kani::any();
+        let erased: Box<dyn Any + Send + Sync> = Box::new(value);
+        let boxed = unsafe { erased.downcast_unchecked::<bool>() };
+        assert!(*boxed == value);
+        cover_reached();
+    }
+
+    #[kani::proof]
+    pub fn check_from_slice_trivial_clone() {
+        let data: [u8; 2] = kani::any();
+        let boxed = Box::<[u8]>::from(&data[..]);
+        assert!(&*boxed == &data);
+    }
+
+    #[kani::proof]
+    #[kani::unwind(3)]
+    pub fn check_from_slice_clone() {
+        let data = [CloneCell(kani::any())];
+        let boxed = Box::<[CloneCell]>::from(&data[..]);
+        assert!(boxed.len() == 1);
+        assert!(boxed[0].0 == data[0].0);
+    }
+
+    #[kani::proof]
+    pub fn check_from_str() {
+        let boxed: Box<str> = Box::from("xy");
+        assert!(&*boxed == "xy");
+    }
+
+    #[kani::proof]
+    pub fn check_from_box_str_to_bytes() {
+        let boxed: Box<str> = Box::from("xy");
+        let bytes: Box<[u8]> = Box::from(boxed);
+        assert!(&*bytes == b"xy");
+    }
+
+    #[kani::proof]
+    pub fn check_try_from_boxed_slice() {
+        // One element more than N, so the slice can be shorter or longer than N.
+        let data: [i32; 3] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&data);
+        let boxed: Box<[i32]> = Box::from(slice);
+        let len = boxed.len();
+        kani::cover(len < 2, "slice shorter than N");
+        kani::cover(len == 2, "slice of length N");
+        kani::cover(len > 2, "slice longer than N");
+        match Box::<[i32; 2]>::try_from(boxed) {
+            Ok(_arr) => assert!(len == 2),
+            Err(rest) => assert!(rest.len() != 2),
+        }
+    }
+
+    #[kani::proof]
+    pub fn check_try_from_vec() {
+        // One element more than N, so the vector can be shorter or longer than N.
+        let data: [i32; 3] = kani::any();
+        let slice = kani::slice::any_slice_of_array(&data);
+        let vec: Vec<i32> = slice.to_vec();
+        let len = vec.len();
+        kani::cover(len < 2, "vector shorter than N");
+        kani::cover(len == 2, "vector of length N");
+        kani::cover(len > 2, "vector longer than N");
+        match Box::<[i32; 2]>::try_from(vec) {
+            Ok(_arr) => assert!(len == 2),
+            Err(rest) => assert!(rest.len() != 2),
+        }
+    }
+
+    #[kani::proof_for_contract(boxed_slice_as_array_unchecked)]
+    pub fn check_boxed_slice_as_array_unchecked() {
+        let data: [u8; 2] = kani::any();
+        let boxed: Box<[u8]> = Box::from(data);
+        let arr = unsafe { boxed_slice_as_array_unchecked::<u8, _, 2>(boxed) };
+        assert!(arr[0] == data[0] && arr[1] == data[1]);
+        cover_reached();
+    }
+
+    #[kani::proof]
+    pub fn check_downcast_any() {
+        let value: i32 = kani::any();
+        let ok: Box<dyn Any> = Box::new(value);
+        let ok = ok.downcast::<i32>();
+        kani::cover(ok.is_ok(), "Ok: downcast to the stored type");
+        assert!(ok.is_ok());
+        let err: Box<dyn Any> = Box::new(value);
+        let err = err.downcast::<u8>();
+        kani::cover(err.is_err(), "Err: downcast to another type");
+        assert!(err.is_err());
+    }
+
+    #[kani::proof]
+    pub fn check_downcast_any_send() {
+        let value: i32 = kani::any();
+        let ok: Box<dyn Any + Send> = Box::new(value);
+        let ok = ok.downcast::<i32>();
+        kani::cover(ok.is_ok(), "Ok: downcast to the stored type");
+        assert!(ok.is_ok());
+        let err: Box<dyn Any + Send> = Box::new(value);
+        let err = err.downcast::<u8>();
+        kani::cover(err.is_err(), "Err: downcast to another type");
+        assert!(err.is_err());
+    }
+
+    #[kani::proof]
+    pub fn check_downcast_any_send_sync() {
+        let value: i32 = kani::any();
+        let ok: Box<dyn Any + Send + Sync> = Box::new(value);
+        let ok = ok.downcast::<i32>();
+        kani::cover(ok.is_ok(), "Ok: downcast to the stored type");
+        assert!(ok.is_ok());
+        let err: Box<dyn Any + Send + Sync> = Box::new(value);
+        let err = err.downcast::<bool>();
+        kani::cover(err.is_err(), "Err: downcast to another type");
+        assert!(err.is_err());
+    }
+
+    #[kani::proof]
+    pub fn check_downcast_error() {
+        let ok: Box<dyn Error> = Box::new(ProbeError(kani::any()));
+        let ok = ok.downcast::<ProbeError>();
+        kani::cover(ok.is_ok(), "Ok: downcast to the stored type");
+        assert!(ok.is_ok());
+        let err: Box<dyn Error> = Box::new(ProbeError(0));
+        let err = err.downcast::<OtherError>();
+        kani::cover(err.is_err(), "Err: downcast to another type");
+        assert!(err.is_err());
+    }
+
+    #[kani::proof]
+    pub fn check_downcast_error_send() {
+        let ok: Box<dyn Error + Send> = Box::new(ProbeError(kani::any()));
+        let ok = ok.downcast::<ProbeError>();
+        kani::cover(ok.is_ok(), "Ok: downcast to the stored type");
+        assert!(ok.is_ok());
+        let err: Box<dyn Error + Send> = Box::new(ProbeError(0));
+        let err = err.downcast::<OtherError>();
+        kani::cover(err.is_err(), "Err: downcast to another type");
+        assert!(err.is_err());
+    }
+
+    #[kani::proof]
+    pub fn check_downcast_error_send_sync() {
+        let ok: Box<dyn Error + Send + Sync> = Box::new(ProbeError(kani::any()));
+        let ok = ok.downcast::<ProbeError>();
+        kani::cover(ok.is_ok(), "Ok: downcast to the stored type");
+        assert!(ok.is_ok());
+        let err: Box<dyn Error + Send + Sync> = Box::new(ProbeError(0));
+        let err = err.downcast::<OtherError>();
+        kani::cover(err.is_err(), "Err: downcast to another type");
+        assert!(err.is_err());
+    }
+}
diff --git a/library/alloc/src/boxed/thin.rs b/library/alloc/src/boxed/thin.rs
index 90bb2ef9b838c..ba333b152407c 100644
--- a/library/alloc/src/boxed/thin.rs
+++ b/library/alloc/src/boxed/thin.rs
@@ -6,6 +6,8 @@ use core::error::Error;
 use core::fmt::{self, Debug, Display, Formatter};
 #[cfg(not(no_global_oom_handling))]
 use core::intrinsics::{const_allocate, const_make_global};
+#[cfg(kani)]
+use core::kani;
 use core::marker::PhantomData;
 #[cfg(not(no_global_oom_handling))]
 use core::marker::Unsize;
@@ -14,6 +16,10 @@ use core::mem;
 use core::mem::SizedTypeProperties;
 use core::ops::{Deref, DerefMut};
 use core::ptr::{self, NonNull, Pointee};
+#[cfg(kani)]
+use core::ub_checks;
+
+use safety::requires;
 
 use crate::alloc::{self, Layout, LayoutError};
 
@@ -373,6 +379,7 @@ impl<H> WithHeader<H> {
     ///
     /// `value` must point to an undropped owned `T`, and `self` must not be
     /// accessed again after this is called.
+    #[requires(ub_checks::can_dereference(value))]
     unsafe fn drop<T: ?Sized>(&self, value: *mut T) {
         struct DropGuard<H> {
             ptr: NonNull<u8>,
@@ -453,3 +460,93 @@ impl<T> From<T> for ThinBox<T> {
         Self::new(value)
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    #![allow(missing_docs)]
+
+    use core::any::Any;
+    use core::kani;
+    use core::ops::{Deref, DerefMut};
+
+    use super::{ThinBox, WithHeader};
+
+    #[kani::proof]
+    pub fn check_deref() {
+        let value: i32 = kani::any();
+        let thin = ThinBox::new(value);
+        assert!(*thin.deref() == value);
+    }
+
+    #[kani::proof]
+    pub fn check_deref_mut() {
+        let value: i32 = kani::any();
+        let mut thin = ThinBox::new(value);
+        *thin.deref_mut() = value.wrapping_add(1);
+        assert!(*thin == value.wrapping_add(1));
+    }
+
+    #[kani::proof]
+    pub fn check_drop() {
+        drop(ThinBox::new(kani::any::<i32>()));
+        drop(ThinBox::new(()));
+    }
+
+    #[kani::proof]
+    pub fn check_meta() {
+        let thin = ThinBox::new(kani::any::<i32>());
+        let _ = thin.meta();
+    }
+
+    #[kani::proof]
+    pub fn check_with_header() {
+        let thin = ThinBox::new(kani::any::<u8>());
+        let _ = thin.with_header();
+    }
+
+    #[kani::proof]
+    pub fn check_withheader_new() {
+        let value: i32 = kani::any();
+        let header = WithHeader::<()>::new((), value);
+        unsafe {
+            assert!(*header.value().cast::<i32>() == value);
+            WithHeader::<()>::drop::<i32>(&header, header.value().cast());
+        }
+    }
+
+    #[kani::proof]
+    pub fn check_withheader_try_new() {
+        let value: u8 = kani::any();
+        let header = WithHeader::<()>::try_new((), value).expect("alloc");
+        unsafe {
+            assert!(*header.value().cast::<u8>() == value);
+            WithHeader::<()>::drop::<u8>(&header, header.value().cast());
+        }
+    }
+
+    #[kani::proof]
+    pub fn check_withheader_new_unsize_zst() {
+        let thin = ThinBox::<[i32]>::new_unsize([0i32; 0]);
+        assert!(thin.deref().is_empty());
+    }
+
+    #[kani::proof]
+    pub fn check_withheader_header() {
+        let thin = ThinBox::new(kani::any::<i32>());
+        let _ = thin.with_header().header();
+    }
+
+    #[kani::proof]
+    pub fn check_deref_unsize_slice() {
+        let thin = ThinBox::<[u8]>::new_unsize([kani::any::<u8>(), kani::any::<u8>()]);
+        assert!(thin.deref().len() == 2);
+    }
+
+    #[kani::proof]
+    pub fn check_deref_dyn_any() {
+        let value: i32 = kani::any();
+        let thin: ThinBox<dyn Any> = ThinBox::new_unsize(value);
+        assert!(*thin.deref().downcast_ref::<i32>().expect("type") == value);
+    }
+}