diff --git a/library/alloc/src/boxed.rs b/library/alloc/src/boxed.rs
index f426345f9fc62..7d56b5d218233 100644
--- a/library/alloc/src/boxed.rs
+++ b/library/alloc/src/boxed.rs
@@ -204,6 +204,10 @@ use core::pin::{Pin, PinSafePointer};
 use core::ptr::{self, NonNull};
 use core::task::{Context, Poll};
 
+use safety::{ensures, requires};
+#[cfg(kani)]
+use {crate::vec::Vec, core::kani};
+
 #[cfg(not(no_global_oom_handling))]
 use crate::alloc::handle_alloc_error;
 use crate::alloc::{AllocError, Allocator, AllocatorNightly, Global, Layout, StaticAllocator};
@@ -211,6 +215,16 @@ use crate::raw_vec::RawVec;
 #[cfg(not(no_global_oom_handling))]
 use crate::str::from_boxed_utf8_unchecked_in;
 
+// Checks the expressible layout and validity requirements for raw reconstruction.
+// Unique ownership and matching allocator provenance remain caller obligations.
+#[cfg(kani)]
+fn box_raw_valid<T: ?Sized>(raw: *const T) -> bool {
+    !raw.is_null()
+        && kani::mem::checked_align_of_raw(raw).is_some()
+        && kani::mem::checked_size_of_raw(raw).is_some_and(|n| n <= isize::MAX as usize)
+        && core::ub_checks::can_dereference(raw)
+}
+
 /// Conversion related impls for `Box<_>` (`From`, `downcast`, etc)
 mod convert;
 /// Iterator related impls for `Box<_>`.
@@ -1276,6 +1290,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: Restore contracts after kani#4985 fixes const-fn E0493.
+    // #[requires({
+    //     let ptr = (&*self) as *const mem::MaybeUninit<T> as *const T;
+    //     core::ub_checks::can_dereference(ptr)
+    // })]
+    // #[ensures(|result: &Box<T, A>| {
+    //     core::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 +1368,13 @@ impl<T, A: Allocator> Box<[mem::MaybeUninit<T>], A> {
     /// ```
     #[stable(feature = "new_uninit", since = "1.82.0")]
     #[inline]
