diff --git a/library/core/src/intrinsics/mod.rs b/library/core/src/intrinsics/mod.rs
index a12705189fb04..0077f38b820fe 100644
--- a/library/core/src/intrinsics/mod.rs
+++ b/library/core/src/intrinsics/mod.rs
@@ -4682,6 +4682,602 @@ mod verify {
     fn supported_status(status: AllocationStatus) -> bool {
         status != AllocationStatus::Dangling && status != AllocationStatus::DeadObject
     }
+
+    // Challenge 7, Part 3: atomic intrinsic contracts.
+    //
+    // Kani cannot currently attach contracts directly to bodyless
+    // `rustc_intrinsic` declarations (model-checking/kani#3345). These wrappers
+    // are the Kani-facing specifications for the const-generic intrinsics above.
+    // The harness instantiations follow the integer and pointer restrictions in
+    // the intrinsic documentation, while the contracts encode only the local
+    // memory obligations required by the intrinsic calls.
+    //
+    // `can_dereference` and `can_write` express local memory requirements for `T`.
+    // Checking initialization through `can_dereference` requires `-Z uninit-checks`.
+    // These single-threaded proofs do not establish the absence of data races or
+    // unsynchronized mixed-size overlapping atomic accesses. The load and store
+    // wrappers cover non-volatile accesses only; volatile accesses have separate
+    // safety requirements.
+
+    #[allow(dead_code)]
+    #[kani::modifies(dst)]
+    #[requires(crate::ub_checks::can_write(dst))]
+    unsafe fn atomic_store_wrapper<T: Copy, const ORD: AtomicOrdering>(dst: *mut T, val: T) {
+        unsafe { atomic_store::<T, ORD, false>(dst, val) }
+    }
+
+    #[allow(dead_code)]
+    #[requires(crate::ub_checks::can_dereference(src))]
+    unsafe fn atomic_load_wrapper<T: Copy, const ORD: AtomicOrdering>(src: *const T) -> T {
+        unsafe { atomic_load::<T, ORD, false>(src) }
+    }
+
+    #[allow(dead_code)]
+    #[kani::modifies(dst)]
+    #[requires(crate::ub_checks::can_dereference(dst as *const T))]
+    #[requires(crate::ub_checks::can_write(dst))]
+    unsafe fn atomic_xchg_wrapper<T: Copy, const ORD: AtomicOrdering>(dst: *mut T, val: T) -> T {
+        unsafe { atomic_xchg::<T, ORD>(dst, val) }
+    }
+
+    macro_rules! define_atomic_binary_rmw_wrapper {
+        ($wrapper:ident, $intrinsic:ident) => {
+            #[allow(dead_code)]
+            #[kani::modifies(dst)]
+            #[requires(crate::ub_checks::can_dereference(dst as *const T))]
+            #[requires(crate::ub_checks::can_write(dst))]
+            unsafe fn $wrapper<T: Copy, U: Copy, const ORD: AtomicOrdering>(
+                dst: *mut T,
+                val: U,
+            ) -> T {
+                unsafe { $intrinsic::<T, U, ORD>(dst, val) }
+            }
+        };
+    }
+
+    define_atomic_binary_rmw_wrapper!(atomic_xadd_wrapper, atomic_xadd);
+    define_atomic_binary_rmw_wrapper!(atomic_xsub_wrapper, atomic_xsub);
+    define_atomic_binary_rmw_wrapper!(atomic_and_wrapper, atomic_and);
+    define_atomic_binary_rmw_wrapper!(atomic_nand_wrapper, atomic_nand);
+    define_atomic_binary_rmw_wrapper!(atomic_or_wrapper, atomic_or);
+    define_atomic_binary_rmw_wrapper!(atomic_xor_wrapper, atomic_xor);
+
+    macro_rules! define_atomic_extremum_wrapper {
+        ($wrapper:ident, $intrinsic:ident) => {
+            #[allow(dead_code)]
+            #[kani::modifies(dst)]
+            #[requires(crate::ub_checks::can_dereference(dst as *const T))]
+            #[requires(crate::ub_checks::can_write(dst))]
+            unsafe fn $wrapper<T: Copy, const ORD: AtomicOrdering>(dst: *mut T, val: T) -> T {
+                unsafe { $intrinsic::<T, ORD>(dst, val) }
+            }
+        };
+    }
+
+    define_atomic_extremum_wrapper!(atomic_max_wrapper, atomic_max);
+    define_atomic_extremum_wrapper!(atomic_min_wrapper, atomic_min);
+    define_atomic_extremum_wrapper!(atomic_umax_wrapper, atomic_umax);
+    define_atomic_extremum_wrapper!(atomic_umin_wrapper, atomic_umin);
+
+    macro_rules! define_atomic_compare_exchange_wrapper {
+        ($wrapper:ident, $intrinsic:ident) => {
+            #[allow(dead_code)]
+            #[kani::modifies(dst)]
+            #[requires(crate::ub_checks::can_dereference(dst as *const T))]
+            #[requires(crate::ub_checks::can_write(dst))]
+            unsafe fn $wrapper<
+                T: Copy,
+                const ORD_SUCC: AtomicOrdering,
+                const ORD_FAIL: AtomicOrdering,
+            >(
+                dst: *mut T,
+                old: T,
+                new: T,
+            ) -> (T, bool) {
+                unsafe { $intrinsic::<T, ORD_SUCC, ORD_FAIL>(dst, old, new) }
+            }
+        };
+    }
+
+    define_atomic_compare_exchange_wrapper!(atomic_cxchg_wrapper, atomic_cxchg);
+    define_atomic_compare_exchange_wrapper!(atomic_cxchgweak_wrapper, atomic_cxchgweak);
+
+    // Every ordering-specific harness below expands to every legal integer
+    // width and to the pointer form.  Storage is a local object, so the raw
+    // pointer passed to the intrinsic has concrete provenance without a
+    // separate wrapper type. Pointer *values* remain arbitrary addresses.
+    macro_rules! atomic_integer_load_store_types {
+        ($call:ident, $($args:tt)*) => {
+            #[cfg(target_has_atomic_load_store = "8")] { $call!(i8, $($args)*); $call!(u8, $($args)*); }
+            #[cfg(target_has_atomic_load_store = "16")] { $call!(i16, $($args)*); $call!(u16, $($args)*); }
+            #[cfg(target_has_atomic_load_store = "32")] { $call!(i32, $($args)*); $call!(u32, $($args)*); }
+            #[cfg(target_has_atomic_load_store = "64")] { $call!(i64, $($args)*); $call!(u64, $($args)*); }
+            #[cfg(target_has_atomic_load_store = "128")] { $call!(i128, $($args)*); $call!(u128, $($args)*); }
+            #[cfg(target_has_atomic_load_store = "ptr")] { $call!(isize, $($args)*); $call!(usize, $($args)*); }
+        };
+    }
+
+    macro_rules! atomic_integer_types {
+        ($call:ident, $($args:tt)*) => {
+            #[cfg(target_has_atomic = "8")] { $call!(i8, $($args)*); $call!(u8, $($args)*); }
+            #[cfg(target_has_atomic = "16")] { $call!(i16, $($args)*); $call!(u16, $($args)*); }
+            #[cfg(target_has_atomic = "32")] { $call!(i32, $($args)*); $call!(u32, $($args)*); }
+            #[cfg(target_has_atomic = "64")] { $call!(i64, $($args)*); $call!(u64, $($args)*); }
+            #[cfg(target_has_atomic = "128")] { $call!(i128, $($args)*); $call!(u128, $($args)*); }
+            #[cfg(target_has_atomic = "ptr")] { $call!(isize, $($args)*); $call!(usize, $($args)*); }
+        };
+    }
+
+    macro_rules! atomic_signed_types {
+        ($call:ident, $($args:tt)*) => {
+            #[cfg(target_has_atomic = "8")] { $call!(i8, $($args)*); }
+            #[cfg(target_has_atomic = "16")] { $call!(i16, $($args)*); }
+            #[cfg(target_has_atomic = "32")] { $call!(i32, $($args)*); }
+            #[cfg(target_has_atomic = "64")] { $call!(i64, $($args)*); }
+            #[cfg(target_has_atomic = "128")] { $call!(i128, $($args)*); }
+            #[cfg(target_has_atomic = "ptr")] { $call!(isize, $($args)*); }
+        };
+    }
+
+    macro_rules! atomic_unsigned_types {
+        ($call:ident, $($args:tt)*) => {
+            #[cfg(target_has_atomic = "8")] { $call!(u8, $($args)*); }
+            #[cfg(target_has_atomic = "16")] { $call!(u16, $($args)*); }
+            #[cfg(target_has_atomic = "32")] { $call!(u32, $($args)*); }
+            #[cfg(target_has_atomic = "64")] { $call!(u64, $($args)*); }
+            #[cfg(target_has_atomic = "128")] { $call!(u128, $($args)*); }
+            #[cfg(target_has_atomic = "ptr")] { $call!(usize, $($args)*); }
+        };
+    }
+
+    // Store: integer and pointer T, with the three orderings accepted by the
+    // intrinsic's stabilized atomic counterpart.
+    macro_rules! atomic_store_call {
+        ($ty:ty, $ord:path) => {{
+            let mut dst: $ty = kani::any();
+            let val: $ty = kani::any();
+            unsafe { atomic_store_wrapper::<$ty, { $ord }>(&mut dst, val) };
+        }};
+    }
+    macro_rules! atomic_store_harness {
+        ($name:ident, $ord:path) => {
+            #[kani::proof_for_contract(atomic_store_wrapper)]
+            fn $name() {
+                atomic_integer_load_store_types!(atomic_store_call, $ord);
+                #[cfg(target_has_atomic_load_store = "ptr")]
+                {
+                    let mut dst: *mut u8 = kani::any::<usize>() as *mut u8;
+                    let val: *mut u8 = kani::any::<usize>() as *mut u8;
+                    unsafe { atomic_store_wrapper::<*mut u8, { $ord }>(&mut dst, val) };
+                }
+                kani::cover(true, "atomic intrinsic store: reached after call");
+            }
+        };
+    }
+    atomic_store_harness!(harness_intrinsic_atomic_store_relaxed, AtomicOrdering::Relaxed);
+    atomic_store_harness!(harness_intrinsic_atomic_store_release, AtomicOrdering::Release);
+    atomic_store_harness!(harness_intrinsic_atomic_store_seqcst, AtomicOrdering::SeqCst);
+
+    // Load: the same complete T matrix as store.
+    macro_rules! atomic_load_call {
+        ($ty:ty, $ord:path) => {{
+            let src: $ty = kani::any();
+            let _ = unsafe { atomic_load_wrapper::<$ty, { $ord }>(&src) };
+        }};
+    }
+    macro_rules! atomic_load_harness {
+        ($name:ident, $ord:path) => {
+            #[kani::proof_for_contract(atomic_load_wrapper)]
+            fn $name() {
+                atomic_integer_load_store_types!(atomic_load_call, $ord);
+                #[cfg(target_has_atomic_load_store = "ptr")]
+                {
+                    let src: *mut u8 = kani::any::<usize>() as *mut u8;
+                    let _ = unsafe { atomic_load_wrapper::<*mut u8, { $ord }>(&src) };
+                }
+                kani::cover(true, "atomic intrinsic load: reached after call");
+            }
+        };
+    }
+    atomic_load_harness!(harness_intrinsic_atomic_load_relaxed, AtomicOrdering::Relaxed);
+    atomic_load_harness!(harness_intrinsic_atomic_load_acquire, AtomicOrdering::Acquire);
+    atomic_load_harness!(harness_intrinsic_atomic_load_seqcst, AtomicOrdering::SeqCst);
+
+    // Unary RMW operations (swap, xchg): integer and pointer T.
+    macro_rules! atomic_rmw_call {
+        ($ty:ty, $wrapper:ident, $ord:path) => {{
+            let mut dst: $ty = kani::any();
+            let val: $ty = kani::any();
+            let _ = unsafe { $wrapper::<$ty, { $ord }>(&mut dst, val) };
+        }};
+    }
+    macro_rules! atomic_rmw_harness {
+        ($name:ident, $wrapper:ident, $ord:path) => {
+            #[kani::proof_for_contract($wrapper)]
+            fn $name() {
+                atomic_integer_types!(atomic_rmw_call, $wrapper, $ord);
+                #[cfg(target_has_atomic = "ptr")]
+                {
+                    let mut dst: *mut u8 = kani::any::<usize>() as *mut u8;
+                    let val: *mut u8 = kani::any::<usize>() as *mut u8;
+                    let _ = unsafe { $wrapper::<*mut u8, { $ord }>(&mut dst, val) };
+                }
+                kani::cover(true, "atomic intrinsic exchange: reached after call");
+            }
+        };
+    }
+    macro_rules! atomic_rmw_orders {
+        ($wrapper:ident, $relaxed:ident, $acquire:ident, $release:ident, $acqrel:ident, $seqcst:ident) => {
+            atomic_rmw_harness!($relaxed, $wrapper, AtomicOrdering::Relaxed);
+            atomic_rmw_harness!($acquire, $wrapper, AtomicOrdering::Acquire);
+            atomic_rmw_harness!($release, $wrapper, AtomicOrdering::Release);
+            atomic_rmw_harness!($acqrel, $wrapper, AtomicOrdering::AcqRel);
+            atomic_rmw_harness!($seqcst, $wrapper, AtomicOrdering::SeqCst);
+        };
+    }
+    atomic_rmw_orders!(
+        atomic_xchg_wrapper,
+        harness_intrinsic_atomic_xchg_relaxed,
+        harness_intrinsic_atomic_xchg_acquire,
+        harness_intrinsic_atomic_xchg_release,
+        harness_intrinsic_atomic_xchg_acqrel,
+        harness_intrinsic_atomic_xchg_seqcst
+    );
+
+    // Binary RMW operations: U == T for integer T, and U == usize for pointer T.
+    macro_rules! atomic_binary_call {
+        ($ty:ty, $wrapper:ident, $ord:path) => {{
+            let mut dst: $ty = kani::any();
+            let val: $ty = kani::any();
+            let _ = unsafe { $wrapper::<$ty, $ty, { $ord }>(&mut dst, val) };
+        }};
+    }
+    macro_rules! atomic_binary_harness {
+        ($name:ident, $wrapper:ident, $ord:path) => {
+            #[kani::proof_for_contract($wrapper)]
+            fn $name() {
+                atomic_integer_types!(atomic_binary_call, $wrapper, $ord);
+                #[cfg(target_has_atomic = "ptr")]
+                {
+                    let mut dst: *mut u8 = kani::any::<usize>() as *mut u8;
+                    let val: usize = kani::any();
+                    let _ = unsafe { $wrapper::<*mut u8, usize, { $ord }>(&mut dst, val) };
+                }
+                kani::cover(true, "atomic intrinsic binary RMW: reached after call");
+            }
+        };
+    }
+    macro_rules! atomic_binary_orders {
+        ($wrapper:ident, $relaxed:ident, $acquire:ident, $release:ident, $acqrel:ident, $seqcst:ident) => {
+            atomic_binary_harness!($relaxed, $wrapper, AtomicOrdering::Relaxed);
+            atomic_binary_harness!($acquire, $wrapper, AtomicOrdering::Acquire);
+            atomic_binary_harness!($release, $wrapper, AtomicOrdering::Release);
+            atomic_binary_harness!($acqrel, $wrapper, AtomicOrdering::AcqRel);
+            atomic_binary_harness!($seqcst, $wrapper, AtomicOrdering::SeqCst);
+        };
+    }
+    atomic_binary_orders!(
+        atomic_xadd_wrapper,
+        harness_intrinsic_atomic_xadd_relaxed,
+        harness_intrinsic_atomic_xadd_acquire,
+        harness_intrinsic_atomic_xadd_release,
+        harness_intrinsic_atomic_xadd_acqrel,
+        harness_intrinsic_atomic_xadd_seqcst
+    );
+    atomic_binary_orders!(
+        atomic_xsub_wrapper,
+        harness_intrinsic_atomic_xsub_relaxed,
+        harness_intrinsic_atomic_xsub_acquire,
+        harness_intrinsic_atomic_xsub_release,
+        harness_intrinsic_atomic_xsub_acqrel,
+        harness_intrinsic_atomic_xsub_seqcst
+    );
+    atomic_binary_orders!(
+        atomic_and_wrapper,
+        harness_intrinsic_atomic_and_relaxed,
+        harness_intrinsic_atomic_and_acquire,
+        harness_intrinsic_atomic_and_release,
+        harness_intrinsic_atomic_and_acqrel,
+        harness_intrinsic_atomic_and_seqcst
+    );
+    atomic_binary_orders!(
+        atomic_nand_wrapper,
+        harness_intrinsic_atomic_nand_relaxed,
+        harness_intrinsic_atomic_nand_acquire,
+        harness_intrinsic_atomic_nand_release,
+        harness_intrinsic_atomic_nand_acqrel,
+        harness_intrinsic_atomic_nand_seqcst
+    );
+    atomic_binary_orders!(
+        atomic_or_wrapper,
+        harness_intrinsic_atomic_or_relaxed,
+        harness_intrinsic_atomic_or_acquire,
+        harness_intrinsic_atomic_or_release,
+        harness_intrinsic_atomic_or_acqrel,
+        harness_intrinsic_atomic_or_seqcst
+    );
+    atomic_binary_orders!(
+        atomic_xor_wrapper,
+        harness_intrinsic_atomic_xor_relaxed,
+        harness_intrinsic_atomic_xor_acquire,
+        harness_intrinsic_atomic_xor_release,
+        harness_intrinsic_atomic_xor_acqrel,
+        harness_intrinsic_atomic_xor_seqcst
+    );
+
+    // Signed and unsigned extrema have the restricted T matrices documented by
+    // atomic_max/min and atomic_umax/umin respectively.
+    macro_rules! atomic_extremum_call {
+        ($ty:ty, $wrapper:ident, $ord:path) => {{
+            let mut dst: $ty = kani::any();
+            let val: $ty = kani::any();
+            let _ = unsafe { $wrapper::<$ty, { $ord }>(&mut dst, val) };
+        }};
+    }
+    macro_rules! atomic_extremum_harness {
+        ($name:ident, $wrapper:ident, $types:ident, $ord:path) => {
+            #[kani::proof_for_contract($wrapper)]
+            fn $name() {
+                $types!(atomic_extremum_call, $wrapper, $ord);
+                kani::cover(true, "atomic intrinsic extremum: reached after call");
+            }
+        };
+    }
+    macro_rules! atomic_extremum_orders {
+        ($wrapper:ident, $types:ident, $relaxed:ident, $acquire:ident, $release:ident, $acqrel:ident, $seqcst:ident) => {
+            atomic_extremum_harness!($relaxed, $wrapper, $types, AtomicOrdering::Relaxed);
+            atomic_extremum_harness!($acquire, $wrapper, $types, AtomicOrdering::Acquire);
+            atomic_extremum_harness!($release, $wrapper, $types, AtomicOrdering::Release);
+            atomic_extremum_harness!($acqrel, $wrapper, $types, AtomicOrdering::AcqRel);
+            atomic_extremum_harness!($seqcst, $wrapper, $types, AtomicOrdering::SeqCst);
+        };
+    }
+    atomic_extremum_orders!(
+        atomic_max_wrapper,
+        atomic_signed_types,
+        harness_intrinsic_atomic_max_relaxed,
+        harness_intrinsic_atomic_max_acquire,
+        harness_intrinsic_atomic_max_release,
+        harness_intrinsic_atomic_max_acqrel,
+        harness_intrinsic_atomic_max_seqcst
+    );
+    atomic_extremum_orders!(
+        atomic_min_wrapper,
+        atomic_signed_types,
+        harness_intrinsic_atomic_min_relaxed,
+        harness_intrinsic_atomic_min_acquire,
+        harness_intrinsic_atomic_min_release,
+        harness_intrinsic_atomic_min_acqrel,
+        harness_intrinsic_atomic_min_seqcst
+    );
+    atomic_extremum_orders!(
+        atomic_umax_wrapper,
+        atomic_unsigned_types,
+        harness_intrinsic_atomic_umax_relaxed,
+        harness_intrinsic_atomic_umax_acquire,
+        harness_intrinsic_atomic_umax_release,
+        harness_intrinsic_atomic_umax_acqrel,
+        harness_intrinsic_atomic_umax_seqcst
+    );
+    atomic_extremum_orders!(
+        atomic_umin_wrapper,
+        atomic_unsigned_types,
+        harness_intrinsic_atomic_umin_relaxed,
+        harness_intrinsic_atomic_umin_acquire,
+        harness_intrinsic_atomic_umin_release,
+        harness_intrinsic_atomic_umin_acqrel,
+        harness_intrinsic_atomic_umin_seqcst
+    );
+
+    // Compare exchange uses all integer/pointer T types for every legal
+    // success/failure ordering pair. Failure orderings are exactly the three
+    // values listed in the intrinsic documentation.
+    macro_rules! atomic_cxchg_call {
+        ($ty:ty, $wrapper:ident, $succ:path, $fail:path) => {{
+            let mut dst: $ty = kani::any();
+            let old: $ty = kani::any();
+            let new: $ty = kani::any();
+            let _ = unsafe { $wrapper::<$ty, { $succ }, { $fail }>(&mut dst, old, new) };
+        }};
+    }
+    macro_rules! atomic_cxchg_harness {
+        ($name:ident, $wrapper:ident, $succ:path, $fail:path) => {
+            #[kani::proof_for_contract($wrapper)]
+            fn $name() {
+                atomic_integer_types!(atomic_cxchg_call, $wrapper, $succ, $fail);
+                #[cfg(target_has_atomic = "ptr")]
+                {
+                    let mut dst: *mut u8 = kani::any::<usize>() as *mut u8;
+                    let old: *mut u8 = kani::any::<usize>() as *mut u8;
+                    let new: *mut u8 = kani::any::<usize>() as *mut u8;
+                    let _ =
+                        unsafe { $wrapper::<*mut u8, { $succ }, { $fail }>(&mut dst, old, new) };
+                }
+                kani::cover(true, "atomic intrinsic compare-exchange: reached after call");
+            }
+        };
+    }
+    atomic_cxchg_harness!(
+        harness_intrinsic_atomic_cxchg_relaxed_relaxed,
+        atomic_cxchg_wrapper,
+        AtomicOrdering::Relaxed,
+        AtomicOrdering::Relaxed
+    );
+    atomic_cxchg_harness!(
+        harness_intrinsic_atomic_cxchg_relaxed_acquire,
+        atomic_cxchg_wrapper,
+        AtomicOrdering::Relaxed,
+        AtomicOrdering::Acquire
+    );
+    atomic_cxchg_harness!(
+        harness_intrinsic_atomic_cxchg_relaxed_seqcst,
+        atomic_cxchg_wrapper,
+        AtomicOrdering::Relaxed,
+        AtomicOrdering::SeqCst
+    );
+    atomic_cxchg_harness!(
+        harness_intrinsic_atomic_cxchg_acquire_relaxed,
+        atomic_cxchg_wrapper,
+        AtomicOrdering::Acquire,
+        AtomicOrdering::Relaxed
+    );
+    atomic_cxchg_harness!(
+        harness_intrinsic_atomic_cxchg_acquire_acquire,
+        atomic_cxchg_wrapper,
+        AtomicOrdering::Acquire,
+        AtomicOrdering::Acquire
+    );
+    atomic_cxchg_harness!(
+        harness_intrinsic_atomic_cxchg_acquire_seqcst,
+        atomic_cxchg_wrapper,
+        AtomicOrdering::Acquire,
+        AtomicOrdering::SeqCst
+    );
+    atomic_cxchg_harness!(
+        harness_intrinsic_atomic_cxchg_release_relaxed,
+        atomic_cxchg_wrapper,
+        AtomicOrdering::Release,
+        AtomicOrdering::Relaxed
+    );
+    atomic_cxchg_harness!(
+        harness_intrinsic_atomic_cxchg_release_acquire,
+        atomic_cxchg_wrapper,
+        AtomicOrdering::Release,
+        AtomicOrdering::Acquire
+    );
+    atomic_cxchg_harness!(
+        harness_intrinsic_atomic_cxchg_release_seqcst,
+        atomic_cxchg_wrapper,
+        AtomicOrdering::Release,
+        AtomicOrdering::SeqCst
+    );
+    atomic_cxchg_harness!(
+        harness_intrinsic_atomic_cxchg_acqrel_relaxed,
+        atomic_cxchg_wrapper,
+        AtomicOrdering::AcqRel,
+        AtomicOrdering::Relaxed
+    );
+    atomic_cxchg_harness!(
+        harness_intrinsic_atomic_cxchg_acqrel_acquire,
+        atomic_cxchg_wrapper,
+        AtomicOrdering::AcqRel,
+        AtomicOrdering::Acquire
+    );
+    atomic_cxchg_harness!(
+        harness_intrinsic_atomic_cxchg_acqrel_seqcst,
+        atomic_cxchg_wrapper,
+        AtomicOrdering::AcqRel,
+        AtomicOrdering::SeqCst
+    );
+    atomic_cxchg_harness!(
+        harness_intrinsic_atomic_cxchg_seqcst_relaxed,
+        atomic_cxchg_wrapper,
+        AtomicOrdering::SeqCst,
+        AtomicOrdering::Relaxed
+    );
+    atomic_cxchg_harness!(
+        harness_intrinsic_atomic_cxchg_seqcst_acquire,
+        atomic_cxchg_wrapper,
+        AtomicOrdering::SeqCst,
+        AtomicOrdering::Acquire
+    );
+    atomic_cxchg_harness!(
+        harness_intrinsic_atomic_cxchg_seqcst_seqcst,
+        atomic_cxchg_wrapper,
+        AtomicOrdering::SeqCst,
+        AtomicOrdering::SeqCst
+    );
+
+    atomic_cxchg_harness!(
+        harness_intrinsic_atomic_cxchgweak_relaxed_relaxed,
+        atomic_cxchgweak_wrapper,
+        AtomicOrdering::Relaxed,
+        AtomicOrdering::Relaxed
+    );
+    atomic_cxchg_harness!(
+        harness_intrinsic_atomic_cxchgweak_relaxed_acquire,
+        atomic_cxchgweak_wrapper,
+        AtomicOrdering::Relaxed,
+        AtomicOrdering::Acquire
+    );
+    atomic_cxchg_harness!(
+        harness_intrinsic_atomic_cxchgweak_relaxed_seqcst,
+        atomic_cxchgweak_wrapper,
+        AtomicOrdering::Relaxed,
+        AtomicOrdering::SeqCst
+    );
+    atomic_cxchg_harness!(
+        harness_intrinsic_atomic_cxchgweak_acquire_relaxed,
+        atomic_cxchgweak_wrapper,
+        AtomicOrdering::Acquire,
+        AtomicOrdering::Relaxed
+    );
+    atomic_cxchg_harness!(
+        harness_intrinsic_atomic_cxchgweak_acquire_acquire,
+        atomic_cxchgweak_wrapper,
+        AtomicOrdering::Acquire,
+        AtomicOrdering::Acquire
+    );
+    atomic_cxchg_harness!(
+        harness_intrinsic_atomic_cxchgweak_acquire_seqcst,
+        atomic_cxchgweak_wrapper,
+        AtomicOrdering::Acquire,
+        AtomicOrdering::SeqCst
+    );
+    atomic_cxchg_harness!(
+        harness_intrinsic_atomic_cxchgweak_release_relaxed,
+        atomic_cxchgweak_wrapper,
+        AtomicOrdering::Release,
+        AtomicOrdering::Relaxed
+    );
+    atomic_cxchg_harness!(
+        harness_intrinsic_atomic_cxchgweak_release_acquire,
+        atomic_cxchgweak_wrapper,
+        AtomicOrdering::Release,
+        AtomicOrdering::Acquire
+    );
+    atomic_cxchg_harness!(
+        harness_intrinsic_atomic_cxchgweak_release_seqcst,
+        atomic_cxchgweak_wrapper,
+        AtomicOrdering::Release,
+        AtomicOrdering::SeqCst
+    );
+    atomic_cxchg_harness!(
+        harness_intrinsic_atomic_cxchgweak_acqrel_relaxed,
+        atomic_cxchgweak_wrapper,
+        AtomicOrdering::AcqRel,
+        AtomicOrdering::Relaxed
+    );
+    atomic_cxchg_harness!(
+        harness_intrinsic_atomic_cxchgweak_acqrel_acquire,
+        atomic_cxchgweak_wrapper,
+        AtomicOrdering::AcqRel,
+        AtomicOrdering::Acquire
+    );
+    atomic_cxchg_harness!(
+        harness_intrinsic_atomic_cxchgweak_acqrel_seqcst,
+        atomic_cxchgweak_wrapper,
+        AtomicOrdering::AcqRel,
+        AtomicOrdering::SeqCst
+    );
+    atomic_cxchg_harness!(
+        harness_intrinsic_atomic_cxchgweak_seqcst_relaxed,
+        atomic_cxchgweak_wrapper,
+        AtomicOrdering::SeqCst,
+        AtomicOrdering::Relaxed
+    );
+    atomic_cxchg_harness!(
+        harness_intrinsic_atomic_cxchgweak_seqcst_acquire,
+        atomic_cxchgweak_wrapper,
+        AtomicOrdering::SeqCst,
+        AtomicOrdering::Acquire
+    );
+    atomic_cxchg_harness!(
+        harness_intrinsic_atomic_cxchgweak_seqcst_seqcst,
+        atomic_cxchgweak_wrapper,
+        AtomicOrdering::SeqCst,
+        AtomicOrdering::SeqCst
+    );
 }
 
 /// Returns the return address of the caller function (after inlining) in a best-effort manner or a null pointer if it is not supported on the current backend.
diff --git a/library/core/src/sync/atomic.rs b/library/core/src/sync/atomic.rs
index 14e33019a45ff..cf90992f2e9e2 100644
--- a/library/core/src/sync/atomic.rs
+++ b/library/core/src/sync/atomic.rs
@@ -242,11 +242,17 @@
 // are just normal values that get loaded/stored, but not dereferenced.
 #![allow(clippy::not_unsafe_ptr_arg_deref)]
 
+use safety::{ensures, requires};
+
 use self::Ordering::*;
 use crate::cell::UnsafeCell;
 use crate::hint::spin_loop;
 use crate::intrinsics::AtomicOrdering as AO;
+#[cfg(kani)]
+use crate::kani;
 use crate::mem::transmute;
+#[cfg(kani)]
+use crate::ub_checks;
 use crate::{fmt, intrinsics};
 
 #[unstable(
@@ -600,6 +606,12 @@ impl AtomicBool {
     #[inline]
     #[stable(feature = "atomic_from_ptr", since = "1.75.0")]
     #[rustc_const_stable(feature = "const_atomic_from_ptr", since = "1.84.0")]
+    #[requires(ptr.cast::<AtomicBool>().is_aligned())]
+    #[requires(ub_checks::can_dereference(ptr))]
+    #[requires(ub_checks::can_write(ptr))]
+    #[ensures(|result: &&AtomicBool| {
+        core::ptr::eq(*result, ptr.cast::<AtomicBool>())
+    })]
     pub const unsafe fn from_ptr<'a>(ptr: *mut bool) -> &'a AtomicBool {
         // SAFETY: guaranteed by the caller
         unsafe { &*ptr.cast() }
@@ -766,6 +778,7 @@ impl AtomicBool {
     #[stable(feature = "rust1", since = "1.0.0")]
     #[rustc_const_unstable(feature = "const_atomic", issue = "160078")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+    #[requires(order == Relaxed || order == Acquire || order == SeqCst)]
     pub const fn load(&self, order: Ordering) -> bool {
         // SAFETY: any data races are prevented by atomic intrinsics and the raw
         // pointer passed in is valid because we got it from a reference.
@@ -832,6 +845,8 @@ impl AtomicBool {
     #[rustc_const_unstable(feature = "const_atomic", issue = "160078")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[rustc_should_not_be_called_on_const_items]
+    #[requires(order == Relaxed || order == Release || order == SeqCst)]
+    #[cfg_attr(kani, kani::modifies(self))]
     pub const fn store(&self, val: bool, order: Ordering) {
         // SAFETY: any data races are prevented by atomic intrinsics and the raw
         // pointer passed in is valid because we got it from a reference.
@@ -899,6 +914,7 @@ impl AtomicBool {
     #[cfg(target_has_atomic = "8")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[rustc_should_not_be_called_on_const_items]
+    #[cfg_attr(kani, kani::modifies(self))]
     pub const fn swap(&self, val: bool, order: Ordering) -> bool {
         if EMULATE_ATOMIC_BOOL {
             if val { self.fetch_or(true, order) } else { self.fetch_and(false, order) }
@@ -968,6 +984,7 @@ impl AtomicBool {
     #[cfg(target_has_atomic = "8")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[rustc_should_not_be_called_on_const_items]
+    #[cfg_attr(kani, kani::modifies(self))]
     pub const fn compare_and_swap(&self, current: bool, new: bool, order: Ordering) -> bool {
         match self.compare_exchange(current, new, order, strongest_failure_ordering(order)) {
             Ok(x) => x,
@@ -1031,6 +1048,8 @@ impl AtomicBool {
     #[cfg(target_has_atomic = "8")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[rustc_should_not_be_called_on_const_items]
+    #[requires(failure == Relaxed || failure == Acquire || failure == SeqCst)]
+    #[cfg_attr(kani, kani::modifies(self))]
     pub const fn compare_exchange(
         &self,
         current: bool,
@@ -1134,6 +1153,8 @@ impl AtomicBool {
     #[cfg(target_has_atomic = "8")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[rustc_should_not_be_called_on_const_items]
+    #[requires(failure == Relaxed || failure == Acquire || failure == SeqCst)]
+    #[cfg_attr(kani, kani::modifies(self))]
     pub const fn compare_exchange_weak(
         &self,
         current: bool,
@@ -1198,6 +1219,7 @@ impl AtomicBool {
     #[cfg(target_has_atomic = "8")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[rustc_should_not_be_called_on_const_items]
+    #[cfg_attr(kani, kani::modifies(self))]
     pub const fn fetch_and(&self, val: bool, order: Ordering) -> bool {
         // SAFETY: data races are prevented by atomic intrinsics.
         unsafe { atomic_and(self.v.get().cast::<u8>(), val as u8, order) != 0 }
@@ -1242,6 +1264,7 @@ impl AtomicBool {
     #[cfg(target_has_atomic = "8")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[rustc_should_not_be_called_on_const_items]
+    #[cfg_attr(kani, kani::modifies(self))]
     pub const fn fetch_nand(&self, val: bool, order: Ordering) -> bool {
         // We can't use atomic_nand here because it can result in a bool with
         // an invalid value. This happens because the atomic operation is done
@@ -1296,6 +1319,7 @@ impl AtomicBool {
     #[cfg(target_has_atomic = "8")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[rustc_should_not_be_called_on_const_items]
+    #[cfg_attr(kani, kani::modifies(self))]
     pub const fn fetch_or(&self, val: bool, order: Ordering) -> bool {
         // SAFETY: data races are prevented by atomic intrinsics.
         unsafe { atomic_or(self.v.get().cast::<u8>(), val as u8, order) != 0 }
@@ -1339,6 +1363,7 @@ impl AtomicBool {
     #[cfg(target_has_atomic = "8")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[rustc_should_not_be_called_on_const_items]
+    #[cfg_attr(kani, kani::modifies(self))]
     pub const fn fetch_xor(&self, val: bool, order: Ordering) -> bool {
         // SAFETY: data races are prevented by atomic intrinsics.
         unsafe { atomic_xor(self.v.get().cast::<u8>(), val as u8, order) != 0 }
@@ -1378,6 +1403,7 @@ impl AtomicBool {
     #[cfg(target_has_atomic = "8")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[rustc_should_not_be_called_on_const_items]
+    #[cfg_attr(kani, kani::modifies(self))]
     pub const fn fetch_not(&self, order: Ordering) -> bool {
         self.fetch_xor(true, order)
     }
@@ -1638,6 +1664,12 @@ impl<T> AtomicPtr<T> {
     #[inline]
     #[stable(feature = "atomic_from_ptr", since = "1.75.0")]
     #[rustc_const_stable(feature = "const_atomic_from_ptr", since = "1.84.0")]
+    #[requires(ptr.cast::<AtomicPtr<T>>().is_aligned())]
+    #[requires(ub_checks::can_dereference(ptr))]
+    #[requires(ub_checks::can_write(ptr))]
+    #[ensures(|result: &&AtomicPtr<T>| {
+        core::ptr::eq(*result, ptr.cast::<AtomicPtr<T>>())
+    })]
     pub const unsafe fn from_ptr<'a>(ptr: *mut *mut T) -> &'a AtomicPtr<T> {
         // SAFETY: guaranteed by the caller
         unsafe { &*ptr.cast() }
@@ -1849,6 +1881,7 @@ impl<T> AtomicPtr<T> {
     #[stable(feature = "rust1", since = "1.0.0")]
     #[rustc_const_unstable(feature = "const_atomic", issue = "160078")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+    #[requires(order == Relaxed || order == Acquire || order == SeqCst)]
     pub const fn load(&self, order: Ordering) -> *mut T {
         // SAFETY: data races are prevented by atomic intrinsics.
         unsafe {
@@ -1947,6 +1980,8 @@ impl<T> AtomicPtr<T> {
     #[rustc_const_unstable(feature = "const_atomic", issue = "160078")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[rustc_should_not_be_called_on_const_items]
+    #[requires(order == Relaxed || order == Release || order == SeqCst)]
+    #[cfg_attr(kani, kani::modifies(self))]
     pub const fn store(&self, ptr: *mut T, order: Ordering) {
         // SAFETY: data races are prevented by atomic intrinsics.
         unsafe {
@@ -2043,6 +2078,7 @@ impl<T> AtomicPtr<T> {
     #[cfg(target_has_atomic = "ptr")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[rustc_should_not_be_called_on_const_items]
+    #[cfg_attr(kani, kani::modifies(self))]
     pub const fn swap(&self, ptr: *mut T, order: Ordering) -> *mut T {
         // SAFETY: data races are prevented by atomic intrinsics.
         unsafe { atomic_swap(self.as_ptr(), ptr, order) }
@@ -2106,6 +2142,7 @@ impl<T> AtomicPtr<T> {
     #[cfg(target_has_atomic = "ptr")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[rustc_should_not_be_called_on_const_items]
+    #[cfg_attr(kani, kani::modifies(self))]
     pub fn compare_and_swap(&self, current: *mut T, new: *mut T, order: Ordering) -> *mut T {
         match self.compare_exchange(current, new, order, strongest_failure_ordering(order)) {
             Ok(x) => x,
@@ -2161,6 +2198,8 @@ impl<T> AtomicPtr<T> {
     #[cfg(target_has_atomic = "ptr")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[rustc_should_not_be_called_on_const_items]
+    #[requires(failure == Relaxed || failure == Acquire || failure == SeqCst)]
+    #[cfg_attr(kani, kani::modifies(self))]
     pub fn compare_exchange(
         &self,
         current: *mut T,
@@ -2225,6 +2264,8 @@ impl<T> AtomicPtr<T> {
     #[cfg(target_has_atomic = "ptr")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[rustc_should_not_be_called_on_const_items]
+    #[requires(failure == Relaxed || failure == Acquire || failure == SeqCst)]
+    #[cfg_attr(kani, kani::modifies(self))]
     pub fn compare_exchange_weak(
         &self,
         current: *mut T,
@@ -2610,6 +2651,7 @@ impl<T> AtomicPtr<T> {
     #[stable(feature = "strict_provenance_atomic_ptr", since = "1.91.0")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[rustc_should_not_be_called_on_const_items]
+    #[cfg_attr(kani, kani::modifies(self))]
     pub fn fetch_or(&self, val: usize, order: Ordering) -> *mut T {
         // SAFETY: data races are prevented by atomic intrinsics.
         unsafe { atomic_or(self.as_ptr(), val, order).cast() }
@@ -2660,6 +2702,7 @@ impl<T> AtomicPtr<T> {
     #[stable(feature = "strict_provenance_atomic_ptr", since = "1.91.0")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[rustc_should_not_be_called_on_const_items]
+    #[cfg_attr(kani, kani::modifies(self))]
     pub fn fetch_and(&self, val: usize, order: Ordering) -> *mut T {
         // SAFETY: data races are prevented by atomic intrinsics.
         unsafe { atomic_and(self.as_ptr(), val, order).cast() }
@@ -2708,6 +2751,7 @@ impl<T> AtomicPtr<T> {
     #[stable(feature = "strict_provenance_atomic_ptr", since = "1.91.0")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
     #[rustc_should_not_be_called_on_const_items]
+    #[cfg_attr(kani, kani::modifies(self))]
     pub fn fetch_xor(&self, val: usize, order: Ordering) -> *mut T {
         // SAFETY: data races are prevented by atomic intrinsics.
         unsafe { atomic_xor(self.as_ptr(), val, order).cast() }
@@ -2940,6 +2984,19 @@ macro_rules! atomic_int {
             #[inline]
             #[stable(feature = "atomic_from_ptr", since = "1.75.0")]
             #[rustc_const_stable(feature = "const_atomic_from_ptr", since = "1.84.0")]
+            #[requires(ptr.cast::<$atomic_type>().is_aligned())]
+            #[requires(!ptr.is_null())]
+            #[requires(ub_checks::can_dereference(ptr))]
+            #[requires(ub_checks::can_write(ptr))]
+            #[ensures(|result: &&$atomic_type| {
+                core::ptr::eq(*result, ptr.cast::<$atomic_type>())
+            })]
+            #[ensures(|result: &&$atomic_type| {
+                ub_checks::can_dereference(*result as *const $atomic_type)
+            })]
+            #[ensures(|result: &&$atomic_type| {
+                ub_checks::can_write((*result).as_ptr())
+            })]
             pub const unsafe fn from_ptr<'a>(ptr: *mut $int_type) -> &'a $atomic_type {
                 // SAFETY: guaranteed by the caller
                 unsafe { &*ptr.cast() }
@@ -3138,6 +3195,7 @@ macro_rules! atomic_int {
             #[$stable]
             #[rustc_const_unstable(feature = "const_atomic", issue = "160078")]
             #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+            #[requires(order == Relaxed || order == Acquire || order == SeqCst)]
             pub const fn load(&self, order: Ordering) -> $int_type {
                 // SAFETY: data races are prevented by atomic intrinsics.
                 unsafe { atomic_load::<_, /* VOLATILE */ false>(self.as_ptr(), order) }
@@ -3217,6 +3275,8 @@ macro_rules! atomic_int {
             #[rustc_const_unstable(feature = "const_atomic", issue = "160078")]
             #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
             #[rustc_should_not_be_called_on_const_items]
+            #[requires(order == Relaxed || order == Release || order == SeqCst)]
+            #[cfg_attr(kani, kani::modifies(self))]
             pub const fn store(&self, val: $int_type, order: Ordering) {
                 // SAFETY: data races are prevented by atomic intrinsics.
                 unsafe { atomic_store::<_, /* VOLATILE */ false>(self.as_ptr(), val, order); }
@@ -3295,6 +3355,7 @@ macro_rules! atomic_int {
             #[cfg(any($cfg_cas, doc))]
             #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
             #[rustc_should_not_be_called_on_const_items]
+            #[cfg_attr(kani, kani::modifies(self))]
             pub const fn swap(&self, val: $int_type, order: Ordering) -> $int_type {
                 // SAFETY: data races are prevented by atomic intrinsics.
                 unsafe { atomic_swap(self.as_ptr(), val, order) }
@@ -3362,6 +3423,7 @@ macro_rules! atomic_int {
             #[cfg(any($cfg_cas, doc))]
             #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
             #[rustc_should_not_be_called_on_const_items]
+            #[cfg_attr(kani, kani::modifies(self))]
             pub const fn compare_and_swap(&self,
                                     current: $int_type,
                                     new: $int_type,
@@ -3433,6 +3495,8 @@ macro_rules! atomic_int {
             #[cfg(any($cfg_cas, doc))]
             #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
             #[rustc_should_not_be_called_on_const_items]
+            #[requires(failure == Relaxed || failure == Acquire || failure == SeqCst)]
+            #[cfg_attr(kani, kani::modifies(self))]
             pub const fn compare_exchange(&self,
                                     current: $int_type,
                                     new: $int_type,
@@ -3499,6 +3563,8 @@ macro_rules! atomic_int {
             #[cfg(any($cfg_cas, doc))]
             #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
             #[rustc_should_not_be_called_on_const_items]
+            #[requires(failure == Relaxed || failure == Acquire || failure == SeqCst)]
+            #[cfg_attr(kani, kani::modifies(self))]
             pub const fn compare_exchange_weak(&self,
                                          current: $int_type,
                                          new: $int_type,
@@ -3538,6 +3604,7 @@ macro_rules! atomic_int {
             #[cfg(any($cfg_cas, doc))]
             #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
             #[rustc_should_not_be_called_on_const_items]
+            #[cfg_attr(kani, kani::modifies(self))]
             pub const fn fetch_add(&self, val: $int_type, order: Ordering) -> $int_type {
                 // SAFETY: data races are prevented by atomic intrinsics.
                 unsafe { atomic_add(self.as_ptr(), val, order) }
@@ -3571,6 +3638,7 @@ macro_rules! atomic_int {
             #[cfg(any($cfg_cas, doc))]
             #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
             #[rustc_should_not_be_called_on_const_items]
+            #[cfg_attr(kani, kani::modifies(self))]
             pub const fn fetch_sub(&self, val: $int_type, order: Ordering) -> $int_type {
                 // SAFETY: data races are prevented by atomic intrinsics.
                 unsafe { atomic_sub(self.as_ptr(), val, order) }
@@ -3607,6 +3675,7 @@ macro_rules! atomic_int {
             #[cfg(any($cfg_cas, doc))]
             #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
             #[rustc_should_not_be_called_on_const_items]
+            #[cfg_attr(kani, kani::modifies(self))]
             pub const fn fetch_and(&self, val: $int_type, order: Ordering) -> $int_type {
                 // SAFETY: data races are prevented by atomic intrinsics.
                 unsafe { atomic_and(self.as_ptr(), val, order) }
@@ -3643,6 +3712,7 @@ macro_rules! atomic_int {
             #[cfg(any($cfg_cas, doc))]
             #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
             #[rustc_should_not_be_called_on_const_items]
+            #[cfg_attr(kani, kani::modifies(self))]
             pub const fn fetch_nand(&self, val: $int_type, order: Ordering) -> $int_type {
                 // SAFETY: data races are prevented by atomic intrinsics.
                 unsafe { atomic_nand(self.as_ptr(), val, order) }
@@ -3679,6 +3749,7 @@ macro_rules! atomic_int {
             #[cfg(any($cfg_cas, doc))]
             #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
             #[rustc_should_not_be_called_on_const_items]
+            #[cfg_attr(kani, kani::modifies(self))]
             pub const fn fetch_or(&self, val: $int_type, order: Ordering) -> $int_type {
                 // SAFETY: data races are prevented by atomic intrinsics.
                 unsafe { atomic_or(self.as_ptr(), val, order) }
@@ -3715,6 +3786,7 @@ macro_rules! atomic_int {
             #[cfg(any($cfg_cas, doc))]
             #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
             #[rustc_should_not_be_called_on_const_items]
+            #[cfg_attr(kani, kani::modifies(self))]
             pub const fn fetch_xor(&self, val: $int_type, order: Ordering) -> $int_type {
                 // SAFETY: data races are prevented by atomic intrinsics.
                 unsafe { atomic_xor(self.as_ptr(), val, order) }
@@ -3919,6 +3991,7 @@ macro_rules! atomic_int {
             #[cfg(any($cfg_cas, doc))]
             #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
             #[rustc_should_not_be_called_on_const_items]
+            #[cfg_attr(kani, kani::modifies(self))]
             pub const fn fetch_max(&self, val: $int_type, order: Ordering) -> $int_type {
                 // SAFETY: data races are prevented by atomic intrinsics.
                 unsafe { $max_fn(self.as_ptr(), val, order) }
@@ -3969,6 +4042,7 @@ macro_rules! atomic_int {
             #[cfg(any($cfg_cas, doc))]
             #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
             #[rustc_should_not_be_called_on_const_items]
+            #[cfg_attr(kani, kani::modifies(self))]
             pub const fn fetch_min(&self, val: $int_type, order: Ordering) -> $int_type {
                 // SAFETY: data races are prevented by atomic intrinsics.
                 unsafe { $min_fn(self.as_ptr(), val, order) }
@@ -4296,6 +4370,11 @@ const fn strongest_failure_ordering(order: Ordering) -> Ordering {
 #[inline]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
 #[rustc_const_unstable(feature = "const_atomic", issue = "160078")]
+#[cfg_attr(kani, kani::modifies(dst))]
+#[requires(ub_checks::can_write(dst))]
+#[requires(order == Relaxed || order == Release || order == SeqCst)]
+#[ensures(|_| ub_checks::can_dereference(dst as *const T))]
+#[ensures(|_| ub_checks::can_write(dst))]
 const unsafe fn atomic_store<T: Copy, const VOLATILE: bool>(dst: *mut T, val: T, order: Ordering) {
     // SAFETY: the caller must uphold the safety contract for `atomic_store`.
     unsafe {
@@ -4312,6 +4391,9 @@ const unsafe fn atomic_store<T: Copy, const VOLATILE: bool>(dst: *mut T, val: T,
 #[inline]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
 #[rustc_const_unstable(feature = "const_atomic", issue = "160078")]
+#[requires(ub_checks::can_dereference(dst))]
+#[requires(order == Relaxed || order == Acquire || order == SeqCst)]
+#[ensures(|_| ub_checks::can_dereference(dst))]
 const unsafe fn atomic_load<T: Copy, const VOLATILE: bool>(dst: *const T, order: Ordering) -> T {
     // SAFETY: the caller must uphold the safety contract for `atomic_load`.
     unsafe {
@@ -4329,6 +4411,12 @@ const unsafe fn atomic_load<T: Copy, const VOLATILE: bool>(dst: *const T, order:
 #[cfg(target_has_atomic)]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
 #[rustc_const_unstable(feature = "const_atomic", issue = "160078")]
+#[cfg_attr(kani, kani::modifies(dst))]
+#[requires(ub_checks::can_dereference(dst as *const T))]
+#[requires(ub_checks::can_write(dst))]
+#[ensures(|_| {
+    ub_checks::can_dereference(dst as *const T) && ub_checks::can_write(dst)
+})]
 const unsafe fn atomic_swap<T: Copy>(dst: *mut T, val: T, order: Ordering) -> T {
     // SAFETY: the caller must uphold the safety contract for `atomic_swap`.
     unsafe {
@@ -4347,6 +4435,12 @@ const unsafe fn atomic_swap<T: Copy>(dst: *mut T, val: T, order: Ordering) -> T
 #[cfg(target_has_atomic)]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
 #[rustc_const_unstable(feature = "const_atomic", issue = "160078")]
+#[cfg_attr(kani, kani::modifies(dst))]
+#[requires(ub_checks::can_dereference(dst as *const T))]
+#[requires(ub_checks::can_write(dst))]
+#[ensures(|_| {
+    ub_checks::can_dereference(dst as *const T) && ub_checks::can_write(dst)
+})]
 const unsafe fn atomic_add<T: Copy, U: Copy>(dst: *mut T, val: U, order: Ordering) -> T {
     // SAFETY: the caller must uphold the safety contract for `atomic_add`.
     unsafe {
@@ -4365,6 +4459,12 @@ const unsafe fn atomic_add<T: Copy, U: Copy>(dst: *mut T, val: U, order: Orderin
 #[cfg(target_has_atomic)]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
 #[rustc_const_unstable(feature = "const_atomic", issue = "160078")]
+#[cfg_attr(kani, kani::modifies(dst))]
+#[requires(ub_checks::can_dereference(dst as *const T))]
+#[requires(ub_checks::can_write(dst))]
+#[ensures(|_| {
+    ub_checks::can_dereference(dst as *const T) && ub_checks::can_write(dst)
+})]
 const unsafe fn atomic_sub<T: Copy, U: Copy>(dst: *mut T, val: U, order: Ordering) -> T {
     // SAFETY: the caller must uphold the safety contract for `atomic_sub`.
     unsafe {
@@ -4385,6 +4485,13 @@ const unsafe fn atomic_sub<T: Copy, U: Copy>(dst: *mut T, val: U, order: Orderin
 #[unstable(feature = "core_intrinsics", issue = "none")]
 #[doc(hidden)]
 #[rustc_const_unstable(feature = "const_atomic", issue = "160078")]
+#[cfg_attr(kani, kani::modifies(dst))]
+#[requires(ub_checks::can_dereference(dst as *const T))]
+#[requires(ub_checks::can_write(dst))]
+#[requires(failure != Release && failure != AcqRel)]
+#[ensures(|_| {
+    ub_checks::can_dereference(dst as *const T) && ub_checks::can_write(dst)
+})]
 pub const unsafe fn atomic_compare_exchange<T: Copy>(
     dst: *mut T,
     old: T,
@@ -4451,6 +4558,13 @@ pub const unsafe fn atomic_compare_exchange<T: Copy>(
 #[cfg(target_has_atomic)]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
 #[rustc_const_unstable(feature = "const_atomic", issue = "160078")]
+#[cfg_attr(kani, kani::modifies(dst))]
+#[requires(ub_checks::can_dereference(dst as *const T))]
+#[requires(ub_checks::can_write(dst))]
+#[requires(failure != Release && failure != AcqRel)]
+#[ensures(|_| {
+    ub_checks::can_dereference(dst as *const T) && ub_checks::can_write(dst)
+})]
 const unsafe fn atomic_compare_exchange_weak<T: Copy>(
     dst: *mut T,
     old: T,
@@ -4517,6 +4631,12 @@ const unsafe fn atomic_compare_exchange_weak<T: Copy>(
 #[cfg(target_has_atomic)]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
 #[rustc_const_unstable(feature = "const_atomic", issue = "160078")]
+#[cfg_attr(kani, kani::modifies(dst))]
+#[requires(ub_checks::can_dereference(dst as *const T))]
+#[requires(ub_checks::can_write(dst))]
+#[ensures(|_| {
+    ub_checks::can_dereference(dst as *const T) && ub_checks::can_write(dst)
+})]
 const unsafe fn atomic_and<T: Copy, U: Copy>(dst: *mut T, val: U, order: Ordering) -> T {
     // SAFETY: the caller must uphold the safety contract for `atomic_and`
     unsafe {
@@ -4534,6 +4654,12 @@ const unsafe fn atomic_and<T: Copy, U: Copy>(dst: *mut T, val: U, order: Orderin
 #[cfg(target_has_atomic)]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
 #[rustc_const_unstable(feature = "const_atomic", issue = "160078")]
+#[cfg_attr(kani, kani::modifies(dst))]
+#[requires(ub_checks::can_dereference(dst as *const T))]
+#[requires(ub_checks::can_write(dst))]
+#[ensures(|_| {
+    ub_checks::can_dereference(dst as *const T) && ub_checks::can_write(dst)
+})]
 const unsafe fn atomic_nand<T: Copy, U: Copy>(dst: *mut T, val: U, order: Ordering) -> T {
     // SAFETY: the caller must uphold the safety contract for `atomic_nand`
     unsafe {
@@ -4551,6 +4677,12 @@ const unsafe fn atomic_nand<T: Copy, U: Copy>(dst: *mut T, val: U, order: Orderi
 #[cfg(target_has_atomic)]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
 #[rustc_const_unstable(feature = "const_atomic", issue = "160078")]
+#[cfg_attr(kani, kani::modifies(dst))]
+#[requires(ub_checks::can_dereference(dst as *const T))]
+#[requires(ub_checks::can_write(dst))]
+#[ensures(|_| {
+    ub_checks::can_dereference(dst as *const T) && ub_checks::can_write(dst)
+})]
 const unsafe fn atomic_or<T: Copy, U: Copy>(dst: *mut T, val: U, order: Ordering) -> T {
     // SAFETY: the caller must uphold the safety contract for `atomic_or`
     unsafe {
@@ -4568,6 +4700,12 @@ const unsafe fn atomic_or<T: Copy, U: Copy>(dst: *mut T, val: U, order: Ordering
 #[cfg(target_has_atomic)]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
 #[rustc_const_unstable(feature = "const_atomic", issue = "160078")]
+#[cfg_attr(kani, kani::modifies(dst))]
+#[requires(ub_checks::can_dereference(dst as *const T))]
+#[requires(ub_checks::can_write(dst))]
+#[ensures(|_| {
+    ub_checks::can_dereference(dst as *const T) && ub_checks::can_write(dst)
+})]
 const unsafe fn atomic_xor<T: Copy, U: Copy>(dst: *mut T, val: U, order: Ordering) -> T {
     // SAFETY: the caller must uphold the safety contract for `atomic_xor`
     unsafe {
@@ -4586,6 +4724,12 @@ const unsafe fn atomic_xor<T: Copy, U: Copy>(dst: *mut T, val: U, order: Orderin
 #[cfg(target_has_atomic)]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
 #[rustc_const_unstable(feature = "const_atomic", issue = "160078")]
+#[cfg_attr(kani, kani::modifies(dst))]
+#[requires(ub_checks::can_dereference(dst as *const T))]
+#[requires(ub_checks::can_write(dst))]
+#[ensures(|_| {
+    ub_checks::can_dereference(dst as *const T) && ub_checks::can_write(dst)
+})]
 const unsafe fn atomic_max<T: Copy>(dst: *mut T, val: T, order: Ordering) -> T {
     // SAFETY: the caller must uphold the safety contract for `atomic_max`
     unsafe {
@@ -4622,6 +4766,12 @@ const unsafe fn atomic_min<T: Copy>(dst: *mut T, val: T, order: Ordering) -> T {
 #[cfg(target_has_atomic)]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
 #[rustc_const_unstable(feature = "const_atomic", issue = "160078")]
+#[cfg_attr(kani, kani::modifies(dst))]
+#[requires(ub_checks::can_dereference(dst as *const T))]
+#[requires(ub_checks::can_write(dst))]
+#[ensures(|_| {
+    ub_checks::can_dereference(dst as *const T) && ub_checks::can_write(dst)
+})]
 const unsafe fn atomic_umax<T: Copy>(dst: *mut T, val: T, order: Ordering) -> T {
     // SAFETY: the caller must uphold the safety contract for `atomic_umax`
     unsafe {
@@ -4640,6 +4790,12 @@ const unsafe fn atomic_umax<T: Copy>(dst: *mut T, val: T, order: Ordering) -> T
 #[cfg(target_has_atomic)]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
 #[rustc_const_unstable(feature = "const_atomic", issue = "160078")]
+#[cfg_attr(kani, kani::modifies(dst))]
+#[requires(ub_checks::can_dereference(dst as *const T))]
+#[requires(ub_checks::can_write(dst))]
+#[ensures(|_| {
+    ub_checks::can_dereference(dst as *const T) && ub_checks::can_write(dst)
+})]
 const unsafe fn atomic_umin<T: Copy>(dst: *mut T, val: T, order: Ordering) -> T {
     // SAFETY: the caller must uphold the safety contract for `atomic_umin`
     unsafe {
@@ -4944,3 +5100,1340 @@ impl<T> fmt::Pointer for AtomicPtr<T> {
 pub fn spin_loop_hint() {
     spin_loop()
 }
+
+#[cfg(kani)]
+#[unstable(feature = "kani", issue = "none")]
+mod verify {
+    use super::*;
+
+    // Generate candidates across the allocation. Contract proofs assume the callee's
+    // preconditions, retaining only initialized, aligned, readable, and writable offsets.
+    fn ptr_at_offset<T>(buf: &mut [u8; 100]) -> *mut T {
+        let offset = kani::any_where(|offset: &usize| *offset < 100);
+        buf.as_mut_ptr().wrapping_add(offset).cast::<T>()
+    }
+
+    fn any_ordering() -> Ordering {
+        match kani::any::<u8>() {
+            0 => Relaxed,
+            1 => Release,
+            2 => Acquire,
+            3 => AcqRel,
+            _ => SeqCst,
+        }
+    }
+
+    // Use the concrete Atomic<T> type in proof targets: Kani's contract resolver
+    // does not resolve methods through the AtomicBool/AtomicPtr/integer aliases.
+    // Calls below still exercise the corresponding public aliases.
+    // Part 1: from_ptr.
+    #[cfg(target_has_atomic_load_store = "8")]
+    #[kani::proof_for_contract(Atomic::<bool>::from_ptr)]
+    pub fn harness_atomic_bool_from_ptr() {
+        // Arbitrary bool arrays use a MaybeUninit array internally, whose layout
+        // is unsupported by uninit-checks. Use independent symbolic bytes instead;
+        // from_ptr's preconditions retain only valid bool values at the chosen offset.
+        let mut buf: [u8; 100] = kani::any();
+        let ptr = ptr_at_offset::<bool>(&mut buf);
+
+        let _ = unsafe { AtomicBool::from_ptr(ptr) };
+        let byte = unsafe { ptr.cast::<u8>().read() };
+        assert!(byte <= 1);
+        kani::cover(byte == 0, "AtomicBool::from_ptr: false is reachable");
+        kani::cover(byte == 1, "AtomicBool::from_ptr: true is reachable");
+        kani::cover(true, "AtomicBool::from_ptr: reached after call");
+    }
+
+    // Harnesses for integer Atomic*::from_ptr functions.
+    macro_rules! from_ptr_harness {
+        ($name:ident, $atomic:ty, $value:ty) => {
+            #[kani::proof_for_contract(Atomic::<$value>::from_ptr)]
+            pub fn $name() {
+                let mut buf: [u8; 100] = kani::any();
+                let ptr = ptr_at_offset::<$value>(&mut buf);
+
+                let _ = unsafe { <$atomic>::from_ptr(ptr) };
+                kani::cover(true, "integer from_ptr: reached after call");
+            }
+        };
+    }
+
+    #[cfg(target_has_atomic_load_store = "8")]
+    from_ptr_harness!(harness_atomic_i8_from_ptr, AtomicI8, i8);
+    #[cfg(target_has_atomic_load_store = "8")]
+    from_ptr_harness!(harness_atomic_u8_from_ptr, AtomicU8, u8);
+    #[cfg(target_has_atomic_load_store = "16")]
+    from_ptr_harness!(harness_atomic_i16_from_ptr, AtomicI16, i16);
+    #[cfg(target_has_atomic_load_store = "16")]
+    from_ptr_harness!(harness_atomic_u16_from_ptr, AtomicU16, u16);
+    #[cfg(target_has_atomic_load_store = "32")]
+    from_ptr_harness!(harness_atomic_i32_from_ptr, AtomicI32, i32);
+    #[cfg(target_has_atomic_load_store = "32")]
+    from_ptr_harness!(harness_atomic_u32_from_ptr, AtomicU32, u32);
+    #[cfg(target_has_atomic_load_store = "64")]
+    from_ptr_harness!(harness_atomic_i64_from_ptr, AtomicI64, i64);
+    #[cfg(target_has_atomic_load_store = "64")]
+    from_ptr_harness!(harness_atomic_u64_from_ptr, AtomicU64, u64);
+    #[cfg(target_has_atomic_load_store = "128")]
+    from_ptr_harness!(harness_atomic_i128_from_ptr, AtomicI128, i128);
+    #[cfg(target_has_atomic_load_store = "128")]
+    from_ptr_harness!(harness_atomic_u128_from_ptr, AtomicU128, u128);
+
+    // Harnesses for AtomicPtr::from_ptr.
+    // Kani matches this selector against the generic impl's definition path.
+    // `T` names its type parameter, not the concrete pointee used by the proof;
+    // each harness call below still instantiates the requested $pointee.
+    macro_rules! atomic_ptr_from_ptr_harness {
+        ($name:ident, $pointee:ty) => {
+            #[cfg(target_has_atomic_load_store = "ptr")]
+            #[kani::proof_for_contract(Atomic::<*mut T>::from_ptr)]
+            pub fn $name() {
+                // The stored pointer is arbitrary; the outer pointer targets valid local storage.
+                let mut value = kani::any::<usize>() as *mut $pointee;
+                let ptr = &mut value as *mut *mut $pointee;
+
+                let _ = unsafe { AtomicPtr::<$pointee>::from_ptr(ptr) };
+                kani::cover(true, "AtomicPtr::from_ptr: reached after call");
+            }
+        };
+    }
+
+    // Cover pointee sizes 0, 1, 2, 4, and the non-power-of-two size 3.
+    atomic_ptr_from_ptr_harness!(harness_atomic_ptr_from_ptr_unit, ());
+    atomic_ptr_from_ptr_harness!(harness_atomic_ptr_from_ptr_u8, u8);
+    atomic_ptr_from_ptr_harness!(harness_atomic_ptr_from_ptr_u16, u16);
+    atomic_ptr_from_ptr_harness!(harness_atomic_ptr_from_ptr_u32, u32);
+    atomic_ptr_from_ptr_harness!(harness_atomic_ptr_from_ptr_u8_3, [u8; 3]);
+
+    // Part 2: unsafe atomic helpers.
+    // Harnesses for ordinary (non-volatile) atomic_store and atomic_load.
+    // Volatile accesses have separate safety requirements and are not covered here.
+    macro_rules! store_harness {
+        ($name:ident, $atomic:ty, $value:ty) => {
+            #[kani::proof_for_contract(atomic_store::<$value, false>)]
+            pub fn $name() {
+                let initial: $value = kani::any();
+                let storage = <$atomic>::new(initial);
+                let val: $value = kani::any();
+
+                unsafe { atomic_store::<$value, false>(storage.as_ptr(), val, any_ordering()) };
+                kani::cover(true, "atomic_store: reached after call");
+            }
+        };
+    }
+
+    #[cfg(target_has_atomic_load_store = "8")]
+    store_harness!(harness_atomic_store_i8, AtomicI8, i8);
+    #[cfg(target_has_atomic_load_store = "8")]
+    store_harness!(harness_atomic_store_u8, AtomicU8, u8);
+    #[cfg(target_has_atomic_load_store = "16")]
+    store_harness!(harness_atomic_store_i16, AtomicI16, i16);
+    #[cfg(target_has_atomic_load_store = "16")]
+    store_harness!(harness_atomic_store_u16, AtomicU16, u16);
+    #[cfg(target_has_atomic_load_store = "32")]
+    store_harness!(harness_atomic_store_i32, AtomicI32, i32);
+    #[cfg(target_has_atomic_load_store = "32")]
+    store_harness!(harness_atomic_store_u32, AtomicU32, u32);
+    #[cfg(target_has_atomic_load_store = "64")]
+    store_harness!(harness_atomic_store_i64, AtomicI64, i64);
+    #[cfg(target_has_atomic_load_store = "64")]
+    store_harness!(harness_atomic_store_u64, AtomicU64, u64);
+    #[cfg(target_has_atomic_load_store = "128")]
+    store_harness!(harness_atomic_store_i128, AtomicI128, i128);
+    #[cfg(target_has_atomic_load_store = "128")]
+    store_harness!(harness_atomic_store_u128, AtomicU128, u128);
+    #[cfg(target_has_atomic_load_store = "ptr")]
+    store_harness!(harness_atomic_store_isize, AtomicIsize, isize);
+    #[cfg(target_has_atomic_load_store = "ptr")]
+    store_harness!(harness_atomic_store_usize, AtomicUsize, usize);
+
+    // Pointer harnesses for atomic_store.
+    #[cfg(target_has_atomic_load_store = "ptr")]
+    #[kani::proof_for_contract(atomic_store::<*mut u8, false>)]
+    pub fn harness_atomic_store_ptr() {
+        let initial = kani::any::<usize>() as *mut u8;
+        let storage = AtomicPtr::<u8>::new(initial);
+        let val = kani::any::<usize>() as *mut u8;
+
+        unsafe { atomic_store::<*mut u8, false>(storage.as_ptr(), val, any_ordering()) };
+        kani::cover(true, "atomic_store: reached after call");
+    }
+
+    // Harnesses for atomic_load.
+    macro_rules! load_harness {
+        ($name:ident, $atomic:ty, $value:ty) => {
+            #[kani::proof_for_contract(atomic_load::<$value, false>)]
+            pub fn $name() {
+                let initial: $value = kani::any();
+                let storage = <$atomic>::new(initial);
+
+                let _ = unsafe {
+                    atomic_load::<$value, false>(storage.as_ptr().cast_const(), any_ordering())
+                };
+                kani::cover(true, "atomic_load: reached after call");
+            }
+        };
+    }
+
+    // Load helpers.
+    #[cfg(target_has_atomic_load_store = "8")]
+    load_harness!(harness_atomic_load_i8, AtomicI8, i8);
+    #[cfg(target_has_atomic_load_store = "8")]
+    load_harness!(harness_atomic_load_u8, AtomicU8, u8);
+    #[cfg(target_has_atomic_load_store = "16")]
+    load_harness!(harness_atomic_load_i16, AtomicI16, i16);
+    #[cfg(target_has_atomic_load_store = "16")]
+    load_harness!(harness_atomic_load_u16, AtomicU16, u16);
+    #[cfg(target_has_atomic_load_store = "32")]
+    load_harness!(harness_atomic_load_i32, AtomicI32, i32);
+    #[cfg(target_has_atomic_load_store = "32")]
+    load_harness!(harness_atomic_load_u32, AtomicU32, u32);
+    #[cfg(target_has_atomic_load_store = "64")]
+    load_harness!(harness_atomic_load_i64, AtomicI64, i64);
+    #[cfg(target_has_atomic_load_store = "64")]
+    load_harness!(harness_atomic_load_u64, AtomicU64, u64);
+    #[cfg(target_has_atomic_load_store = "128")]
+    load_harness!(harness_atomic_load_i128, AtomicI128, i128);
+    #[cfg(target_has_atomic_load_store = "128")]
+    load_harness!(harness_atomic_load_u128, AtomicU128, u128);
+    #[cfg(target_has_atomic_load_store = "ptr")]
+    load_harness!(harness_atomic_load_isize, AtomicIsize, isize);
+    #[cfg(target_has_atomic_load_store = "ptr")]
+    load_harness!(harness_atomic_load_usize, AtomicUsize, usize);
+
+    // Pointer harness for atomic_load.
+    #[cfg(target_has_atomic_load_store = "ptr")]
+    #[kani::proof_for_contract(atomic_load::<*mut u8, false>)]
+    pub fn harness_atomic_load_ptr_u8() {
+        let initial = kani::any::<usize>() as *mut u8;
+        let storage = AtomicPtr::<u8>::new(initial);
+
+        let _ =
+            unsafe { atomic_load::<*mut u8, false>(storage.as_ptr().cast_const(), any_ordering()) };
+        kani::cover(true, "atomic_load: reached after call");
+    }
+
+    // Harnesses for atomic_swap, atomic_max, atomic_umax, and atomic_umin.
+    macro_rules! rmw_harness {
+        ($name:ident, $operation:ident, $atomic:ty, $value:ty) => {
+            #[kani::proof_for_contract($operation::<$value>)]
+            pub fn $name() {
+                let initial: $value = kani::any();
+                let storage = <$atomic>::new(initial);
+                let val: $value = kani::any();
+
+                let _ = unsafe { $operation(storage.as_ptr(), val, any_ordering()) };
+                kani::cover(true, "atomic_swap/max/umax/umin: reached after call");
+            }
+        };
+    }
+
+    // Exchange helpers.
+    #[cfg(target_has_atomic = "8")]
+    rmw_harness!(harness_atomic_swap_i8, atomic_swap, AtomicI8, i8);
+    #[cfg(target_has_atomic = "8")]
+    rmw_harness!(harness_atomic_swap_u8, atomic_swap, AtomicU8, u8);
+    #[cfg(target_has_atomic = "16")]
+    rmw_harness!(harness_atomic_swap_i16, atomic_swap, AtomicI16, i16);
+    #[cfg(target_has_atomic = "16")]
+    rmw_harness!(harness_atomic_swap_u16, atomic_swap, AtomicU16, u16);
+    #[cfg(target_has_atomic = "32")]
+    rmw_harness!(harness_atomic_swap_i32, atomic_swap, AtomicI32, i32);
+    #[cfg(target_has_atomic = "32")]
+    rmw_harness!(harness_atomic_swap_u32, atomic_swap, AtomicU32, u32);
+    #[cfg(target_has_atomic = "64")]
+    rmw_harness!(harness_atomic_swap_i64, atomic_swap, AtomicI64, i64);
+    #[cfg(target_has_atomic = "64")]
+    rmw_harness!(harness_atomic_swap_u64, atomic_swap, AtomicU64, u64);
+    #[cfg(target_has_atomic = "128")]
+    rmw_harness!(harness_atomic_swap_i128, atomic_swap, AtomicI128, i128);
+    #[cfg(target_has_atomic = "128")]
+    rmw_harness!(harness_atomic_swap_u128, atomic_swap, AtomicU128, u128);
+    #[cfg(target_has_atomic = "ptr")]
+    rmw_harness!(harness_atomic_swap_isize, atomic_swap, AtomicIsize, isize);
+    #[cfg(target_has_atomic = "ptr")]
+    rmw_harness!(harness_atomic_swap_usize, atomic_swap, AtomicUsize, usize);
+
+    // Signed maximum helpers.
+    #[cfg(target_has_atomic = "8")]
+    rmw_harness!(harness_atomic_max_i8, atomic_max, AtomicI8, i8);
+    #[cfg(target_has_atomic = "16")]
+    rmw_harness!(harness_atomic_max_i16, atomic_max, AtomicI16, i16);
+    #[cfg(target_has_atomic = "32")]
+    rmw_harness!(harness_atomic_max_i32, atomic_max, AtomicI32, i32);
+    #[cfg(target_has_atomic = "64")]
+    rmw_harness!(harness_atomic_max_i64, atomic_max, AtomicI64, i64);
+    #[cfg(target_has_atomic = "128")]
+    rmw_harness!(harness_atomic_max_i128, atomic_max, AtomicI128, i128);
+    #[cfg(target_has_atomic = "ptr")]
+    rmw_harness!(harness_atomic_max_isize, atomic_max, AtomicIsize, isize);
+
+    // Unsigned maximum helpers.
+    #[cfg(target_has_atomic = "8")]
+    rmw_harness!(harness_atomic_umax_u8, atomic_umax, AtomicU8, u8);
+    #[cfg(target_has_atomic = "16")]
+    rmw_harness!(harness_atomic_umax_u16, atomic_umax, AtomicU16, u16);
+    #[cfg(target_has_atomic = "32")]
+    rmw_harness!(harness_atomic_umax_u32, atomic_umax, AtomicU32, u32);
+    #[cfg(target_has_atomic = "64")]
+    rmw_harness!(harness_atomic_umax_u64, atomic_umax, AtomicU64, u64);
+    #[cfg(target_has_atomic = "128")]
+    rmw_harness!(harness_atomic_umax_u128, atomic_umax, AtomicU128, u128);
+    #[cfg(target_has_atomic = "ptr")]
+    rmw_harness!(harness_atomic_umax_usize, atomic_umax, AtomicUsize, usize);
+
+    // Unsigned minimum helpers.
+    #[cfg(target_has_atomic = "8")]
+    rmw_harness!(harness_atomic_umin_u8, atomic_umin, AtomicU8, u8);
+    #[cfg(target_has_atomic = "16")]
+    rmw_harness!(harness_atomic_umin_u16, atomic_umin, AtomicU16, u16);
+    #[cfg(target_has_atomic = "32")]
+    rmw_harness!(harness_atomic_umin_u32, atomic_umin, AtomicU32, u32);
+    #[cfg(target_has_atomic = "64")]
+    rmw_harness!(harness_atomic_umin_u64, atomic_umin, AtomicU64, u64);
+    #[cfg(target_has_atomic = "128")]
+    rmw_harness!(harness_atomic_umin_u128, atomic_umin, AtomicU128, u128);
+    #[cfg(target_has_atomic = "ptr")]
+    rmw_harness!(harness_atomic_umin_usize, atomic_umin, AtomicUsize, usize);
+
+    // Pointer harnesses for atomic_swap.
+    #[cfg(target_has_atomic = "ptr")]
+    #[kani::proof_for_contract(atomic_swap::<*mut u8>)]
+    pub fn harness_atomic_swap_ptr() {
+        let initial = kani::any::<usize>() as *mut u8;
+        let storage = AtomicPtr::<u8>::new(initial);
+        let val = kani::any::<usize>() as *mut u8;
+
+        let _ = unsafe { atomic_swap(storage.as_ptr(), val, any_ordering()) };
+        kani::cover(true, "atomic_swap: reached after call");
+    }
+
+    // Harnesses for atomic_add, atomic_sub, atomic_and, atomic_nand, atomic_or, and atomic_xor.
+    macro_rules! binary_rmw_harness {
+        ($name:ident, $operation:ident, $atomic:ty, $value:ty) => {
+            #[kani::proof_for_contract($operation::<$value, $value>)]
+            pub fn $name() {
+                let initial: $value = kani::any();
+                let storage = <$atomic>::new(initial);
+                let val: $value = kani::any();
+
+                let _ = unsafe { $operation(storage.as_ptr(), val, any_ordering()) };
+                kani::cover(true, "atomic_add/sub/and/nand/or/xor: reached after call");
+            }
+        };
+    }
+
+    // Pointer versions use a usize operand; raw pointers do not implement kani::Arbitrary.
+    macro_rules! binary_rmw_ptr_harness {
+        ($name:ident, $operation:ident, $pointee:ty) => {
+            #[kani::proof_for_contract($operation::<*mut $pointee, usize>)]
+            pub fn $name() {
+                let initial = kani::any::<usize>() as *mut $pointee;
+                let storage = AtomicPtr::<$pointee>::new(initial);
+                let val: usize = kani::any();
+
+                let _ = unsafe { $operation(storage.as_ptr(), val, any_ordering()) };
+                kani::cover(true, "atomic pointer binary RMW: reached after call");
+            }
+        };
+    }
+
+    // Add helpers.
+    #[cfg(target_has_atomic = "8")]
+    binary_rmw_harness!(harness_atomic_add_i8, atomic_add, AtomicI8, i8);
+    #[cfg(target_has_atomic = "8")]
+    binary_rmw_harness!(harness_atomic_add_u8, atomic_add, AtomicU8, u8);
+    #[cfg(target_has_atomic = "16")]
+    binary_rmw_harness!(harness_atomic_add_i16, atomic_add, AtomicI16, i16);
+    #[cfg(target_has_atomic = "16")]
+    binary_rmw_harness!(harness_atomic_add_u16, atomic_add, AtomicU16, u16);
+    #[cfg(target_has_atomic = "32")]
+    binary_rmw_harness!(harness_atomic_add_i32, atomic_add, AtomicI32, i32);
+    #[cfg(target_has_atomic = "32")]
+    binary_rmw_harness!(harness_atomic_add_u32, atomic_add, AtomicU32, u32);
+    #[cfg(target_has_atomic = "64")]
+    binary_rmw_harness!(harness_atomic_add_i64, atomic_add, AtomicI64, i64);
+    #[cfg(target_has_atomic = "64")]
+    binary_rmw_harness!(harness_atomic_add_u64, atomic_add, AtomicU64, u64);
+    #[cfg(target_has_atomic = "128")]
+    binary_rmw_harness!(harness_atomic_add_i128, atomic_add, AtomicI128, i128);
+    #[cfg(target_has_atomic = "128")]
+    binary_rmw_harness!(harness_atomic_add_u128, atomic_add, AtomicU128, u128);
+    #[cfg(target_has_atomic = "ptr")]
+    binary_rmw_harness!(harness_atomic_add_isize, atomic_add, AtomicIsize, isize);
+    #[cfg(target_has_atomic = "ptr")]
+    binary_rmw_harness!(harness_atomic_add_usize, atomic_add, AtomicUsize, usize);
+    #[cfg(target_has_atomic = "ptr")]
+    binary_rmw_ptr_harness!(harness_atomic_add_ptr, atomic_add, u8);
+
+    // Subtract helpers.
+    #[cfg(target_has_atomic = "8")]
+    binary_rmw_harness!(harness_atomic_sub_i8, atomic_sub, AtomicI8, i8);
+    #[cfg(target_has_atomic = "8")]
+    binary_rmw_harness!(harness_atomic_sub_u8, atomic_sub, AtomicU8, u8);
+    #[cfg(target_has_atomic = "16")]
+    binary_rmw_harness!(harness_atomic_sub_i16, atomic_sub, AtomicI16, i16);
+    #[cfg(target_has_atomic = "16")]
+    binary_rmw_harness!(harness_atomic_sub_u16, atomic_sub, AtomicU16, u16);
+    #[cfg(target_has_atomic = "32")]
+    binary_rmw_harness!(harness_atomic_sub_i32, atomic_sub, AtomicI32, i32);
+    #[cfg(target_has_atomic = "32")]
+    binary_rmw_harness!(harness_atomic_sub_u32, atomic_sub, AtomicU32, u32);
+    #[cfg(target_has_atomic = "64")]
+    binary_rmw_harness!(harness_atomic_sub_i64, atomic_sub, AtomicI64, i64);
+    #[cfg(target_has_atomic = "64")]
+    binary_rmw_harness!(harness_atomic_sub_u64, atomic_sub, AtomicU64, u64);
+    #[cfg(target_has_atomic = "128")]
+    binary_rmw_harness!(harness_atomic_sub_i128, atomic_sub, AtomicI128, i128);
+    #[cfg(target_has_atomic = "128")]
+    binary_rmw_harness!(harness_atomic_sub_u128, atomic_sub, AtomicU128, u128);
+    #[cfg(target_has_atomic = "ptr")]
+    binary_rmw_harness!(harness_atomic_sub_isize, atomic_sub, AtomicIsize, isize);
+    #[cfg(target_has_atomic = "ptr")]
+    binary_rmw_harness!(harness_atomic_sub_usize, atomic_sub, AtomicUsize, usize);
+    #[cfg(target_has_atomic = "ptr")]
+    binary_rmw_ptr_harness!(harness_atomic_sub_ptr, atomic_sub, u8);
+
+    // Bitwise AND helpers.
+    #[cfg(target_has_atomic = "8")]
+    binary_rmw_harness!(harness_atomic_and_i8, atomic_and, AtomicI8, i8);
+    #[cfg(target_has_atomic = "8")]
+    binary_rmw_harness!(harness_atomic_and_u8, atomic_and, AtomicU8, u8);
+    #[cfg(target_has_atomic = "16")]
+    binary_rmw_harness!(harness_atomic_and_i16, atomic_and, AtomicI16, i16);
+    #[cfg(target_has_atomic = "16")]
+    binary_rmw_harness!(harness_atomic_and_u16, atomic_and, AtomicU16, u16);
+    #[cfg(target_has_atomic = "32")]
+    binary_rmw_harness!(harness_atomic_and_i32, atomic_and, AtomicI32, i32);
+    #[cfg(target_has_atomic = "32")]
+    binary_rmw_harness!(harness_atomic_and_u32, atomic_and, AtomicU32, u32);
+    #[cfg(target_has_atomic = "64")]
+    binary_rmw_harness!(harness_atomic_and_i64, atomic_and, AtomicI64, i64);
+    #[cfg(target_has_atomic = "64")]
+    binary_rmw_harness!(harness_atomic_and_u64, atomic_and, AtomicU64, u64);
+    #[cfg(target_has_atomic = "128")]
+    binary_rmw_harness!(harness_atomic_and_i128, atomic_and, AtomicI128, i128);
+    #[cfg(target_has_atomic = "128")]
+    binary_rmw_harness!(harness_atomic_and_u128, atomic_and, AtomicU128, u128);
+    #[cfg(target_has_atomic = "ptr")]
+    binary_rmw_harness!(harness_atomic_and_isize, atomic_and, AtomicIsize, isize);
+    #[cfg(target_has_atomic = "ptr")]
+    binary_rmw_harness!(harness_atomic_and_usize, atomic_and, AtomicUsize, usize);
+    #[cfg(target_has_atomic = "ptr")]
+    binary_rmw_ptr_harness!(harness_atomic_and_ptr, atomic_and, u8);
+
+    // Bitwise NAND helpers.
+    #[cfg(target_has_atomic = "8")]
+    binary_rmw_harness!(harness_atomic_nand_i8, atomic_nand, AtomicI8, i8);
+    #[cfg(target_has_atomic = "8")]
+    binary_rmw_harness!(harness_atomic_nand_u8, atomic_nand, AtomicU8, u8);
+    #[cfg(target_has_atomic = "16")]
+    binary_rmw_harness!(harness_atomic_nand_i16, atomic_nand, AtomicI16, i16);
+    #[cfg(target_has_atomic = "16")]
+    binary_rmw_harness!(harness_atomic_nand_u16, atomic_nand, AtomicU16, u16);
+    #[cfg(target_has_atomic = "32")]
+    binary_rmw_harness!(harness_atomic_nand_i32, atomic_nand, AtomicI32, i32);
+    #[cfg(target_has_atomic = "32")]
+    binary_rmw_harness!(harness_atomic_nand_u32, atomic_nand, AtomicU32, u32);
+    #[cfg(target_has_atomic = "64")]
+    binary_rmw_harness!(harness_atomic_nand_i64, atomic_nand, AtomicI64, i64);
+    #[cfg(target_has_atomic = "64")]
+    binary_rmw_harness!(harness_atomic_nand_u64, atomic_nand, AtomicU64, u64);
+    #[cfg(target_has_atomic = "128")]
+    binary_rmw_harness!(harness_atomic_nand_i128, atomic_nand, AtomicI128, i128);
+    #[cfg(target_has_atomic = "128")]
+    binary_rmw_harness!(harness_atomic_nand_u128, atomic_nand, AtomicU128, u128);
+    #[cfg(target_has_atomic = "ptr")]
+    binary_rmw_harness!(harness_atomic_nand_isize, atomic_nand, AtomicIsize, isize);
+    #[cfg(target_has_atomic = "ptr")]
+    binary_rmw_harness!(harness_atomic_nand_usize, atomic_nand, AtomicUsize, usize);
+
+    // Bitwise OR helpers.
+    #[cfg(target_has_atomic = "8")]
+    binary_rmw_harness!(harness_atomic_or_i8, atomic_or, AtomicI8, i8);
+    #[cfg(target_has_atomic = "8")]
+    binary_rmw_harness!(harness_atomic_or_u8, atomic_or, AtomicU8, u8);
+    #[cfg(target_has_atomic = "16")]
+    binary_rmw_harness!(harness_atomic_or_i16, atomic_or, AtomicI16, i16);
+    #[cfg(target_has_atomic = "16")]
+    binary_rmw_harness!(harness_atomic_or_u16, atomic_or, AtomicU16, u16);
+    #[cfg(target_has_atomic = "32")]
+    binary_rmw_harness!(harness_atomic_or_i32, atomic_or, AtomicI32, i32);
+    #[cfg(target_has_atomic = "32")]
+    binary_rmw_harness!(harness_atomic_or_u32, atomic_or, AtomicU32, u32);
+    #[cfg(target_has_atomic = "64")]
+    binary_rmw_harness!(harness_atomic_or_i64, atomic_or, AtomicI64, i64);
+    #[cfg(target_has_atomic = "64")]
+    binary_rmw_harness!(harness_atomic_or_u64, atomic_or, AtomicU64, u64);
+    #[cfg(target_has_atomic = "128")]
+    binary_rmw_harness!(harness_atomic_or_i128, atomic_or, AtomicI128, i128);
+    #[cfg(target_has_atomic = "128")]
+    binary_rmw_harness!(harness_atomic_or_u128, atomic_or, AtomicU128, u128);
+    #[cfg(target_has_atomic = "ptr")]
+    binary_rmw_harness!(harness_atomic_or_isize, atomic_or, AtomicIsize, isize);
+    #[cfg(target_has_atomic = "ptr")]
+    binary_rmw_harness!(harness_atomic_or_usize, atomic_or, AtomicUsize, usize);
+    #[cfg(target_has_atomic = "ptr")]
+    binary_rmw_ptr_harness!(harness_atomic_or_ptr, atomic_or, u8);
+
+    // Bitwise XOR helpers.
+    #[cfg(target_has_atomic = "8")]
+    binary_rmw_harness!(harness_atomic_xor_i8, atomic_xor, AtomicI8, i8);
+    #[cfg(target_has_atomic = "8")]
+    binary_rmw_harness!(harness_atomic_xor_u8, atomic_xor, AtomicU8, u8);
+    #[cfg(target_has_atomic = "16")]
+    binary_rmw_harness!(harness_atomic_xor_i16, atomic_xor, AtomicI16, i16);
+    #[cfg(target_has_atomic = "16")]
+    binary_rmw_harness!(harness_atomic_xor_u16, atomic_xor, AtomicU16, u16);
+    #[cfg(target_has_atomic = "32")]
+    binary_rmw_harness!(harness_atomic_xor_i32, atomic_xor, AtomicI32, i32);
+    #[cfg(target_has_atomic = "32")]
+    binary_rmw_harness!(harness_atomic_xor_u32, atomic_xor, AtomicU32, u32);
+    #[cfg(target_has_atomic = "64")]
+    binary_rmw_harness!(harness_atomic_xor_i64, atomic_xor, AtomicI64, i64);
+    #[cfg(target_has_atomic = "64")]
+    binary_rmw_harness!(harness_atomic_xor_u64, atomic_xor, AtomicU64, u64);
+    #[cfg(target_has_atomic = "128")]
+    binary_rmw_harness!(harness_atomic_xor_i128, atomic_xor, AtomicI128, i128);
+    #[cfg(target_has_atomic = "128")]
+    binary_rmw_harness!(harness_atomic_xor_u128, atomic_xor, AtomicU128, u128);
+    #[cfg(target_has_atomic = "ptr")]
+    binary_rmw_harness!(harness_atomic_xor_isize, atomic_xor, AtomicIsize, isize);
+    #[cfg(target_has_atomic = "ptr")]
+    binary_rmw_harness!(harness_atomic_xor_usize, atomic_xor, AtomicUsize, usize);
+    #[cfg(target_has_atomic = "ptr")]
+    binary_rmw_ptr_harness!(harness_atomic_xor_ptr, atomic_xor, u8);
+
+    // Harnesses for atomic_compare_exchange and atomic_compare_exchange_weak.
+    macro_rules! compare_exchange_harness {
+        ($name:ident, $operation:ident, $atomic:ty, $value:ty) => {
+            #[kani::proof_for_contract($operation::<$value>)]
+            pub fn $name() {
+                let initial: $value = kani::any();
+                let storage = <$atomic>::new(initial);
+                let old: $value = kani::any();
+                let new: $value = kani::any();
+
+                let _ = unsafe {
+                    $operation(storage.as_ptr(), old, new, any_ordering(), any_ordering())
+                };
+                kani::cover(true, "atomic_compare_exchange/weak: reached after call");
+            }
+        };
+    }
+
+    // Strong compare-exchange helpers.
+    #[cfg(target_has_atomic = "8")]
+    compare_exchange_harness!(
+        harness_atomic_compare_exchange_i8,
+        atomic_compare_exchange,
+        AtomicI8,
+        i8
+    );
+    #[cfg(target_has_atomic = "8")]
+    compare_exchange_harness!(
+        harness_atomic_compare_exchange_u8,
+        atomic_compare_exchange,
+        AtomicU8,
+        u8
+    );
+    #[cfg(target_has_atomic = "16")]
+    compare_exchange_harness!(
+        harness_atomic_compare_exchange_i16,
+        atomic_compare_exchange,
+        AtomicI16,
+        i16
+    );
+    #[cfg(target_has_atomic = "16")]
+    compare_exchange_harness!(
+        harness_atomic_compare_exchange_u16,
+        atomic_compare_exchange,
+        AtomicU16,
+        u16
+    );
+    #[cfg(target_has_atomic = "32")]
+    compare_exchange_harness!(
+        harness_atomic_compare_exchange_i32,
+        atomic_compare_exchange,
+        AtomicI32,
+        i32
+    );
+    #[cfg(target_has_atomic = "32")]
+    compare_exchange_harness!(
+        harness_atomic_compare_exchange_u32,
+        atomic_compare_exchange,
+        AtomicU32,
+        u32
+    );
+    #[cfg(target_has_atomic = "64")]
+    compare_exchange_harness!(
+        harness_atomic_compare_exchange_i64,
+        atomic_compare_exchange,
+        AtomicI64,
+        i64
+    );
+    #[cfg(target_has_atomic = "64")]
+    compare_exchange_harness!(
+        harness_atomic_compare_exchange_u64,
+        atomic_compare_exchange,
+        AtomicU64,
+        u64
+    );
+    #[cfg(target_has_atomic = "128")]
+    compare_exchange_harness!(
+        harness_atomic_compare_exchange_i128,
+        atomic_compare_exchange,
+        AtomicI128,
+        i128
+    );
+    #[cfg(target_has_atomic = "128")]
+    compare_exchange_harness!(
+        harness_atomic_compare_exchange_u128,
+        atomic_compare_exchange,
+        AtomicU128,
+        u128
+    );
+    #[cfg(target_has_atomic = "ptr")]
+    compare_exchange_harness!(
+        harness_atomic_compare_exchange_isize,
+        atomic_compare_exchange,
+        AtomicIsize,
+        isize
+    );
+    #[cfg(target_has_atomic = "ptr")]
+    compare_exchange_harness!(
+        harness_atomic_compare_exchange_usize,
+        atomic_compare_exchange,
+        AtomicUsize,
+        usize
+    );
+
+    // Weak compare-exchange helpers.
+    #[cfg(target_has_atomic = "8")]
+    compare_exchange_harness!(
+        harness_atomic_compare_exchange_weak_i8,
+        atomic_compare_exchange_weak,
+        AtomicI8,
+        i8
+    );
+    #[cfg(target_has_atomic = "8")]
+    compare_exchange_harness!(
+        harness_atomic_compare_exchange_weak_u8,
+        atomic_compare_exchange_weak,
+        AtomicU8,
+        u8
+    );
+    #[cfg(target_has_atomic = "16")]
+    compare_exchange_harness!(
+        harness_atomic_compare_exchange_weak_i16,
+        atomic_compare_exchange_weak,
+        AtomicI16,
+        i16
+    );
+    #[cfg(target_has_atomic = "16")]
+    compare_exchange_harness!(
+        harness_atomic_compare_exchange_weak_u16,
+        atomic_compare_exchange_weak,
+        AtomicU16,
+        u16
+    );
+    #[cfg(target_has_atomic = "32")]
+    compare_exchange_harness!(
+        harness_atomic_compare_exchange_weak_i32,
+        atomic_compare_exchange_weak,
+        AtomicI32,
+        i32
+    );
+    #[cfg(target_has_atomic = "32")]
+    compare_exchange_harness!(
+        harness_atomic_compare_exchange_weak_u32,
+        atomic_compare_exchange_weak,
+        AtomicU32,
+        u32
+    );
+    #[cfg(target_has_atomic = "64")]
+    compare_exchange_harness!(
+        harness_atomic_compare_exchange_weak_i64,
+        atomic_compare_exchange_weak,
+        AtomicI64,
+        i64
+    );
+    #[cfg(target_has_atomic = "64")]
+    compare_exchange_harness!(
+        harness_atomic_compare_exchange_weak_u64,
+        atomic_compare_exchange_weak,
+        AtomicU64,
+        u64
+    );
+    #[cfg(target_has_atomic = "128")]
+    compare_exchange_harness!(
+        harness_atomic_compare_exchange_weak_i128,
+        atomic_compare_exchange_weak,
+        AtomicI128,
+        i128
+    );
+    #[cfg(target_has_atomic = "128")]
+    compare_exchange_harness!(
+        harness_atomic_compare_exchange_weak_u128,
+        atomic_compare_exchange_weak,
+        AtomicU128,
+        u128
+    );
+    #[cfg(target_has_atomic = "ptr")]
+    compare_exchange_harness!(
+        harness_atomic_compare_exchange_weak_isize,
+        atomic_compare_exchange_weak,
+        AtomicIsize,
+        isize
+    );
+    #[cfg(target_has_atomic = "ptr")]
+    compare_exchange_harness!(
+        harness_atomic_compare_exchange_weak_usize,
+        atomic_compare_exchange_weak,
+        AtomicUsize,
+        usize
+    );
+
+    // Pointer harnesses for atomic_compare_exchange and atomic_compare_exchange_weak.
+    macro_rules! compare_exchange_ptr_harness {
+        ($name:ident, $operation:ident, $pointee:ty) => {
+            #[kani::proof_for_contract($operation::<*mut $pointee>)]
+            pub fn $name() {
+                let initial = kani::any::<usize>() as *mut $pointee;
+                let storage = AtomicPtr::<$pointee>::new(initial);
+                let old = kani::any::<usize>() as *mut $pointee;
+                let new = kani::any::<usize>() as *mut $pointee;
+
+                let _ = unsafe {
+                    $operation(storage.as_ptr(), old, new, any_ordering(), any_ordering())
+                };
+                kani::cover(true, "atomic_compare_exchange/weak: reached after call");
+            }
+        };
+    }
+
+    #[cfg(target_has_atomic = "ptr")]
+    compare_exchange_ptr_harness!(harness_atomic_compare_exchange_ptr, atomic_compare_exchange, u8);
+    #[cfg(target_has_atomic = "ptr")]
+    compare_exchange_ptr_harness!(
+        harness_atomic_compare_exchange_weak_ptr,
+        atomic_compare_exchange_weak,
+        u8
+    );
+
+    // Part 2 (optional): safe atomic abstractions and ordering contracts.
+    fn any_load_order() -> Ordering {
+        match kani::any::<u8>() % 3 {
+            0 => Relaxed,
+            1 => Acquire,
+            _ => SeqCst,
+        }
+    }
+
+    fn any_store_order() -> Ordering {
+        match kani::any::<u8>() % 3 {
+            0 => Relaxed,
+            1 => Release,
+            _ => SeqCst,
+        }
+    }
+
+    fn any_failure_order() -> Ordering {
+        any_load_order()
+    }
+
+    // Harnesses for load and store methods of atomic types, with safe abstractions.
+    macro_rules! safe_load_store_harness {
+        ($load_name:ident, $store_name:ident, $atomic:ty, $value:ty) => {
+            #[kani::proof_for_contract(Atomic::<$value>::load)]
+            pub fn $load_name() {
+                let storage = <$atomic>::new(kani::any::<$value>());
+                let _ = storage.load(any_load_order());
+                kani::cover(true, "safe atomic load: reached after call");
+            }
+
+            #[kani::proof_for_contract(Atomic::<$value>::store)]
+            pub fn $store_name() {
+                let storage = <$atomic>::new(kani::any::<$value>());
+                storage.store(kani::any::<$value>(), any_store_order());
+                kani::cover(true, "safe atomic store: reached after call");
+            }
+        };
+    }
+
+    #[cfg(target_has_atomic_load_store = "8")]
+    safe_load_store_harness!(harness_safe_load_bool, harness_safe_store_bool, AtomicBool, bool);
+    #[cfg(target_has_atomic_load_store = "8")]
+    safe_load_store_harness!(harness_safe_load_i8, harness_safe_store_i8, AtomicI8, i8);
+    #[cfg(target_has_atomic_load_store = "8")]
+    safe_load_store_harness!(harness_safe_load_u8, harness_safe_store_u8, AtomicU8, u8);
+    #[cfg(target_has_atomic_load_store = "16")]
+    safe_load_store_harness!(harness_safe_load_i16, harness_safe_store_i16, AtomicI16, i16);
+    #[cfg(target_has_atomic_load_store = "16")]
+    safe_load_store_harness!(harness_safe_load_u16, harness_safe_store_u16, AtomicU16, u16);
+    #[cfg(target_has_atomic_load_store = "32")]
+    safe_load_store_harness!(harness_safe_load_i32, harness_safe_store_i32, AtomicI32, i32);
+    #[cfg(target_has_atomic_load_store = "32")]
+    safe_load_store_harness!(harness_safe_load_u32, harness_safe_store_u32, AtomicU32, u32);
+    #[cfg(target_has_atomic_load_store = "64")]
+    safe_load_store_harness!(harness_safe_load_i64, harness_safe_store_i64, AtomicI64, i64);
+    #[cfg(target_has_atomic_load_store = "64")]
+    safe_load_store_harness!(harness_safe_load_u64, harness_safe_store_u64, AtomicU64, u64);
+    #[cfg(target_has_atomic_load_store = "128")]
+    safe_load_store_harness!(harness_safe_load_i128, harness_safe_store_i128, AtomicI128, i128);
+    #[cfg(target_has_atomic_load_store = "128")]
+    safe_load_store_harness!(harness_safe_load_u128, harness_safe_store_u128, AtomicU128, u128);
+    #[cfg(target_has_atomic_load_store = "ptr")]
+    safe_load_store_harness!(harness_safe_load_isize, harness_safe_store_isize, AtomicIsize, isize);
+    #[cfg(target_has_atomic_load_store = "ptr")]
+    safe_load_store_harness!(harness_safe_load_usize, harness_safe_store_usize, AtomicUsize, usize);
+
+    #[cfg(target_has_atomic_load_store = "ptr")]
+    #[kani::proof_for_contract(Atomic::<*mut T>::load)]
+    pub fn harness_safe_load_ptr() {
+        let storage = AtomicPtr::<u8>::new(kani::any::<usize>() as *mut u8);
+        let _ = storage.load(any_load_order());
+        kani::cover(true, "safe atomic pointer load: reached after call");
+    }
+
+    #[cfg(target_has_atomic_load_store = "ptr")]
+    #[kani::proof_for_contract(Atomic::<*mut T>::store)]
+    pub fn harness_safe_store_ptr() {
+        let storage = AtomicPtr::<u8>::new(kani::any::<usize>() as *mut u8);
+        storage.store(kani::any::<usize>() as *mut u8, any_store_order());
+        kani::cover(true, "safe atomic pointer store: reached after call");
+    }
+
+    macro_rules! safe_compare_exchange_harness {
+        ($name:ident, $atomic:ty, $value:ty, $method:ident) => {
+            #[kani::proof_for_contract(Atomic::<$value>::$method)]
+            pub fn $name() {
+                let storage = <$atomic>::new(kani::any::<$value>());
+                let _ = storage.$method(
+                    kani::any::<$value>(),
+                    kani::any::<$value>(),
+                    any_ordering(),
+                    any_failure_order(),
+                );
+                kani::cover(true, "safe atomic compare-exchange: reached after call");
+            }
+        };
+    }
+
+    #[cfg(target_has_atomic = "8")]
+    safe_compare_exchange_harness!(
+        harness_safe_compare_exchange_bool,
+        AtomicBool,
+        bool,
+        compare_exchange
+    );
+    #[cfg(target_has_atomic = "8")]
+    safe_compare_exchange_harness!(
+        harness_safe_compare_exchange_weak_bool,
+        AtomicBool,
+        bool,
+        compare_exchange_weak
+    );
+    #[cfg(target_has_atomic = "ptr")]
+    #[kani::proof_for_contract(Atomic::<*mut T>::compare_exchange)]
+    pub fn harness_safe_compare_exchange_ptr() {
+        let storage = AtomicPtr::<u8>::new(kani::any::<usize>() as *mut u8);
+        let _ = storage.compare_exchange(
+            kani::any::<usize>() as *mut u8,
+            kani::any::<usize>() as *mut u8,
+            any_ordering(),
+            any_failure_order(),
+        );
+        kani::cover(true, "safe atomic pointer compare-exchange: reached after call");
+    }
+    #[cfg(target_has_atomic = "ptr")]
+    #[kani::proof_for_contract(Atomic::<*mut T>::compare_exchange_weak)]
+    pub fn harness_safe_compare_exchange_weak_ptr() {
+        let storage = AtomicPtr::<u8>::new(kani::any::<usize>() as *mut u8);
+        let _ = storage.compare_exchange_weak(
+            kani::any::<usize>() as *mut u8,
+            kani::any::<usize>() as *mut u8,
+            any_ordering(),
+            any_failure_order(),
+        );
+        kani::cover(true, "safe atomic pointer weak compare-exchange: reached after call");
+    }
+    #[cfg(target_has_atomic = "8")]
+    safe_compare_exchange_harness!(
+        harness_safe_compare_exchange_u8,
+        AtomicU8,
+        u8,
+        compare_exchange
+    );
+    #[cfg(target_has_atomic = "8")]
+    safe_compare_exchange_harness!(
+        harness_safe_compare_exchange_weak_u8,
+        AtomicU8,
+        u8,
+        compare_exchange_weak
+    );
+    #[cfg(target_has_atomic = "8")]
+    safe_compare_exchange_harness!(
+        harness_safe_compare_exchange_i8,
+        AtomicI8,
+        i8,
+        compare_exchange
+    );
+    #[cfg(target_has_atomic = "8")]
+    safe_compare_exchange_harness!(
+        harness_safe_compare_exchange_weak_i8,
+        AtomicI8,
+        i8,
+        compare_exchange_weak
+    );
+    #[cfg(target_has_atomic = "16")]
+    safe_compare_exchange_harness!(
+        harness_safe_compare_exchange_i16,
+        AtomicI16,
+        i16,
+        compare_exchange
+    );
+    #[cfg(target_has_atomic = "16")]
+    safe_compare_exchange_harness!(
+        harness_safe_compare_exchange_weak_i16,
+        AtomicI16,
+        i16,
+        compare_exchange_weak
+    );
+    #[cfg(target_has_atomic = "16")]
+    safe_compare_exchange_harness!(
+        harness_safe_compare_exchange_u16,
+        AtomicU16,
+        u16,
+        compare_exchange
+    );
+    #[cfg(target_has_atomic = "16")]
+    safe_compare_exchange_harness!(
+        harness_safe_compare_exchange_weak_u16,
+        AtomicU16,
+        u16,
+        compare_exchange_weak
+    );
+    #[cfg(target_has_atomic = "32")]
+    safe_compare_exchange_harness!(
+        harness_safe_compare_exchange_i32,
+        AtomicI32,
+        i32,
+        compare_exchange
+    );
+    #[cfg(target_has_atomic = "32")]
+    safe_compare_exchange_harness!(
+        harness_safe_compare_exchange_weak_i32,
+        AtomicI32,
+        i32,
+        compare_exchange_weak
+    );
+    #[cfg(target_has_atomic = "32")]
+    safe_compare_exchange_harness!(
+        harness_safe_compare_exchange_u32,
+        AtomicU32,
+        u32,
+        compare_exchange
+    );
+    #[cfg(target_has_atomic = "32")]
+    safe_compare_exchange_harness!(
+        harness_safe_compare_exchange_weak_u32,
+        AtomicU32,
+        u32,
+        compare_exchange_weak
+    );
+    #[cfg(target_has_atomic = "64")]
+    safe_compare_exchange_harness!(
+        harness_safe_compare_exchange_i64,
+        AtomicI64,
+        i64,
+        compare_exchange
+    );
+    #[cfg(target_has_atomic = "64")]
+    safe_compare_exchange_harness!(
+        harness_safe_compare_exchange_weak_i64,
+        AtomicI64,
+        i64,
+        compare_exchange_weak
+    );
+    #[cfg(target_has_atomic = "64")]
+    safe_compare_exchange_harness!(
+        harness_safe_compare_exchange_u64,
+        AtomicU64,
+        u64,
+        compare_exchange
+    );
+    #[cfg(target_has_atomic = "64")]
+    safe_compare_exchange_harness!(
+        harness_safe_compare_exchange_weak_u64,
+        AtomicU64,
+        u64,
+        compare_exchange_weak
+    );
+    #[cfg(target_has_atomic = "128")]
+    safe_compare_exchange_harness!(
+        harness_safe_compare_exchange_i128,
+        AtomicI128,
+        i128,
+        compare_exchange
+    );
+    #[cfg(target_has_atomic = "128")]
+    safe_compare_exchange_harness!(
+        harness_safe_compare_exchange_weak_i128,
+        AtomicI128,
+        i128,
+        compare_exchange_weak
+    );
+    #[cfg(target_has_atomic = "128")]
+    safe_compare_exchange_harness!(
+        harness_safe_compare_exchange_u128,
+        AtomicU128,
+        u128,
+        compare_exchange
+    );
+    #[cfg(target_has_atomic = "128")]
+    safe_compare_exchange_harness!(
+        harness_safe_compare_exchange_weak_u128,
+        AtomicU128,
+        u128,
+        compare_exchange_weak
+    );
+    #[cfg(target_has_atomic = "ptr")]
+    safe_compare_exchange_harness!(
+        harness_safe_compare_exchange_isize,
+        AtomicIsize,
+        isize,
+        compare_exchange
+    );
+    #[cfg(target_has_atomic = "ptr")]
+    safe_compare_exchange_harness!(
+        harness_safe_compare_exchange_weak_isize,
+        AtomicIsize,
+        isize,
+        compare_exchange_weak
+    );
+    #[cfg(target_has_atomic = "ptr")]
+    safe_compare_exchange_harness!(
+        harness_safe_compare_exchange_usize,
+        AtomicUsize,
+        usize,
+        compare_exchange
+    );
+    #[cfg(target_has_atomic = "ptr")]
+    safe_compare_exchange_harness!(
+        harness_safe_compare_exchange_weak_usize,
+        AtomicUsize,
+        usize,
+        compare_exchange_weak
+    );
+
+    // Callback-taking methods use ordinary proofs: a callback may legally write to
+    // captured state or other memory, so `modifies(self)` is not a valid general
+    // contract for these APIs. Keep the former ordering precondition explicit in
+    // each harness instead. The callbacks below mutate captured state to exercise
+    // this case; the proofs cover these callbacks, not every possible FnMut.
+    // As with the other harnesses, this is single-threaded verification.
+    macro_rules! safe_update_harness {
+        ($name:ident, $atomic:ty, $value:ty, $method:ident) => {
+            #[kani::proof]
+            #[kani::unwind(2)]
+            pub fn $name() {
+                let initial: $value = kani::any();
+                let storage = <$atomic>::new(initial);
+                let new: $value = kani::any();
+                let should_update: bool = kani::any();
+                let set_order = any_ordering();
+                let fetch_order = any_ordering();
+                kani::assume(matches!(fetch_order, Relaxed | Acquire | SeqCst));
+                let mut calls = 0u32;
+                let result = storage.$method(set_order, fetch_order, |_| {
+                    calls += 1;
+                    if should_update { Some(new) } else { None }
+                });
+                assert!(calls > 0);
+                assert_eq!(result, if should_update { Ok(initial) } else { Err(initial) });
+                assert_eq!(storage.load(Relaxed), if should_update { new } else { initial });
+                kani::cover(result.is_ok(), "safe atomic update: Some branch completed");
+                kani::cover(result.is_err(), "safe atomic update: None branch completed");
+                kani::cover(true, "safe atomic update: reached after call");
+            }
+        };
+    }
+
+    #[cfg(target_has_atomic = "8")]
+    safe_update_harness!(harness_safe_fetch_update_bool, AtomicBool, bool, fetch_update);
+    #[cfg(target_has_atomic = "8")]
+    safe_update_harness!(harness_safe_try_update_bool, AtomicBool, bool, try_update);
+    #[cfg(target_has_atomic = "ptr")]
+    #[kani::proof]
+    #[kani::unwind(2)]
+    pub fn harness_safe_fetch_update_ptr() {
+        let initial = kani::any::<usize>() as *mut u8;
+        let storage = AtomicPtr::<u8>::new(initial);
+        let new = kani::any::<usize>() as *mut u8;
+        let should_update: bool = kani::any();
+        let set_order = any_ordering();
+        let fetch_order = any_ordering();
+        kani::assume(matches!(fetch_order, Relaxed | Acquire | SeqCst));
+        let mut calls = 0u32;
+        let result = storage.fetch_update(set_order, fetch_order, |_| {
+            calls += 1;
+            if should_update { Some(new) } else { None }
+        });
+        assert!(calls > 0);
+        assert_eq!(result, if should_update { Ok(initial) } else { Err(initial) });
+        assert_eq!(storage.load(Relaxed), if should_update { new } else { initial });
+        kani::cover(result.is_ok(), "safe pointer fetch-update: Some branch completed");
+        kani::cover(result.is_err(), "safe pointer fetch-update: None branch completed");
+        kani::cover(true, "safe atomic pointer fetch-update: reached after call");
+    }
+    #[cfg(target_has_atomic = "ptr")]
+    #[kani::proof]
+    #[kani::unwind(2)]
+    pub fn harness_safe_try_update_ptr() {
+        let initial = kani::any::<usize>() as *mut u8;
+        let storage = AtomicPtr::<u8>::new(initial);
+        let new = kani::any::<usize>() as *mut u8;
+        let should_update: bool = kani::any();
+        let set_order = any_ordering();
+        let fetch_order = any_ordering();
+        kani::assume(matches!(fetch_order, Relaxed | Acquire | SeqCst));
+        let mut calls = 0u32;
+        let result = storage.try_update(set_order, fetch_order, |_| {
+            calls += 1;
+            if should_update { Some(new) } else { None }
+        });
+        assert!(calls > 0);
+        assert_eq!(result, if should_update { Ok(initial) } else { Err(initial) });
+        assert_eq!(storage.load(Relaxed), if should_update { new } else { initial });
+        kani::cover(result.is_ok(), "safe pointer try-update: Some branch completed");
+        kani::cover(result.is_err(), "safe pointer try-update: None branch completed");
+        kani::cover(true, "safe atomic pointer try-update: reached after call");
+    }
+    #[cfg(target_has_atomic = "8")]
+    safe_update_harness!(harness_safe_fetch_update_i8, AtomicI8, i8, fetch_update);
+    #[cfg(target_has_atomic = "8")]
+    safe_update_harness!(harness_safe_try_update_i8, AtomicI8, i8, try_update);
+    #[cfg(target_has_atomic = "8")]
+    safe_update_harness!(harness_safe_fetch_update_u8, AtomicU8, u8, fetch_update);
+    #[cfg(target_has_atomic = "8")]
+    safe_update_harness!(harness_safe_try_update_u8, AtomicU8, u8, try_update);
+    #[cfg(target_has_atomic = "16")]
+    safe_update_harness!(harness_safe_fetch_update_i16, AtomicI16, i16, fetch_update);
+    #[cfg(target_has_atomic = "16")]
+    safe_update_harness!(harness_safe_try_update_i16, AtomicI16, i16, try_update);
+    #[cfg(target_has_atomic = "16")]
+    safe_update_harness!(harness_safe_fetch_update_u16, AtomicU16, u16, fetch_update);
+    #[cfg(target_has_atomic = "16")]
+    safe_update_harness!(harness_safe_try_update_u16, AtomicU16, u16, try_update);
+    #[cfg(target_has_atomic = "32")]
+    safe_update_harness!(harness_safe_fetch_update_i32, AtomicI32, i32, fetch_update);
+    #[cfg(target_has_atomic = "32")]
+    safe_update_harness!(harness_safe_try_update_i32, AtomicI32, i32, try_update);
+    #[cfg(target_has_atomic = "32")]
+    safe_update_harness!(harness_safe_fetch_update_u32, AtomicU32, u32, fetch_update);
+    #[cfg(target_has_atomic = "32")]
+    safe_update_harness!(harness_safe_try_update_u32, AtomicU32, u32, try_update);
+    #[cfg(target_has_atomic = "64")]
+    safe_update_harness!(harness_safe_fetch_update_i64, AtomicI64, i64, fetch_update);
+    #[cfg(target_has_atomic = "64")]
+    safe_update_harness!(harness_safe_try_update_i64, AtomicI64, i64, try_update);
+    #[cfg(target_has_atomic = "64")]
+    safe_update_harness!(harness_safe_fetch_update_u64, AtomicU64, u64, fetch_update);
+    #[cfg(target_has_atomic = "64")]
+    safe_update_harness!(harness_safe_try_update_u64, AtomicU64, u64, try_update);
+    #[cfg(target_has_atomic = "128")]
+    safe_update_harness!(harness_safe_fetch_update_i128, AtomicI128, i128, fetch_update);
+    #[cfg(target_has_atomic = "128")]
+    safe_update_harness!(harness_safe_try_update_i128, AtomicI128, i128, try_update);
+    #[cfg(target_has_atomic = "128")]
+    safe_update_harness!(harness_safe_fetch_update_u128, AtomicU128, u128, fetch_update);
+    #[cfg(target_has_atomic = "128")]
+    safe_update_harness!(harness_safe_try_update_u128, AtomicU128, u128, try_update);
+    #[cfg(target_has_atomic = "ptr")]
+    safe_update_harness!(harness_safe_fetch_update_isize, AtomicIsize, isize, fetch_update);
+    #[cfg(target_has_atomic = "ptr")]
+    safe_update_harness!(harness_safe_try_update_isize, AtomicIsize, isize, try_update);
+    #[cfg(target_has_atomic = "ptr")]
+    safe_update_harness!(harness_safe_fetch_update_usize, AtomicUsize, usize, fetch_update);
+    #[cfg(target_has_atomic = "ptr")]
+    safe_update_harness!(harness_safe_try_update_usize, AtomicUsize, usize, try_update);
+
+    // Kani does not infer a finite bound for this CAS retry loop automatically.
+    // An unwind bound of 2 is sufficient for this single-threaded harness under
+    // Kani's current atomic intrinsic model.
+    macro_rules! safe_update_loop_harness {
+        ($name:ident, $atomic:ty, $value:ty) => {
+            #[kani::proof]
+            #[kani::unwind(2)]
+            pub fn $name() {
+                let initial: $value = kani::any();
+                let storage = <$atomic>::new(initial);
+                let new: $value = kani::any();
+                let set_order = any_ordering();
+                let fetch_order = any_ordering();
+                kani::assume(matches!(fetch_order, Relaxed | Acquire | SeqCst));
+                let mut calls = 0u32;
+                let previous = storage.update(set_order, fetch_order, |_| {
+                    calls += 1;
+                    new
+                });
+                assert!(calls > 0);
+                assert_eq!(previous, initial);
+                assert_eq!(storage.load(Relaxed), new);
+                kani::cover(true, "safe atomic update: reached after call");
+            }
+        };
+    }
+    #[cfg(target_has_atomic = "8")]
+    safe_update_loop_harness!(harness_safe_update_bool, AtomicBool, bool);
+    #[cfg(target_has_atomic = "8")]
+    safe_update_loop_harness!(harness_safe_update_i8, AtomicI8, i8);
+    #[cfg(target_has_atomic = "8")]
+    safe_update_loop_harness!(harness_safe_update_u8, AtomicU8, u8);
+    #[cfg(target_has_atomic = "16")]
+    safe_update_loop_harness!(harness_safe_update_i16, AtomicI16, i16);
+    #[cfg(target_has_atomic = "16")]
+    safe_update_loop_harness!(harness_safe_update_u16, AtomicU16, u16);
+    #[cfg(target_has_atomic = "32")]
+    safe_update_loop_harness!(harness_safe_update_i32, AtomicI32, i32);
+    #[cfg(target_has_atomic = "32")]
+    safe_update_loop_harness!(harness_safe_update_u32, AtomicU32, u32);
+    #[cfg(target_has_atomic = "64")]
+    safe_update_loop_harness!(harness_safe_update_i64, AtomicI64, i64);
+    #[cfg(target_has_atomic = "64")]
+    safe_update_loop_harness!(harness_safe_update_u64, AtomicU64, u64);
+    #[cfg(target_has_atomic = "128")]
+    safe_update_loop_harness!(harness_safe_update_i128, AtomicI128, i128);
+    #[cfg(target_has_atomic = "128")]
+    safe_update_loop_harness!(harness_safe_update_u128, AtomicU128, u128);
+    #[cfg(target_has_atomic = "ptr")]
+    safe_update_loop_harness!(harness_safe_update_isize, AtomicIsize, isize);
+    #[cfg(target_has_atomic = "ptr")]
+    safe_update_loop_harness!(harness_safe_update_usize, AtomicUsize, usize);
+
+    #[cfg(target_has_atomic = "ptr")]
+    #[kani::proof]
+    #[kani::unwind(2)]
+    pub fn harness_safe_update_ptr() {
+        let initial = kani::any::<usize>() as *mut u8;
+        let storage = AtomicPtr::<u8>::new(initial);
+        let new = kani::any::<usize>() as *mut u8;
+        let set_order = any_ordering();
+        let fetch_order = any_ordering();
+        kani::assume(matches!(fetch_order, Relaxed | Acquire | SeqCst));
+        let mut calls = 0u32;
+        let previous = storage.update(set_order, fetch_order, |_| {
+            calls += 1;
+            new
+        });
+        assert!(calls > 0);
+        assert_eq!(previous, initial);
+        assert_eq!(storage.load(Relaxed), new);
+        kani::cover(true, "safe atomic pointer update: reached after call");
+    }
+
+    #[cfg(target_has_atomic_load_store = "8")]
+    #[kani::proof]
+    #[kani::should_panic]
+    pub fn harness_safe_load_panics_on_release() {
+        let storage = AtomicBool::new(false);
+        let _ = storage.load(Release);
+    }
+
+    #[cfg(target_has_atomic_load_store = "8")]
+    #[kani::proof]
+    #[kani::should_panic]
+    pub fn harness_safe_load_panics_on_acqrel() {
+        let storage = AtomicBool::new(false);
+        let _ = storage.load(AcqRel);
+    }
+
+    #[cfg(target_has_atomic_load_store = "8")]
+    #[kani::proof]
+    #[kani::should_panic]
+    pub fn harness_safe_store_panics_on_acquire() {
+        let storage = AtomicBool::new(false);
+        storage.store(true, Acquire);
+    }
+
+    #[cfg(target_has_atomic_load_store = "8")]
+    #[kani::proof]
+    #[kani::should_panic]
+    pub fn harness_safe_store_panics_on_acqrel() {
+        let storage = AtomicBool::new(false);
+        storage.store(true, AcqRel);
+    }
+
+    macro_rules! safe_compare_exchange_panics_harness {
+        ($name:ident, $method:ident, $failure:expr) => {
+            #[cfg(target_has_atomic = "8")]
+            #[kani::proof]
+            #[kani::should_panic]
+            pub fn $name() {
+                let storage = AtomicBool::new(false);
+                let _ = storage.$method(false, true, Relaxed, $failure);
+            }
+        };
+    }
+
+    safe_compare_exchange_panics_harness!(
+        harness_safe_compare_exchange_panics_on_release,
+        compare_exchange,
+        Release
+    );
+    safe_compare_exchange_panics_harness!(
+        harness_safe_compare_exchange_panics_on_acqrel,
+        compare_exchange,
+        AcqRel
+    );
+    safe_compare_exchange_panics_harness!(
+        harness_safe_compare_exchange_weak_panics_on_release,
+        compare_exchange_weak,
+        Release
+    );
+    safe_compare_exchange_panics_harness!(
+        harness_safe_compare_exchange_weak_panics_on_acqrel,
+        compare_exchange_weak,
+        AcqRel
+    );
+
+    macro_rules! safe_update_panics_harness {
+        ($name:ident, $method:ident, $failure:expr, $closure:expr) => {
+            #[cfg(target_has_atomic = "8")]
+            #[kani::proof]
+            #[kani::should_panic]
+            pub fn $name() {
+                let storage = AtomicBool::new(false);
+                let _ = storage.$method(Relaxed, $failure, $closure);
+            }
+        };
+    }
+
+    safe_update_panics_harness!(
+        harness_safe_fetch_update_panics_on_release,
+        fetch_update,
+        Release,
+        |_| None
+    );
+    safe_update_panics_harness!(
+        harness_safe_fetch_update_panics_on_acqrel,
+        fetch_update,
+        AcqRel,
+        |_| None
+    );
+    safe_update_panics_harness!(
+        harness_safe_try_update_panics_on_release,
+        try_update,
+        Release,
+        |_| None
+    );
+    safe_update_panics_harness!(
+        harness_safe_try_update_panics_on_acqrel,
+        try_update,
+        AcqRel,
+        |_| None
+    );
+    safe_update_panics_harness!(harness_safe_update_panics_on_release, update, Release, |x| x);
+    safe_update_panics_harness!(harness_safe_update_panics_on_acqrel, update, AcqRel, |x| x);
+}