+    #[requires({
+        let ptr = (&*self) as *const [mem::MaybeUninit<T>] as *const [T];
+        core::ub_checks::can_dereference(ptr)
+    })]
+    #[ensures(|result: &Box<[T], A>| {
+        core::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 +1430,8 @@ 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`"]
+    #[requires(box_raw_valid(raw))]
+    #[ensures(|result: &Self| (&**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 +1485,11 @@ 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_raw_valid(ptr.as_ptr()))]
+    #[ensures(|result: &Self| {
+        let raw = ptr.as_ptr();
+        (&**result) as *const T == raw
+    })]
     pub unsafe fn from_non_null(ptr: NonNull<T>) -> Self {
         // SAFETY: Upheld by caller.
         unsafe { Self::from_raw(ptr.as_ptr()) }
@@ -1632,6 +1668,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_raw_valid(raw))]
+    #[ensures(|result: &Self| (&**result) as *const T == raw)]
     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 +1723,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_raw_valid(raw.as_ptr()))]
+    #[ensures(|result: &Self| (&**result) as *const T == raw.as_ptr())]
     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 +2665,964 @@ impl<R: core::random::Rng + ?Sized, A: Allocator> core::random::Rng for Box<R, A
         (**self).fill_bytes(bytes)
     }
 }
+
+// Challenge 29
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod kani_box_harness_helpers {
+    use super::*;
+
+    pub(super) fn verifier_nondet_vec<T>() -> Vec<T> {
+        let cap: usize = kani::any();
+        let elem_layout = Layout::new::<T>();
+        kani::assume(elem_layout.repeat(cap).is_ok());
+        let mut v = Vec::<T>::with_capacity(cap);
+        unsafe {
+            let sz: usize = kani::any();
+            kani::assume(sz <= cap);
+            ptr::write_bytes(
+                v.as_mut_ptr().cast::<u8>(),
+                kani::any::<u8>(),
+                mem::size_of::<T>() * sz,
+            );
+            let initialized = ptr::slice_from_raw_parts(v.as_ptr(), sz);
+            // Constrain only the harness-generated bytes to form valid `T`
+            // values before `set_len`, as required by its safety contract.
+            // This does not assume any property or result of the boxed function
+            // under verification, so it is not assuming the proof conclusion.
+            kani::assume(core::ub_checks::can_dereference(initialized));
+            v.set_len(sz);
+        }
+        v
+    }
+
+    pub(super) fn box_slice_layout_ok<T>(len: usize) -> bool {
+        Layout::array::<T>(len).is_ok()
+    }
+
+    pub(super) fn verifier_nondet_vec_box<T>() -> Vec<T> {
+        let vec = verifier_nondet_vec();
+        kani::assume(box_slice_layout_ok::<T>(vec.len()));
+        vec
+    }
+
+    pub(super) fn verifier_nondet_box_uninit_slice<T>() -> Box<[mem::MaybeUninit<T>], Global> {
+        let len = kani::any_where(|l: &usize| box_slice_layout_ok::<T>(*l));
+        let mut boxed = Box::<[T]>::new_uninit_slice(len);
+        unsafe {
+            ptr::write_bytes(
+                boxed.as_mut_ptr().cast::<u8>(),
+                kani::any::<u8>(),
+                mem::size_of::<T>() * len,
+            );
+        }
+        boxed
+    }
+}
+
+// === UNSAFE FUNCTIONS ===
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use core::any::Any;
+    use core::marker::PhantomPinned;
+
+    use super::kani_box_harness_helpers::*;
+    use super::*;
+
+    macro_rules! gen_assume_init_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                let value: $ty = kani::any::<$ty>();
+                let expected = value.clone();
+                let mut uninit: Box<mem::MaybeUninit<$ty>, Global> =
+                    Box::<$ty, Global>::new_uninit_in(Global);
+                (*uninit).write(value);
+                let expected_ptr = (&*uninit) as *const mem::MaybeUninit<$ty> as *const $ty;
+                let init: Box<$ty, Global> = unsafe { uninit.assume_init() };
+                assert_eq!(&*init, &expected);
+                assert!(ptr::eq(&*init as *const $ty, expected_ptr));
+                kani::cover(true, "Box::assume_init preserves value and allocation");
+            }
+        };
+    }
+
+    gen_assume_init_harness!(harness_box_assume_init_i32, i32);
+    gen_assume_init_harness!(harness_box_assume_init_unit, ());
+    gen_assume_init_harness!(harness_box_assume_init_bool, bool);
+
+    macro_rules! gen_assume_init_slice_harness {
+        ($name:ident, $elem:ty) => {
+            #[kani::proof_for_contract(Box::<[core::mem::MaybeUninit<T>], A>::assume_init)]
+            pub fn $name() {
+                let uninit: Box<[mem::MaybeUninit<$elem>], Global> =
+                    verifier_nondet_box_uninit_slice::<$elem>();
+                let expected_data = (&*uninit).as_ptr() as *const $elem;
+                let expected_len = uninit.len();
+                let result: Box<[$elem], Global> = unsafe { uninit.assume_init() };
+                assert_eq!((&*result).as_ptr(), expected_data);
+                assert_eq!(result.len(), expected_len);
+                kani::cover(true, "Box::assume_init slice preserves pointer and length");
+            }
+        };
+    }
+
+    gen_assume_init_slice_harness!(harness_box_assume_init_slice_u8, u8);
+    // Multi-byte elements exercise slice layout scaling and alignment.
+    gen_assume_init_slice_harness!(harness_box_assume_init_slice_u32, u32);
+    gen_assume_init_slice_harness!(harness_box_assume_init_slice_unit, ());
+
+    /// Checks slice assume_init with bool's restricted valid bit patterns.
+    #[kani::proof_for_contract(Box::<[core::mem::MaybeUninit<T>], A>::assume_init)]
+    fn harness_box_assume_init_slice_bool() {
+        let len = kani::any_where(|len: &usize| box_slice_layout_ok::<bool>(*len));
+        let value: bool = kani::any();
+        let mut uninit = Box::<[bool]>::new_uninit_slice(len);
+        let expected_data = uninit.as_ptr().cast::<bool>();
+        // Construct only valid 0/1 bytes before exposing a &[bool]. As in the
+        // other slice generators, the length is symbolic and the fill repeats.
+        unsafe { ptr::write_bytes(uninit.as_mut_ptr(), value as u8, len) };
+        let result = unsafe { uninit.assume_init() };
+        assert_eq!(result.as_ptr(), expected_data);
+        assert_eq!(result.len(), len);
+        if len != 0 {
+            let index = kani::any_where(|i: &usize| *i < len);
+            assert_eq!(result[index], value);
+        }
+        kani::cover(len == 0, "Box::assume_init bool slice accepts empty input");
+        kani::cover(len != 0, "Box::assume_init bool slice preserves valid bool values");
+    }
+
+    macro_rules! gen_from_raw_sized_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof_for_contract(Box::<$ty>::from_raw)]
+            pub fn $name() {
+                let value: $ty = kani::any();
+                let boxed: Box<$ty> = Box::new(value);
+                let ptr: *mut $ty = Box::into_raw(boxed);
+                let recovered: Box<$ty> = unsafe { Box::from_raw(ptr) };
+                assert!(ptr::eq(&*recovered, ptr));
+                kani::cover(true, "Box::from_raw returns under its contract preconditions");
+            }
+        };
+    }
+
+    macro_rules! gen_from_raw_unsized_harness {
+        ($name:ident, $elem:ty) => {
+            #[kani::proof_for_contract(Box::<[$elem]>::from_raw)]
+            pub fn $name() {
+                let boxed: Box<[$elem]> = verifier_nondet_vec_box::<$elem>().into_boxed_slice();
+                let ptr: *mut [$elem] = Box::into_raw(boxed);
+                let recovered: Box<[$elem]> = unsafe { Box::from_raw(ptr) };
+                assert!(ptr::eq(&*recovered, ptr));
+                kani::cover(true, "Box::from_raw returns under its contract preconditions");
+            }
+        };
+    }
+
+    gen_from_raw_sized_harness!(harness_box_from_raw_i32, i32);
+    gen_from_raw_sized_harness!(harness_box_from_raw_unit, ());
+
+    gen_from_raw_unsized_harness!(harness_box_from_raw_vec_u8, u8);
+    gen_from_raw_unsized_harness!(harness_box_from_raw_vec_u32, u32);
+
+    macro_rules! gen_from_non_null_sized_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof_for_contract(Box::<$ty>::from_non_null)]
+            pub fn $name() {
+                let value: $ty = kani::any();
+                let boxed: Box<$ty> = Box::new(value);
+                let ptr: NonNull<$ty> = Box::into_non_null(boxed);
+                let recovered: Box<$ty> = unsafe { Box::from_non_null(ptr) };
+                assert!(ptr::eq(&*recovered, ptr.as_ptr()));
+                kani::cover(true, "Box::from_non_null returns under its contract preconditions");
+            }
+        };
+    }
+
+    macro_rules! gen_from_non_null_unsized_harness {
+        ($name:ident, $elem:ty) => {
+            #[kani::proof_for_contract(Box::<[$elem]>::from_non_null)]
+            pub fn $name() {
+                let boxed: Box<[$elem]> = verifier_nondet_vec_box::<$elem>().into_boxed_slice();
+                let ptr: NonNull<[$elem]> = Box::into_non_null(boxed);
+                let recovered: Box<[$elem]> = unsafe { Box::from_non_null(ptr) };
+                assert!(ptr::eq(&*recovered, ptr.as_ptr()));
+                kani::cover(true, "Box::from_non_null returns under its contract preconditions");
+            }
+        };
+    }
+
+    gen_from_non_null_sized_harness!(harness_box_from_non_null_i32, i32);
+    gen_from_non_null_sized_harness!(harness_box_from_non_null_unit, ());
+
+    gen_from_non_null_unsized_harness!(harness_box_from_non_null_vec_u8, u8);
+    gen_from_non_null_unsized_harness!(harness_box_from_non_null_vec_u32, u32);
+
+    // These harnesses allocate raw memory directly instead of using higher-level
+    // Box constructors. `proof_for_contract` requires a single top-level call to
+    // `Box::from_raw_in`, while helpers such as `Box::new_in`,
+    // `Box::new_uninit_slice_in`, and `Vec::into_boxed_slice` eventually route
+    // through `Box::from_raw_in` during setup.
+
+    macro_rules! gen_from_raw_in_sized_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof_for_contract(Box::<$ty, Global>::from_raw_in)]
+            pub fn $name() {
+                let value: $ty = kani::any();
+                let ptr: *mut $ty = if mem::size_of::<$ty>() == 0 {
+                    // ZST boxes use a non-null dangling pointer and never allocate.
+                    mem::forget(value);
+                    NonNull::<$ty>::dangling().as_ptr()
+                } else {
+                    let layout = Layout::new::<$ty>();
+                    let ptr = match Global.allocate(layout) {
+                        Ok(memory) => memory.cast::<$ty>().as_ptr(),
+                        Err(_) => handle_alloc_error(layout),
+                    };
+                    unsafe { ptr.write(value) };
+                    ptr
+                };
+                let alloc = Global;
+                let recovered: Box<$ty, Global> = unsafe { Box::from_raw_in(ptr, alloc) };
+                assert!(ptr::eq(&*recovered, ptr));
+                kani::cover(true, "Box::from_raw_in returns under its contract preconditions");
+            }
+        };
+    }
+
+    macro_rules! gen_from_raw_in_unsized_harness {
+        ($name:ident, $elem:ty) => {
+            #[kani::proof_for_contract(Box::<[$elem], Global>::from_raw_in)]
+            pub fn $name() {
+                // Keep the slice length symbolic so this remains an unbound
+                // unsized harness, while still ruling out impossible layouts.
+                let len: usize = kani::any_where(|len: &usize| box_slice_layout_ok::<$elem>(*len));
+                let data: *mut $elem = if len == 0 {
+                    NonNull::<$elem>::dangling().as_ptr()
+                } else {
+                    let layout = Layout::array::<$elem>(len).unwrap();
+                    let ptr = match Global.allocate(layout) {
+                        Ok(memory) => memory.cast::<$elem>().as_ptr(),
+                        Err(_) => handle_alloc_error(layout),
+                    };
+                    unsafe {
+                        ptr::write_bytes(
+                            ptr.cast::<u8>(),
+                            kani::any::<u8>(),
+                            mem::size_of::<$elem>() * len,
+                        );
+                    }
+                    ptr
+                };
+                let ptr: *mut [$elem] = ptr::slice_from_raw_parts_mut(data, len);
+                let alloc = Global;
+                let recovered: Box<[$elem], Global> = unsafe { Box::from_raw_in(ptr, alloc) };
+                assert!(ptr::eq(&*recovered, ptr));
+                kani::cover(true, "Box::from_raw_in returns under its contract preconditions");
+            }
+        };
+    }
+
+    gen_from_raw_in_sized_harness!(harness_box_from_raw_in_i32, i32);
+    gen_from_raw_in_sized_harness!(harness_box_from_raw_in_unit, ());
+
+    gen_from_raw_in_unsized_harness!(harness_box_from_raw_in_vec_u8, u8);
+    gen_from_raw_in_unsized_harness!(harness_box_from_raw_in_vec_u32, u32);
+
+    macro_rules! gen_from_non_null_in_sized_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof_for_contract(Box::<$ty, Global>::from_non_null_in)]
+            pub fn $name() {
+                let value: $ty = kani::any();
+                let boxed: Box<$ty, Global> = Box::new_in(value, Global);
+                let (ptr, alloc): (NonNull<$ty>, Global) = Box::into_non_null_with_allocator(boxed);
+                let recovered: Box<$ty, Global> = unsafe { Box::from_non_null_in(ptr, alloc) };
+                assert!(ptr::eq(&*recovered, ptr.as_ptr()));
+                kani::cover(true, "Box::from_non_null_in returns under its contract preconditions");
+            }
+        };
+    }
+
+    macro_rules! gen_from_non_null_in_unsized_harness {
+        ($name:ident, $elem:ty) => {
+            #[kani::proof_for_contract(Box::<[$elem], Global>::from_non_null_in)]
+            pub fn $name() {
+                let boxed: Box<[$elem], Global> =
+                    verifier_nondet_vec_box::<$elem>().into_boxed_slice();
+                let (ptr, alloc): (NonNull<[$elem]>, Global) =
+                    Box::into_non_null_with_allocator(boxed);
+                let recovered: Box<[$elem], Global> = unsafe { Box::from_non_null_in(ptr, alloc) };
+                assert!(ptr::eq(&*recovered, ptr.as_ptr()));
+                kani::cover(true, "Box::from_non_null_in returns under its contract preconditions");
+            }
+        };
+    }
+
+    gen_from_non_null_in_sized_harness!(harness_box_from_non_null_in_i32, i32);
+    gen_from_non_null_in_sized_harness!(harness_box_from_non_null_in_unit, ());
+
+    gen_from_non_null_in_unsized_harness!(harness_box_from_non_null_in_vec_u8, u8);
+    gen_from_non_null_in_unsized_harness!(harness_box_from_non_null_in_vec_u32, u32);
+
+    // === SAFE FUNCTIONS ===
+
+    // Checks Box::new_in.
+    macro_rules! gen_box_new_in_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                let value: $ty = kani::any();
+                let boxed = Box::<$ty, Global>::new_in(value, Global);
+                assert_eq!(*boxed, value);
+                kani::cover(true, "Box::new_in preserves the value");
+            }
+        };
+    }
+
+    // Checks Box::new_in.
+    macro_rules! gen_box_new_in_vec_harness {
+        ($name:ident, $elem:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                let vec: Vec<$elem> = verifier_nondet_vec::<$elem>();
+                let expected = (vec.as_ptr(), vec.len(), vec.capacity());
+                let boxed = Box::<Vec<$elem>, Global>::new_in(vec, Global);
+                assert_eq!((boxed.as_ptr(), boxed.len(), boxed.capacity()), expected);
+                kani::cover(true, "Box::new_in preserves the Vec buffer, length and capacity");
+            }
+        };
+    }
+
+    gen_box_new_in_harness!(harness_box_new_in_i32, i32);
+    gen_box_new_in_harness!(harness_box_new_in_unit, ());
+
+    gen_box_new_in_vec_harness!(harness_box_new_in_vec_u8, u8);
+
+    // Checks Box::try_new_in.
+    macro_rules! gen_box_try_new_in_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                let value: $ty = kani::any();
+                if let Ok(boxed) = Box::<$ty, Global>::try_new_in(value, Global) {
+                    assert_eq!(*boxed, value);
+                    kani::cover(true, "Box::try_new_in succeeds and preserves the value");
+                }
+                kani::cover(true, "Box::try_new_in returns");
+            }
+        };
+    }
+
+    // Checks Box::try_new_in.
+    macro_rules! gen_box_try_new_in_vec_harness {
+        ($name:ident, $elem:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                let vec: Vec<$elem> = verifier_nondet_vec::<$elem>();
+                let expected = (vec.as_ptr(), vec.len(), vec.capacity());
+                if let Ok(boxed) = Box::<Vec<$elem>, Global>::try_new_in(vec, Global) {
+                    assert_eq!((boxed.as_ptr(), boxed.len(), boxed.capacity()), expected);
+                    kani::cover(
+                        true,
+                        "Box::try_new_in preserves the Vec buffer, length and capacity",
+                    );
+                }
+                kani::cover(true, "Box::try_new_in Vec returns");
+            }
+        };
+    }
+
+    gen_box_try_new_in_harness!(harness_box_try_new_in_i32, i32);
+    gen_box_try_new_in_harness!(harness_box_try_new_in_unit, ());
+
+    gen_box_try_new_in_vec_harness!(harness_box_try_new_in_vec_u8, u8);
+
+    // Checks Box::try_new_uninit_in.
+    macro_rules! gen_box_try_new_uninit_in_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                if let Ok(boxed) = Box::<$ty, Global>::try_new_uninit_in(Global) {
+                    assert!(boxed.as_ptr().is_aligned());
+                    assert!(!boxed.as_ptr().is_null());
+                    kani::cover(true, "Box::try_new_uninit_in returns aligned storage");
+                }
+                kani::cover(true, "Box::try_new_uninit_in returns");
+            }
+        };
+    }
+
+    gen_box_try_new_uninit_in_harness!(harness_box_try_new_uninit_in_i32, i32);
+    gen_box_try_new_uninit_in_harness!(harness_box_try_new_uninit_in_unit, ());
+
+    // Checks Box::try_new_zeroed_in.
+    macro_rules! gen_box_try_new_zeroed_in_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                if let Ok(boxed) = Box::<$ty, Global>::try_new_zeroed_in(Global) {
+                    // The instantiated i32 and () types admit an all-zero representation.
+                    assert_eq!(unsafe { boxed.assume_init() }.as_ref(), &<$ty>::default());
+                    kani::cover(true, "Box::try_new_zeroed_in initializes the value to zero");
+                }
+                kani::cover(true, "Box::try_new_zeroed_in returns");
+            }
+        };
+    }
+
+    gen_box_try_new_zeroed_in_harness!(harness_box_try_new_zeroed_in_i32, i32);
+    gen_box_try_new_zeroed_in_harness!(harness_box_try_new_zeroed_in_unit, ());
+
+    // Checks Box::into_boxed_slice.
+    macro_rules! gen_box_into_boxed_slice_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                let value: $ty = kani::any();
+                let boxed: Box<$ty, Global> = Box::<$ty, Global>::new_in(value, Global);
+                let expected = &*boxed as *const $ty;
+                let slice = Box::<$ty, Global>::into_boxed_slice(boxed);
+                assert_eq!(slice.len(), 1);
+                assert_eq!(slice.as_ptr(), expected);
+                assert_eq!(slice[0], value);
+                kani::cover(true, "Box::into_boxed_slice preserves pointer and value");
+            }
+        };
+    }
+
+    // Checks Box::into_boxed_slice.
+    macro_rules! gen_box_into_boxed_slice_vec_harness {
+        ($name:ident, $elem:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                let value: Vec<$elem> = verifier_nondet_vec::<$elem>();
+                let boxed: Box<Vec<$elem>, Global> =
+                    Box::<Vec<$elem>, Global>::new_in(value, Global);
+                let expected = &*boxed as *const Vec<$elem>;
+                let buffer = (boxed.as_ptr(), boxed.len(), boxed.capacity());
+                let slice = Box::<Vec<$elem>, Global>::into_boxed_slice(boxed);
+                assert_eq!(slice.len(), 1);
+                assert_eq!(slice.as_ptr(), expected);
+                assert_eq!((slice[0].as_ptr(), slice[0].len(), slice[0].capacity()), buffer);
+                kani::cover(true, "Box::into_boxed_slice preserves the Vec payload");
+            }
+        };
+    }
+
+    gen_box_into_boxed_slice_harness!(harness_box_into_boxed_slice_u8, u8);
+    gen_box_into_boxed_slice_harness!(harness_box_into_boxed_slice_unit, ());
+
+    gen_box_into_boxed_slice_vec_harness!(harness_box_into_boxed_slice_vec_u8, u8);
+
+    // Checks Box::new_uninit_slice.
+    macro_rules! gen_box_new_uninit_slice_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                let len: usize = kani::any_where(|l: &usize| box_slice_layout_ok::<$ty>(*l));
+                let boxed: Box<[mem::MaybeUninit<$ty>]> = Box::<[$ty]>::new_uninit_slice(len);
+                assert_eq!(boxed.len(), len);
+                assert!(boxed.as_ptr().is_aligned());
+                kani::cover(len == 0, "Box::new_uninit_slice returns an empty slice");
+                kani::cover(len != 0, "Box::new_uninit_slice returns a nonempty slice");
+            }
+        };
+    }
+
+    gen_box_new_uninit_slice_harness!(harness_box_new_uninit_slice_u8, u8);
+    gen_box_new_uninit_slice_harness!(harness_box_new_uninit_slice_u32, u32);
+    gen_box_new_uninit_slice_harness!(harness_box_new_uninit_slice_unit, ());
+
+    // Checks Box::new_zeroed_slice.
+    macro_rules! gen_box_new_zeroed_slice_harness {
+        ($name:ident, $elem_ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                let len: usize = kani::any_where(|l: &usize| box_slice_layout_ok::<$elem_ty>(*l));
+                let boxed: Box<[mem::MaybeUninit<$elem_ty>]> =
+                    Box::<[$elem_ty]>::new_zeroed_slice(len);
+                assert_eq!(boxed.len(), len);
+                assert!(boxed.as_ptr().is_aligned());
+                if len != 0 {
+                    let index = kani::any_where(|i: &usize| *i < len);
+                    // All instantiated element types admit zero initialization.
+                    assert_eq!(unsafe { boxed[index].assume_init() }, <$elem_ty>::default());
+                }
+                kani::cover(len == 0, "Box::new_zeroed_slice returns an empty slice");
+                kani::cover(len != 0, "Box::new_zeroed_slice returns a nonempty slice");
+            }
+        };
+    }
+
+    gen_box_new_zeroed_slice_harness!(harness_box_new_zeroed_slice_u8, u8);
+    gen_box_new_zeroed_slice_harness!(harness_box_new_zeroed_slice_u32, u32);
+    gen_box_new_zeroed_slice_harness!(harness_box_new_zeroed_slice_unit, ());
+
+    // Checks Box::try_new_uninit_slice.
+    macro_rules! gen_box_try_new_uninit_slice_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                let len: usize = kani::any();
+                let result: Result<Box<[mem::MaybeUninit<$ty>]>, AllocError> =
+                    Box::<[$ty]>::try_new_uninit_slice(len);
+                let layout_ok = box_slice_layout_ok::<$ty>(len);
+                assert!(layout_ok || result.is_err());
+                // ZSTs cannot have a layout-overflow error.
+                if mem::size_of::<$ty>() != 0 {
+                    kani::cover(
+                        !layout_ok && result.is_err(),
+                        "slice constructor rejects layout overflow",
+                    );
+                }
+                if let Ok(boxed) = result {
+                    assert_eq!(boxed.len(), len);
+                    assert!(boxed.as_ptr().is_aligned());
+                    kani::cover(len == 0, "Box::try_new_uninit_slice succeeds for an empty slice");
+                    kani::cover(
+                        len != 0,
+                        "Box::try_new_uninit_slice succeeds for a nonempty slice",
+                    );
+                }
+                kani::cover(true, "Box::try_new_uninit_slice returns");
+            }
+        };
+    }
+
+    gen_box_try_new_uninit_slice_harness!(harness_box_try_new_uninit_slice_u8, u8);
+    gen_box_try_new_uninit_slice_harness!(harness_box_try_new_uninit_slice_u32, u32);
+    gen_box_try_new_uninit_slice_harness!(harness_box_try_new_uninit_slice_unit, ());
+
+    // Checks Box::try_new_zeroed_slice.
+    macro_rules! gen_box_try_new_zeroed_slice_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                let len: usize = kani::any();
+                let result: Result<Box<[mem::MaybeUninit<$ty>]>, AllocError> =
+                    Box::<[$ty]>::try_new_zeroed_slice(len);
+                let layout_ok = box_slice_layout_ok::<$ty>(len);
+                assert!(layout_ok || result.is_err());
+                // ZSTs cannot have a layout-overflow error.
+                if mem::size_of::<$ty>() != 0 {
+                    kani::cover(
+                        !layout_ok && result.is_err(),
+                        "slice constructor rejects layout overflow",
+                    );
+                }
+                if let Ok(boxed) = result {
+                    assert_eq!(boxed.len(), len);
+                    assert!(boxed.as_ptr().is_aligned());
+                    if len != 0 {
+                        let index = kani::any_where(|i: &usize| *i < len);
+                        // All instantiated element types admit zero initialization.
+                        assert_eq!(unsafe { boxed[index].assume_init() }, <$ty>::default());
+                    }
+                    kani::cover(len == 0, "Box::try_new_zeroed_slice succeeds for an empty slice");
+                    kani::cover(
+                        len != 0,
+                        "Box::try_new_zeroed_slice succeeds for a nonempty slice",
+                    );
+                }
+                kani::cover(true, "Box::try_new_zeroed_slice returns");
+            }
+        };
+    }
+
+    gen_box_try_new_zeroed_slice_harness!(harness_box_try_new_zeroed_slice_u8, u8);
+    gen_box_try_new_zeroed_slice_harness!(harness_box_try_new_zeroed_slice_u32, u32);
+    gen_box_try_new_zeroed_slice_harness!(harness_box_try_new_zeroed_slice_unit, ());
+
+    // Keep source lengths symbolic for both empty and nonempty array targets.
+    macro_rules! gen_box_into_array_slice_harness {
+        ($name:ident, $ty:ty, $n:expr) => {
+            #[kani::proof]
+            pub fn $name() {
+                let boxed = verifier_nondet_vec_box::<$ty>().into_boxed_slice();
+                let (len, address) = (boxed.len(), boxed.as_ptr());
+                let index = if len == 0 { 0 } else { kani::any_where(|i: &usize| *i < len) };
+                let expected = boxed.get(index).copied();
+                let recovered: Box<[$ty]> = match boxed.into_array::<$n>() {
+                    Ok(array) => {
+                        assert_eq!(len, $n);
+                        array
+                    }
+                    Err(rest) => {
+                        assert_ne!(len, $n);
+                        rest
+                    }
+                };
+                assert_eq!(recovered.len(), len);
+                assert_eq!(recovered.as_ptr(), address);
+                assert_eq!(recovered.get(index).copied(), expected);
+                kani::cover(len == $n, "Box::into_array accepts matching length");
+                kani::cover(len != $n, "Box::into_array rejects mismatched length");
+            }
+        };
+    }
+
+    gen_box_into_array_slice_harness!(harness_box_into_array_slice_u8, u8, 2);
+    gen_box_into_array_slice_harness!(harness_box_into_array_slice_u32, u32, 2);
+    gen_box_into_array_slice_harness!(harness_box_into_array_slice_unit, (), 2);
+    gen_box_into_array_slice_harness!(harness_box_into_array_slice_empty, u8, 0);
+
+    // Checks Box::new_uninit_slice_in.
+    macro_rules! gen_box_new_uninit_slice_in_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                let len: usize = kani::any_where(|l: &usize| box_slice_layout_ok::<$ty>(*l));
+                let boxed: Box<[mem::MaybeUninit<$ty>], Global> =
+                    Box::<[$ty], Global>::new_uninit_slice_in(len, Global);
+                assert_eq!(boxed.len(), len);
+                assert!(boxed.as_ptr().is_aligned());
+                kani::cover(len == 0, "Box::new_uninit_slice_in returns an empty slice");
+                kani::cover(len != 0, "Box::new_uninit_slice_in returns a nonempty slice");
+            }
+        };
+    }
+
+    gen_box_new_uninit_slice_in_harness!(harness_box_new_uninit_slice_in_u8, u8);
+    gen_box_new_uninit_slice_in_harness!(harness_box_new_uninit_slice_in_u32, u32);
+    gen_box_new_uninit_slice_in_harness!(harness_box_new_uninit_slice_in_unit, ());
+
+    // Checks Box::new_zeroed_slice_in.
+    macro_rules! gen_box_new_zeroed_slice_in_harness {
+        ($name:ident, $elem_ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                type T = $elem_ty;
+                let len: usize = kani::any_where(|l: &usize| box_slice_layout_ok::<T>(*l));
+                let boxed: Box<[mem::MaybeUninit<T>], Global> =
+                    Box::<[T], Global>::new_zeroed_slice_in(len, Global);
+                assert_eq!(boxed.len(), len);
+                assert!(boxed.as_ptr().is_aligned());
+                if len != 0 {
+                    let index = kani::any_where(|i: &usize| *i < len);
+                    // All instantiated element types admit zero initialization.
+                    assert_eq!(unsafe { boxed[index].assume_init() }, <T>::default());
+                }
+                kani::cover(len == 0, "Box::new_zeroed_slice_in returns an empty slice");
+                kani::cover(len != 0, "Box::new_zeroed_slice_in returns a nonempty slice");
+            }
+        };
+    }
+
+    gen_box_new_zeroed_slice_in_harness!(harness_box_new_zeroed_slice_in_u8, u8);
+    gen_box_new_zeroed_slice_in_harness!(harness_box_new_zeroed_slice_in_u32, u32);
+    gen_box_new_zeroed_slice_in_harness!(harness_box_new_zeroed_slice_in_unit, ());
+
+    // Checks Box::try_new_uninit_slice_in.
+    macro_rules! gen_box_try_new_uninit_slice_in_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                let len: usize = kani::any();
+                let result: Result<Box<[mem::MaybeUninit<$ty>], Global>, AllocError> =
+                    Box::<[$ty], Global>::try_new_uninit_slice_in(len, Global);
+                let layout_ok = box_slice_layout_ok::<$ty>(len);
+                assert!(layout_ok || result.is_err());
+                // ZSTs cannot have a layout-overflow error.
+                if mem::size_of::<$ty>() != 0 {
+                    kani::cover(
+                        !layout_ok && result.is_err(),
+                        "slice constructor rejects layout overflow",
+                    );
+                }
+                if let Ok(boxed) = result {
+                    assert_eq!(boxed.len(), len);
+                    assert!(boxed.as_ptr().is_aligned());
+                    kani::cover(
+                        len == 0,
+                        "Box::try_new_uninit_slice_in succeeds for an empty slice",
+                    );
+                    kani::cover(
+                        len != 0,
+                        "Box::try_new_uninit_slice_in succeeds for a nonempty slice",
+                    );
+                }
+                kani::cover(true, "Box::try_new_uninit_slice_in returns");
+            }
+        };
+    }
+
+    gen_box_try_new_uninit_slice_in_harness!(harness_box_try_new_uninit_slice_in_u8, u8);
+    gen_box_try_new_uninit_slice_in_harness!(harness_box_try_new_uninit_slice_in_u32, u32);
+    gen_box_try_new_uninit_slice_in_harness!(harness_box_try_new_uninit_slice_in_unit, ());
+
+    // Checks Box::try_new_zeroed_slice_in.
+    macro_rules! gen_box_try_new_zeroed_slice_in_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                let len: usize = kani::any();
+                let result: Result<Box<[mem::MaybeUninit<$ty>], Global>, AllocError> =
+                    Box::<[$ty], Global>::try_new_zeroed_slice_in(len, Global);
+                let layout_ok = box_slice_layout_ok::<$ty>(len);
+                assert!(layout_ok || result.is_err());
+                // ZSTs cannot have a layout-overflow error.
+                if mem::size_of::<$ty>() != 0 {
+                    kani::cover(
+                        !layout_ok && result.is_err(),
+                        "slice constructor rejects layout overflow",
+                    );
+                }
+                if let Ok(boxed) = result {
+                    assert_eq!(boxed.len(), len);
+                    assert!(boxed.as_ptr().is_aligned());
+                    if len != 0 {
+                        let index = kani::any_where(|i: &usize| *i < len);
+                        // All instantiated element types admit zero initialization.
+                        assert_eq!(unsafe { boxed[index].assume_init() }, <$ty>::default());
+                    }
+                    kani::cover(
+                        len == 0,
+                        "Box::try_new_zeroed_slice_in succeeds for an empty slice",
+                    );
+                    kani::cover(
+                        len != 0,
+                        "Box::try_new_zeroed_slice_in succeeds for a nonempty slice",
+                    );
+                }
+                kani::cover(true, "Box::try_new_zeroed_slice_in returns");
+            }
+        };
+    }
+
+    gen_box_try_new_zeroed_slice_in_harness!(harness_box_try_new_zeroed_slice_in_u8, u8);
+    gen_box_try_new_zeroed_slice_in_harness!(harness_box_try_new_zeroed_slice_in_u32, u32);
+    gen_box_try_new_zeroed_slice_in_harness!(harness_box_try_new_zeroed_slice_in_unit, ());
+
+    // Checks Box::write.
+    macro_rules! gen_box_write_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                let value: $ty = kani::any();
+                let boxed: Box<mem::MaybeUninit<$ty>, Global> =
+                    Box::<$ty, Global>::new_uninit_in(Global);
+                let expected = boxed.as_ptr();
+                let written = Box::write(boxed, value);
+                assert_eq!(&*written as *const $ty, expected);
+                assert_eq!(*written, value);
+                kani::cover(true, "Box::write preserves the allocation and stores the value");
+            }
+        };
+    }
+
+    // Checks Box::write.
+    macro_rules! gen_box_write_vec_harness {
+        ($name:ident, $elem:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                let value: Vec<$elem> = verifier_nondet_vec::<$elem>();
+                let boxed: Box<mem::MaybeUninit<Vec<$elem>>, Global> =
+                    Box::<Vec<$elem>, Global>::new_uninit_in(Global);
+                let expected = boxed.as_ptr();
+                let buffer = (value.as_ptr(), value.len(), value.capacity());
+                let written = Box::write(boxed, value);
+                assert_eq!(&*written as *const Vec<$elem>, expected);
+                assert_eq!((written.as_ptr(), written.len(), written.capacity()), buffer);
+                kani::cover(true, "Box::write preserves the allocation and Vec payload");
+            }
+        };
+    }
+
+    gen_box_write_harness!(harness_box_write_i32, i32);
+    gen_box_write_harness!(harness_box_write_unit, ());
+    gen_box_write_harness!(harness_box_write_bool, bool);
+
+    gen_box_write_vec_harness!(harness_box_write_vec_u8, u8);
+
+    // Each module has its own target and proof entry points. Shared setup covers
+    // ordinary allocation, ZSTs and slice metadata.
+    macro_rules! box_pointer_harnesses {
+        ($module:ident, $target:literal, |$boxed:ident| $body:block $(, $dyn_harness:ident)?) => {
+            mod $module {
+                use super::*;
+
+                #[doc = $target]
+                fn check<T: ?Sized>($boxed: Box<T>) {
+                    $body
+                    kani::cover(true, $target);
+                }
+
+                #[kani::proof]
+                fn sized() { check(Box::new(kani::any::<i32>())); }
+
+                #[kani::proof]
+                fn zst() { check(Box::new(())); }
+
+                #[kani::proof]
+                fn slice() { check(verifier_nondet_vec_box::<u8>().into_boxed_slice()); }
+
+                $(
+                    #[kani::proof]
+                    fn $dyn_harness() {
+                        let boxed: Box<dyn Any> = Box::new(kani::any::<i32>());
+                        check(boxed);
+                    }
+                )?
+            }
+        };
+    }
+
+    box_pointer_harnesses!(harness_box_into_non_null, "Checks Box::into_non_null.", |boxed| {
+        let expected = &*boxed as *const _;
+        let ptr = Box::into_non_null(boxed);
+        assert!(ptr::eq(ptr.as_ptr(), expected));
+        let _recovered = unsafe { Box::from_non_null(ptr) };
+    });
+    box_pointer_harnesses!(
+        harness_box_into_raw_with_allocator,
+        "Checks Box::into_raw_with_allocator.",
+        |boxed| {
+            let expected = &*boxed as *const _;
+            let expected_layout = Layout::for_value(&*boxed);
+            let (ptr, alloc) = Box::into_raw_with_allocator(boxed);
+            assert!(ptr::addr_eq(ptr, expected));
+            let recovered = unsafe { Box::from_raw_in(ptr, alloc) };
+            let layout = Layout::for_value(&*recovered);
+            assert_eq!(layout.size(), expected_layout.size());
+            assert_eq!(layout.align(), expected_layout.align());
+        },
+        dyn_any
+    );
+    box_pointer_harnesses!(
+        harness_box_into_non_null_with_allocator,
+        "Checks Box::into_non_null_with_allocator.",
+        |boxed| {
+            let expected = &*boxed as *const _;
+            let (ptr, alloc) = Box::into_non_null_with_allocator(boxed);
+            assert!(ptr::eq(ptr.as_ptr(), expected));
+            let _recovered = unsafe { Box::from_non_null_in(ptr, alloc) };
+        }
+    );
+    box_pointer_harnesses!(harness_box_leak, "Checks Box::leak.", |boxed| {
+        let expected = &*boxed as *const _;
+        let leaked = Box::leak(boxed);
+        assert!(ptr::eq(leaked, expected));
+        // Box::leak intentionally leaves the allocation alive.
+        // Do not reconstruct a Box from the returned mutable reference.
+    });
+    box_pointer_harnesses!(harness_box_into_pin, "Checks Box::into_pin.", |boxed| {
+        let expected = &*boxed as *const _;
+        let pinned = Box::into_pin(boxed);
+        assert!(ptr::eq(&*pinned, expected));
+    });
+    box_pointer_harnesses!(
+        harness_box_drop,
+        "Checks <Box<T> as Drop>::drop.",
+        |boxed| {
+            drop(boxed);
+        },
+        dyn_any
+    );
+
+    /// Checks Box::into_pin for a !Unpin pointee, preserving its address.
+    #[kani::proof]
+    fn harness_box_into_pin_not_unpin() {
+        struct NotUnpin(u8, PhantomPinned);
+        let value = kani::any();
+        let boxed = Box::new(NotUnpin(value, PhantomPinned));
+        let address = &*boxed as *const NotUnpin;
+        let pinned = Box::into_pin(boxed);
+        assert_eq!(&*pinned as *const NotUnpin, address);
+        assert_eq!(pinned.0, value);
+        kani::cover(true, "Box::into_pin preserves the !Unpin value and address");
+    }
+
+    /// Checks Box::drop's no-deallocation branch with nontrivial slice metadata.
+    #[kani::proof]
+    fn harness_box_drop_zst_slice() {
+        drop(verifier_nondet_vec_box::<()>().into_boxed_slice());
+        kani::cover(true, "Box::drop completes for a ZST slice");
+    }
+
+    // Checks <Box<T> as Default>::default.
+    macro_rules! gen_box_default_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                let boxed: Box<$ty> = Box::<$ty>::default();
+                assert_eq!(*boxed, <$ty>::default());
+                kani::cover(true, "Box::default returns the default value");
+            }
+        };
+    }
+
+    gen_box_default_harness!(harness_box_default_i32, i32);
+    gen_box_default_harness!(harness_box_default_unit, ());
+    gen_box_default_harness!(harness_box_default_vec_u8, Vec<u8>);
+
+    // Checks <Box<str> as Default>::default.
+    macro_rules! gen_box_str_default_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                let boxed: Box<$ty> = Box::<$ty>::default();
+                assert!(boxed.is_empty());
+                kani::cover(true, "Box<str>::default returns an empty string");
+            }
+        };
+    }
+
+    gen_box_str_default_harness!(harness_box_default_str, str);
+
+    // Checks <Box<T> as Clone>::clone.
+    macro_rules! gen_box_clone_harness {
+        ($name:ident, $ty:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                let value: $ty = kani::any();
+                let boxed: Box<$ty, Global> = Box::new_in(value, Global);
+                let cloned: Box<$ty, Global> = Clone::clone(&boxed);
+                assert_eq!(*cloned, *boxed);
+                kani::cover(true, "Box::clone preserves the value");
+            }
+        };
+    }
+
+    // Checks <Box<T> as Clone>::clone.
+    macro_rules! gen_box_clone_vec_harness {
+        ($name:ident, $elem:ty) => {
+            #[kani::proof]
+            pub fn $name() {
+                // Fix the length at 10 to avoid CBMC incomplete-result errors in CI.
+                let values: [$elem; 10] = kani::any();
+                let value: Vec<$elem> = Vec::from(values);
+                let boxed: Box<Vec<$elem>, Global> = Box::new_in(value, Global);
+                let cloned: Box<Vec<$elem>, Global> = Clone::clone(&boxed);
+                assert_eq!(cloned.len(), boxed.len());
+                let index = kani::any_where(|i: &usize| *i < boxed.len());
+                assert_eq!(cloned[index], boxed[index]);
+                kani::cover(true, "Box::clone preserves a Vec of length 10");
+            }
+        };
+    }
+
+    gen_box_clone_harness!(harness_box_clone_i32, i32);
+    gen_box_clone_harness!(harness_box_clone_unit, ());
+
+    gen_box_clone_vec_harness!(harness_box_clone_vec_u8, u8);
+
+    // Checks <Box<str> as Clone>::clone.
+    macro_rules! gen_box_str_clone_harness {
+        ($name:ident, $value:expr) => {
+            #[kani::proof]
+            pub fn $name() {
+                let boxed: Box<str> = Box::<str>::from($value);
+                let cloned: Box<str> = Clone::clone(&boxed);
+                assert_eq!(&*cloned, &*boxed);
+                kani::cover(true, "Box<str>::clone preserves the string");
+            }
+        };
+    }
+
+    gen_box_str_clone_harness!(harness_box_clone_str_empty, "");
+    gen_box_str_clone_harness!(harness_box_clone_str_nonempty, "test");
+}
diff --git a/library/alloc/src/boxed/convert.rs b/library/alloc/src/boxed/convert.rs
index 526e8b18a8031..7912fa74f43af 100644
--- a/library/alloc/src/boxed/convert.rs
+++ b/library/alloc/src/boxed/convert.rs
@@ -2,9 +2,13 @@ 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;
 
+use safety::{ensures, requires};
+
 use crate::alloc::{Allocator, StaticAllocator};
 #[cfg(not(no_global_oom_handling))]
 use crate::borrow::Cow;
@@ -364,6 +368,11 @@ impl<A: Allocator> Box<dyn Any, A> {
     /// [`downcast`]: Self::downcast
     #[inline]
     #[unstable(feature = "downcast_unchecked", issue = "90850")]
+    #[requires(self.is::<T>())]
+    #[ensures(|result: &Box<T, A>| core::ptr::addr_eq(
+        &raw const **result,
+        old(&raw const *self 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,11 @@ impl<A: Allocator> Box<dyn Any + Send, A> {
     /// [`downcast`]: Self::downcast
     #[inline]
     #[unstable(feature = "downcast_unchecked", issue = "90850")]
+    #[requires(self.is::<T>())]
+    #[ensures(|result: &Box<T, A>| core::ptr::addr_eq(
+        &raw const **result,
+        old(&raw const *self 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 +500,11 @@ 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: &Box<T, A>| core::ptr::addr_eq(
+        &raw const **result,
+        old(&raw const *self 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 +774,339 @@ impl dyn Error + Send + Sync {
         })
     }
 }
+
+// Challenge 29
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use core::fmt;
+
+    use super::super::kani_box_harness_helpers::verifier_nondet_vec_box;
+    use super::*;
+    use crate::string::String;
+
+    macro_rules! unchecked_downcast {
+        ($name:ident, $object:ty, $ty:ty, $target:path) => {
+            #[kani::proof_for_contract($target)]
+            fn $name() {
+                let erased: Box<$object> = Box::new(kani::any::<$ty>());
+                let result: Box<$ty> = unsafe { erased.downcast_unchecked::<$ty>() };
+                kani::cover(true, "downcast_unchecked precondition is reachable");
+            }
+        };
+    }
+
+    unchecked_downcast!(
+        harness_box_dyn_any_downcast_unchecked_i32,
+        dyn Any,
+        i32,
+        Box::<dyn core::any::Any + 'static, A>::downcast_unchecked::<i32>
+    );
+    unchecked_downcast!(
+        harness_box_dyn_any_downcast_unchecked_unit,
+        dyn Any,
+        (),
+        Box::<dyn core::any::Any + 'static, A>::downcast_unchecked::<()>
+    );
+
+    unchecked_downcast!(
+        harness_box_dyn_any_send_downcast_unchecked_i32,
+        dyn Any + Send,
+        i32,
+        Box::<dyn core::any::Any + core::marker::Send + 'static, A>::downcast_unchecked::<i32>
+    );
+    unchecked_downcast!(
+        harness_box_dyn_any_send_downcast_unchecked_unit,
+        dyn Any + Send,
+        (),
+        Box::<dyn core::any::Any + core::marker::Send + 'static, A>::downcast_unchecked::<()>
+    );
+
+    unchecked_downcast!(
+        harness_box_dyn_any_send_sync_downcast_unchecked_i32,
+        dyn Any + Send + Sync,
+        i32,
+        Box::<dyn core::any::Any + core::marker::Send + core::marker::Sync + 'static, A>::downcast_unchecked::<i32>
+    );
+    unchecked_downcast!(
+        harness_box_dyn_any_send_sync_downcast_unchecked_unit,
+        dyn Any + Send + Sync,
+        (),
+        Box::<dyn core::any::Any + core::marker::Send + core::marker::Sync + 'static, A>::downcast_unchecked::<()>
+    );
+
+    // Checks the named Box<dyn Any...>::downcast or <dyn Error...>::downcast.
+    // A symbolic choice checks both branches, including the Error wrappers that
+    // restore Send/Sync on failure after delegating to dyn Error::downcast.
+    macro_rules! checked_downcast {
+        ($name:ident, $object:ty, $ty:ty, $value:expr, $mismatch:expr) => {
+            #[kani::proof]
+            fn $name() {
+                let matches: bool = kani::any();
+                let erased: Box<$object> =
+                    if matches { Box::new($value) } else { Box::new($mismatch) };
+                assert_eq!(erased.downcast::<$ty>().is_ok(), matches);
+                kani::cover(matches, "Box::downcast succeeds for matching type");
+                kani::cover(!matches, "Box::downcast returns Err for mismatched type");
+            }
+        };
+    }
+
+    checked_downcast!(
+        harness_box_dyn_any_downcast_i32,
+        dyn Any,
+        i32,
+        kani::any::<i32>(),
+        String::from("mismatch")
+    );
+    checked_downcast!(harness_box_dyn_any_downcast_unit, dyn Any, (), (), String::from("mismatch"));
+    checked_downcast!(
+        harness_box_dyn_any_send_downcast_i32,
+        dyn Any + Send,
+        i32,
+        kani::any::<i32>(),
+        String::from("mismatch")
+    );
+    checked_downcast!(
+        harness_box_dyn_any_send_downcast_unit,
+        dyn Any + Send,
+        (),
+        (),
+        String::from("mismatch")
+    );
+    checked_downcast!(
+        harness_box_dyn_any_send_sync_downcast_i32,
+        dyn Any + Send + Sync,
+        i32,
+        kani::any::<i32>(),
+        String::from("mismatch")
+    );
+    checked_downcast!(
+        harness_box_dyn_any_send_sync_downcast_unit,
+        dyn Any + Send + Sync,
+        (),
+        (),
+        String::from("mismatch")
+    );
+
+    #[derive(Debug)]
+    struct Witness<T>(T);
+
+    impl<T: fmt::Debug> fmt::Display for Witness<T> {
+        fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
+            f.write_str("witness")
+        }
+    }
+
+    impl<T: fmt::Debug> Error for Witness<T> {}
+
+    checked_downcast!(
+        harness_box_dyn_error_downcast_byte,
+        dyn Error,
+        Witness<u8>,
+        Witness(kani::any::<u8>()),
+        fmt::Error
+    );
+    checked_downcast!(
+        harness_box_dyn_error_downcast_unit,
+        dyn Error,
+        Witness<()>,
+        Witness(()),
+        fmt::Error
+    );
+    checked_downcast!(
+        harness_box_dyn_error_send_downcast_byte,
+        dyn Error + Send,
+        Witness<u8>,
+        Witness(kani::any::<u8>()),
+        fmt::Error
+    );
+    checked_downcast!(
+        harness_box_dyn_error_send_downcast_unit,
+        dyn Error + Send,
+        Witness<()>,
+        Witness(()),
+        fmt::Error
+    );
+    checked_downcast!(
+        harness_box_dyn_error_send_sync_downcast_byte,
+        dyn Error + Send + Sync,
+        Witness<u8>,
+        Witness(kani::any::<u8>()),
+        fmt::Error
+    );
+    checked_downcast!(
+        harness_box_dyn_error_send_sync_downcast_unit,
+        dyn Error + Send + Sync,
+        Witness<()>,
+        Witness(()),
+        fmt::Error
+    );
+
+    // Independent symbolic ASCII bytes make every prefix a valid UTF-8 string.
+    fn symbolic_ascii_bytes() -> [u8; 8] {
+        let mut bytes: [u8; 8] = kani::any();
+        bytes[0] &= 0x7f;
+        bytes[1] &= 0x7f;
+        bytes[2] &= 0x7f;
+        bytes[3] &= 0x7f;
+        bytes[4] &= 0x7f;
+        bytes[5] &= 0x7f;
+        bytes[6] &= 0x7f;
+        bytes[7] &= 0x7f;
+        bytes
+    }
+
+    /// Checks <Box<str> as From<&str>>::from for empty and nonempty input.
+    #[kani::proof]
+    fn harness_box_from_str() {
+        let source = symbolic_ascii_bytes();
+        let len = kani::any_where(|len: &usize| *len <= source.len());
+        let ascii = core::str::from_utf8(&source).unwrap();
+        let value = ascii.get(..len).unwrap();
+        let boxed = Box::<str>::from(value);
+        assert_eq!(boxed.len(), value.len());
+        // Compare an arbitrary byte without introducing a memcmp loop.
+        if !value.is_empty() {
+            let index = kani::any_where(|i: &usize| *i < value.len());
+            assert_eq!(boxed.as_bytes()[index], value.as_bytes()[index]);
+        }
+        kani::cover(value.is_empty(), "Box::from str handles empty input");
+        kani::cover(!value.is_empty(), "Box::from str handles nonempty input");
+    }
+
+    /// Checks <Box<[u8]> as From<Box<str>>>::from.
+    #[kani::proof]
+    fn harness_box_from_box_str_to_u8_slice() {
+        let source = symbolic_ascii_bytes();
+        let len = kani::any_where(|len: &usize| *len <= source.len());
+        let ascii = core::str::from_utf8(&source).unwrap();
+        let value = ascii.get(..len).unwrap();
+        let boxed = Box::<str>::from(value);
+        let address = boxed.as_ptr();
+        let bytes = Box::<[u8]>::from(boxed);
+        assert_eq!(bytes.as_ptr(), address);
+        assert_eq!(bytes.len(), value.len());
+        // Compare an arbitrary byte without introducing a memcmp loop.
+        if !value.is_empty() {
+            let index = kani::any_where(|i: &usize| *i < value.len());
+            assert_eq!(bytes[index], value.as_bytes()[index]);
+        }
+        kani::cover(value.is_empty(), "Box<str> to bytes handles empty input");
+        kani::cover(!value.is_empty(), "Box<str> to bytes handles nonempty input");
+    }
+
+    /// Checks From<&[u8]> through CloneToUninit's TrivialClone slice specialization.
+    #[kani::proof]
+    fn harness_box_from_slice_trivial_clone() {
+        let source = verifier_nondet_vec_box::<u8>();
+        let boxed = Box::<[u8]>::from(source.as_slice());
+        assert_eq!(boxed.len(), source.len());
+        // A symbolic index checks copying without iterating over the unbounded length.
+        if !source.is_empty() {
+            let index = kani::any_where(|i: &usize| *i < source.len());
+            assert_eq!(boxed[index], source[index]);
+        }
+        kani::cover(source.is_empty(), "Box::from slice trivial clone handles empty input");
+        kani::cover(!source.is_empty(), "Box::from slice trivial clone copies an element");
+    }
+
+    // Deriving Clone alone does not implement TrivialClone, so CopySpec uses
+    // its generic element-wise Clone implementation.
+    #[derive(Clone)]
+    struct CloneOnly(u8);
+
+    /// Checks From<&[CloneOnly]> through CloneToUninit's generic slice clone.
+    #[kani::proof]
+    #[kani::unwind(3)]
+    fn harness_box_from_slice_clone() {
+        // This element-wise clone path uses a bounded, independently symbolic
+        // payload, including an empty slice. Other slice harnesses retain their
+        // symbolic lengths without a small fixed cap.
+        let values = [CloneOnly(kani::any()), CloneOnly(kani::any())];
+        let source = kani::slice::any_slice_of_array(&values);
+        let boxed = Box::<[CloneOnly]>::from(source);
+        assert_eq!(boxed.len(), source.len());
+        if !source.is_empty() {
+            let index = kani::any_where(|i: &usize| *i < source.len());
+            assert_eq!(boxed[index].0, source[index].0);
+        }
+        kani::cover(source.is_empty(), "Box::from slice clone handles empty input");
+        kani::cover(!source.is_empty(), "Box::from slice clone copies an element");
+    }
+
+    // N = 0 and N = 2 cover empty/nonempty targets.
+    macro_rules! slice_to_array {
+        ($name:ident, $ty:ty, $n:expr) => {
+            mod $name {
+                use super::*;
+                const N: usize = $n;
+
+                /// Checks TryFrom<Box<[T]>> for Box<[T; N]>.
+                #[kani::proof]
+                fn boxed_slice() {
+                    let boxed = if N == 0 {
+                        // Bound this setup to 10 elements to work around CBMC's vector::reserve error.
+                        let values: [$ty; 10] = kani::any();
+                        Box::<[$ty]>::from(kani::slice::any_slice_of_array(&values))
+                    } else {
+                        verifier_nondet_vec_box::<$ty>().into_boxed_slice()
+                    };
+                    let (len, address) = (boxed.len(), boxed.as_ptr());
+                    let index = if len == 0 { 0 } else { kani::any_where(|i: &usize| *i < len) };
+                    let expected = boxed.get(index).copied();
+                    let recovered: Box<[$ty]> = match Box::<[$ty; N]>::try_from(boxed) {
+                        Ok(array) => {
+                            assert_eq!(len, N);
+                            array
+                        }
+                        Err(rest) => {
+                            assert_ne!(len, N);
+                            rest
+                        }
+                    };
+                    assert_eq!(recovered.len(), len);
+                    assert_eq!(recovered.as_ptr(), address);
+                    assert_eq!(recovered.get(index).copied(), expected);
+                    kani::cover(len == N, "Box slice to array accepts matching length");
+                    kani::cover(len != N, "Box slice to array rejects mismatched length");
+                }
+
+                /// Checks TryFrom<Vec<T>> for Box<[T; N]>.
+                #[kani::proof]
+                fn vector() {
+                    let vec = verifier_nondet_vec_box::<$ty>();
+                    let (len, capacity, address) = (vec.len(), vec.capacity(), vec.as_ptr());
+                    let index = if len == 0 { 0 } else { kani::any_where(|i: &usize| *i < len) };
+                    let expected = vec.get(index).copied();
+                    let result = Box::<[$ty; N]>::try_from(vec);
+                    let recovered: &[$ty] = match &result {
+                        Ok(array) => {
+                            assert_eq!(len, N);
+                            // Excess capacity may legitimately require reallocation.
+                            if capacity == N {
+                                assert_eq!(array.as_ptr(), address);
+                            }
+                            &array[..]
+                        }
+                        Err(rest) => {
+                            assert_ne!(len, N);
+                            assert_eq!(rest.as_ptr(), address);
+                            assert_eq!(rest.capacity(), capacity);
+                            rest.as_slice()
+                        }
+                    };
+                    assert_eq!(recovered.len(), len);
+                    assert_eq!(recovered.get(index).copied(), expected);
+                    kani::cover(len == N, "Box Vec to array accepts matching length");
+                    kani::cover(len != N, "Box Vec to array rejects mismatched length");
+                }
+            }
+        };
+    }
+
+    slice_to_array!(harness_box_try_from_array_i32, i32, 2);
+    slice_to_array!(harness_box_try_from_array_unit, (), 2);
+    slice_to_array!(harness_box_try_from_array_empty, u8, 0);
+}
diff --git a/library/alloc/src/boxed/thin.rs b/library/alloc/src/boxed/thin.rs
index 90bb2ef9b838c..41a2a04a969be 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;
@@ -15,6 +17,8 @@ use core::mem::SizedTypeProperties;
 use core::ops::{Deref, DerefMut};
 use core::ptr::{self, NonNull, Pointee};
 
+use safety::requires;
+
 use crate::alloc::{self, Layout, LayoutError};
 
 /// ThinBox.
@@ -373,6 +377,10 @@ impl<H> WithHeader<H> {
     ///
     /// `value` must point to an undropped owned `T`, and `self` must not be
     /// accessed again after this is called.
+    #[requires(
+        value.cast::<u8>() == self.0.as_ptr()
+            && core::ub_checks::can_dereference(value)
+    )]
     unsafe fn drop<T: ?Sized>(&self, value: *mut T) {
         struct DropGuard<H> {
             ptr: NonNull<u8>,
@@ -453,3 +461,180 @@ impl<T> From<T> for ThinBox<T> {
         Self::new(value)
     }
 }
+
+// Challenge 29
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use core::any::Any;
+
+    use super::*;
+
+    // Each expansion has a separate named target, with sized, ZST, slice
+    // and vtable metadata. The u128 trait-object payload exercises padding when
+    // value alignment exceeds metadata alignment on the verification target.
+    macro_rules! thinbox_harnesses {
+        ($module:ident, $target:literal, |$thin:ident| $body:block) => {
+            mod $module {
+                use super::*;
+
+                #[doc = $target]
+                fn check<T: ?Sized>($thin: ThinBox<T>) {
+                    $body
+                    kani::cover(true, $target);
+                }
+
+                #[kani::proof]
+                fn sized() { check(ThinBox::new(kani::any::<i32>())); }
+
+                #[kani::proof]
+                fn zst() { check(ThinBox::new(())); }
+
+                #[kani::proof]
+                fn slice() {
+                    check(ThinBox::<[u8]>::new_unsize(kani::any::<[u8; 4]>()));
+                }
+
+                #[kani::proof]
+                fn dyn_any() {
+                    check(ThinBox::<dyn Any>::new_unsize(kani::any::<u128>()));
+                }
+            }
+        };
+    }
+
+    thinbox_harnesses!(harness_thinbox_deref, "Checks ThinBox::deref.", |thin| {
+        let expected_data = thin.ptr.0.as_ptr();
+        let expected_metadata = unsafe { *thin.with_header().header() };
+        let value = Deref::deref(&thin);
+        assert_eq!(ptr::from_ref(value).cast::<u8>(), expected_data.cast_const());
+        assert_eq!(ptr::metadata(value), expected_metadata);
+    });
+    thinbox_harnesses!(harness_thinbox_deref_mut, "Checks ThinBox::deref_mut.", |thin| {
+        let mut thin = thin;
+        let expected_data = thin.ptr.0.as_ptr();
+        let expected_metadata = unsafe { *thin.with_header().header() };
+        let value = DerefMut::deref_mut(&mut thin);
+        assert_eq!(ptr::from_mut(value).cast::<u8>(), expected_data);
+        assert_eq!(ptr::metadata(value), expected_metadata);
+    });
+    thinbox_harnesses!(harness_thinbox_drop, "Checks <ThinBox<T> as Drop>::drop.", |thin| {
+        drop(thin);
+    });
+    thinbox_harnesses!(harness_thinbox_meta, "Checks ThinBox::meta.", |thin| {
+        let expected = unsafe { *thin.with_header().header() };
+        assert_eq!(thin.meta(), expected);
+    });
+    thinbox_harnesses!(harness_thinbox_with_header, "Checks ThinBox::with_header.", |thin| {
+        assert_eq!(thin.with_header().value(), thin.ptr.0.as_ptr());
+    });
+    thinbox_harnesses!(harness_with_header_header, "Checks WithHeader::header.", |thin| {
+        let header = thin.with_header().header();
+        assert!(header.is_aligned());
+        assert!(core::ub_checks::can_dereference(header));
+        assert_eq!(unsafe { header.add(1) }.cast::<u8>(), thin.ptr.0.as_ptr());
+    });
+
+    // Constructor harnesses have distinct targets. Rewrapping transfers the
+    // allocation to ThinBox so cleanup also checks the stored metadata/layout.
+    fn into_thin<T: ?Sized>(header: WithHeader<<T as Pointee>::Metadata>) -> ThinBox<T> {
+        ThinBox { ptr: WithOpaqueHeader(header.0), _marker: PhantomData }
+    }
+
+    macro_rules! header_constructors {
+        ($module:ident, $dst:ty, $value:expr) => {
+            mod $module {
+                use super::*;
+
+                /// Checks WithHeader::new.
+                #[kani::proof]
+                fn new() {
+                    let value = $value;
+                    let metadata = ptr::metadata(&value as &$dst);
+                    let layout = Layout::for_value(&value);
+                    let thin = into_thin::<$dst>(WithHeader::new(metadata, value));
+                    assert_eq!(ptr::metadata(&*thin), metadata);
+                    assert_eq!(Layout::for_value(&*thin), layout);
+                    kani::cover(true, "WithHeader::new preserves metadata and value layout");
+                }
+
+                /// Checks WithHeader::try_new, retaining its fallible result.
+                #[kani::proof]
+                fn try_new() {
+                    let value = $value;
+                    let metadata = ptr::metadata(&value as &$dst);
+                    let layout = Layout::for_value(&value);
+                    if let Ok(header) = WithHeader::try_new(metadata, value) {
+                        let thin = into_thin::<$dst>(header);
+                        assert_eq!(ptr::metadata(&*thin), metadata);
+                        assert_eq!(Layout::for_value(&*thin), layout);
+                        kani::cover(
+                            true,
+                            "WithHeader::try_new preserves metadata and value layout",
+                        );
+                    }
+                    kani::cover(true, "WithHeader::try_new returns");
+                }
+            }
+        };
+    }
+
+    header_constructors!(harness_with_header_sized, i32, kani::any::<i32>());
+    header_constructors!(harness_with_header_zst, (), ());
+    header_constructors!(harness_with_header_slice, [u8], kani::any::<[u8; 4]>());
+    header_constructors!(harness_with_header_dyn_any, dyn Any, kani::any::<u128>());
+
+    /// Checks WithHeader::new_unsize_zst with slice metadata.
+    #[kani::proof]
+    fn harness_with_header_new_unsize_zst_slice() {
+        let header = WithHeader::<usize>::new_unsize_zst::<[u8], [u8; 0]>([]);
+        let thin = into_thin::<[u8]>(header);
+        assert!(thin.is_empty());
+        kani::cover(true, "WithHeader::new_unsize_zst preserves empty slice metadata");
+    }
+
+    /// Checks WithHeader::new_unsize_zst with vtable metadata.
+    #[kani::proof]
+    fn harness_with_header_new_unsize_zst_dyn_any() {
+        let header =
+            WithHeader::<<dyn Any as Pointee>::Metadata>::new_unsize_zst::<dyn Any, ()>(());
+        let metadata = unsafe { *header.header() };
+        assert_eq!(metadata.size_of(), size_of::<()>());
+        assert_eq!(metadata.align_of(), mem::align_of::<()>());
+        kani::cover(true, "WithHeader::new_unsize_zst preserves unit size and alignment");
+    }
+
+    // Non-ZST drop uses ordinary proofs because Kani contracts cannot express
+    // permission to free the allocation created by the harness. Explicitly
+    // check the requires clause before executing the real body; these are body
+    // checks, not proof_for_contract evidence. Keep them in sync with requires.
+    // WithHeader has no Drop impl, so cleanup does not call the target again.
+    #[kani::proof]
+    fn harness_with_header_drop_sized() {
+        let header = WithHeader::new((), kani::any::<i32>());
+        let value = header.value().cast::<i32>();
+        assert_eq!(value.cast::<u8>(), header.0.as_ptr());
+        assert!(core::ub_checks::can_dereference(value));
+        unsafe { header.drop(value) };
+        kani::cover(true, "WithHeader::drop completes for a sized value");
+    }
+
+    // ZST drop does not deallocate, so it retains direct contract checking.
+    #[kani::proof_for_contract(WithHeader::drop)]
+    fn harness_with_header_drop_zst() {
+        let header = WithHeader::new((), ());
+        unsafe { header.drop(header.value().cast::<()>()) };
+        kani::cover(true, "WithHeader::drop completes for a ZST");
+    }
+
+    #[kani::proof]
+    fn harness_with_header_drop_slice() {
+        let header = WithHeader::new(2usize, kani::any::<[u128; 2]>());
+        let value = ptr::slice_from_raw_parts_mut(header.value().cast::<u128>(), 2);
+        assert_eq!(value.cast::<u8>(), header.0.as_ptr());
+        assert!(core::ub_checks::can_dereference(value));
+        unsafe { header.drop(value) };
+        kani::cover(true, "WithHeader::drop completes for a slice");
+    }
+}