diff --git a/library/core/src/intrinsics/mod.rs b/library/core/src/intrinsics/mod.rs
index ddadeeb3c786a..6171fa004c31c 100644
--- a/library/core/src/intrinsics/mod.rs
+++ b/library/core/src/intrinsics/mod.rs
@@ -4150,4 +4150,495 @@ mod verify {
     fn supported_status(status: AllocationStatus) -> bool {
         status != AllocationStatus::Dangling && status != AllocationStatus::DeadObject
     }
+
+    // --- Challenge 7 Part 3: atomic intrinsic contracts ---
+    //
+    // `rustc_intrinsic` declarations have no body, so Kani cannot attach
+    // contracts to them (model-checking/kani#3345). These wrappers encode the
+    // documented pointer preconditions and invoke the const-generic intrinsics
+    // that replaced the older `atomic_*_{relaxed,acquire,...}` names.
+
+    // Write proofs use a live stack object. `wrapping_add` pointers lose
+    // provenance, so CBMC's assignable check fails even when `can_write` is
+    // assumed.
+
+    #[kani::modifies(dst)]
+    #[requires(ub_checks::can_write(dst))]
+    unsafe fn atomic_store_wrapper<T: Copy, const ORD: AtomicOrdering>(dst: *mut T, val: T) {
+        // SAFETY: `requires` guarantees `dst` is aligned and writable.
+        unsafe { atomic_store::<T, ORD>(dst, val) }
+    }
+
+    #[requires(ub_checks::can_dereference(src))]
+    unsafe fn atomic_load_wrapper<T: Copy, const ORD: AtomicOrdering>(src: *const T) -> T {
+        // SAFETY: `requires` guarantees `src` is aligned, allocated, and initialized.
+        unsafe { atomic_load::<T, ORD>(src) }
+    }
+
+    #[kani::modifies(dst)]
+    #[requires(ub_checks::can_dereference(dst as *const T))]
+    #[requires(ub_checks::can_write(dst))]
+    unsafe fn atomic_xchg_wrapper<T: Copy, const ORD: AtomicOrdering>(dst: *mut T, src: T) -> T {
+        // SAFETY: `requires` guarantees `dst` is valid for a read-modify-write.
+        unsafe { atomic_xchg::<T, ORD>(dst, src) }
+    }
+
+    #[kani::modifies(dst)]
+    #[requires(ub_checks::can_dereference(dst as *const T))]
+    #[requires(ub_checks::can_write(dst))]
+    unsafe fn atomic_xadd_wrapper<T: Copy, U: Copy, const ORD: AtomicOrdering>(
+        dst: *mut T,
+        src: U,
+    ) -> T {
+        // SAFETY: `requires` guarantees `dst` is valid for a read-modify-write.
+        unsafe { atomic_xadd::<T, U, ORD>(dst, src) }
+    }
+
+    #[kani::modifies(dst)]
+    #[requires(ub_checks::can_dereference(dst as *const T))]
+    #[requires(ub_checks::can_write(dst))]
+    unsafe fn atomic_xsub_wrapper<T: Copy, U: Copy, const ORD: AtomicOrdering>(
+        dst: *mut T,
+        src: U,
+    ) -> T {
+        // SAFETY: `requires` guarantees `dst` is valid for a read-modify-write.
+        unsafe { atomic_xsub::<T, U, ORD>(dst, src) }
+    }
+
+    #[kani::modifies(dst)]
+    #[requires(ub_checks::can_dereference(dst as *const T))]
+    #[requires(ub_checks::can_write(dst))]
+    unsafe fn atomic_and_wrapper<T: Copy, U: Copy, const ORD: AtomicOrdering>(
+        dst: *mut T,
+        src: U,
+    ) -> T {
+        // SAFETY: `requires` guarantees `dst` is valid for a read-modify-write.
+        unsafe { atomic_and::<T, U, ORD>(dst, src) }
+    }
+
+    #[kani::modifies(dst)]
+    #[requires(ub_checks::can_dereference(dst as *const T))]
+    #[requires(ub_checks::can_write(dst))]
+    unsafe fn atomic_nand_wrapper<T: Copy, U: Copy, const ORD: AtomicOrdering>(
+        dst: *mut T,
+        src: U,
+    ) -> T {
+        // SAFETY: `requires` guarantees `dst` is valid for a read-modify-write.
+        unsafe { atomic_nand::<T, U, ORD>(dst, src) }
+    }
+
+    #[kani::modifies(dst)]
+    #[requires(ub_checks::can_dereference(dst as *const T))]
+    #[requires(ub_checks::can_write(dst))]
+    unsafe fn atomic_or_wrapper<T: Copy, U: Copy, const ORD: AtomicOrdering>(
+        dst: *mut T,
+        src: U,
+    ) -> T {
+        // SAFETY: `requires` guarantees `dst` is valid for a read-modify-write.
+        unsafe { atomic_or::<T, U, ORD>(dst, src) }
+    }
+
+    #[kani::modifies(dst)]
+    #[requires(ub_checks::can_dereference(dst as *const T))]
+    #[requires(ub_checks::can_write(dst))]
+    unsafe fn atomic_xor_wrapper<T: Copy, U: Copy, const ORD: AtomicOrdering>(
+        dst: *mut T,
+        src: U,
+    ) -> T {
+        // SAFETY: `requires` guarantees `dst` is valid for a read-modify-write.
+        unsafe { atomic_xor::<T, U, ORD>(dst, src) }
+    }
+
+    #[kani::modifies(dst)]
+    #[requires(ub_checks::can_dereference(dst as *const T))]
+    #[requires(ub_checks::can_write(dst))]
+    unsafe fn atomic_max_wrapper<T: Copy, const ORD: AtomicOrdering>(dst: *mut T, src: T) -> T {
+        // SAFETY: `requires` guarantees `dst` is valid for a read-modify-write.
+        unsafe { atomic_max::<T, ORD>(dst, src) }
+    }
+
+    #[kani::modifies(dst)]
+    #[requires(ub_checks::can_dereference(dst as *const T))]
+    #[requires(ub_checks::can_write(dst))]
+    unsafe fn atomic_min_wrapper<T: Copy, const ORD: AtomicOrdering>(dst: *mut T, src: T) -> T {
+        // SAFETY: `requires` guarantees `dst` is valid for a read-modify-write.
+        unsafe { atomic_min::<T, ORD>(dst, src) }
+    }
+
+    #[kani::modifies(dst)]
+    #[requires(ub_checks::can_dereference(dst as *const T))]
+    #[requires(ub_checks::can_write(dst))]
+    unsafe fn atomic_umax_wrapper<T: Copy, const ORD: AtomicOrdering>(dst: *mut T, src: T) -> T {
+        // SAFETY: `requires` guarantees `dst` is valid for a read-modify-write.
+        unsafe { atomic_umax::<T, ORD>(dst, src) }
+    }
+
+    #[kani::modifies(dst)]
+    #[requires(ub_checks::can_dereference(dst as *const T))]
+    #[requires(ub_checks::can_write(dst))]
+    unsafe fn atomic_umin_wrapper<T: Copy, const ORD: AtomicOrdering>(dst: *mut T, src: T) -> T {
+        // SAFETY: `requires` guarantees `dst` is valid for a read-modify-write.
+        unsafe { atomic_umin::<T, ORD>(dst, src) }
+    }
+
+    #[kani::modifies(dst)]
+    #[requires(ub_checks::can_dereference(dst as *const T))]
+    #[requires(ub_checks::can_write(dst))]
+    unsafe fn atomic_cxchg_wrapper<
+        T: Copy,
+        const ORD_SUCC: AtomicOrdering,
+        const ORD_FAIL: AtomicOrdering,
+    >(
+        dst: *mut T,
+        old: T,
+        src: T,
+    ) -> (T, bool) {
+        // SAFETY: `requires` guarantees `dst` is valid for a read-modify-write.
+        unsafe { atomic_cxchg::<T, ORD_SUCC, ORD_FAIL>(dst, old, src) }
+    }
+
+    #[kani::modifies(dst)]
+    #[requires(ub_checks::can_dereference(dst as *const T))]
+    #[requires(ub_checks::can_write(dst))]
+    unsafe fn atomic_cxchgweak_wrapper<
+        T: Copy,
+        const ORD_SUCC: AtomicOrdering,
+        const ORD_FAIL: AtomicOrdering,
+    >(
+        dst: *mut T,
+        old: T,
+        src: T,
+    ) -> (T, bool) {
+        // SAFETY: `requires` guarantees `dst` is valid for a read-modify-write.
+        unsafe { atomic_cxchgweak::<T, ORD_SUCC, ORD_FAIL>(dst, old, src) }
+    }
+
+    macro_rules! proof_atomic_store_ord {
+        ($name:ident, $ord:ident) => {
+            #[kani::proof_for_contract(atomic_store_wrapper)]
+            fn $name() {
+                let mut val: u8 = kani::any();
+                unsafe {
+                    atomic_store_wrapper::<u8, { AtomicOrdering::$ord }>(
+                        &mut val as *mut u8,
+                        kani::any(),
+                    );
+                }
+            }
+        };
+    }
+
+    proof_atomic_store_ord!(check_atomic_store_relaxed, Relaxed);
+    proof_atomic_store_ord!(check_atomic_store_release, Release);
+    proof_atomic_store_ord!(check_atomic_store_seqcst, SeqCst);
+
+    macro_rules! proof_atomic_load_ord {
+        ($name:ident, $ord:ident) => {
+            #[kani::proof_for_contract(atomic_load_wrapper)]
+            fn $name() {
+                let val: u8 = kani::any();
+                unsafe {
+                    let _ = atomic_load_wrapper::<u8, { AtomicOrdering::$ord }>(&val as *const u8);
+                }
+            }
+        };
+    }
+
+    proof_atomic_load_ord!(check_atomic_load_relaxed, Relaxed);
+    proof_atomic_load_ord!(check_atomic_load_acquire, Acquire);
+    proof_atomic_load_ord!(check_atomic_load_seqcst, SeqCst);
+
+    macro_rules! proof_atomic_rmw_u8 {
+        ($wrapper:ident, $name:ident, $ord:ident) => {
+            #[kani::proof_for_contract($wrapper)]
+            fn $name() {
+                let mut val: u8 = kani::any();
+                unsafe {
+                    let _ =
+                        $wrapper::<u8, { AtomicOrdering::$ord }>(&mut val as *mut u8, kani::any());
+                }
+            }
+        };
+        ($wrapper:ident, $name:ident, $ord:ident, two_ty) => {
+            #[kani::proof_for_contract($wrapper)]
+            fn $name() {
+                let mut val: u8 = kani::any();
+                unsafe {
+                    let _ = $wrapper::<u8, u8, { AtomicOrdering::$ord }>(
+                        &mut val as *mut u8,
+                        kani::any(),
+                    );
+                }
+            }
+        };
+    }
+
+    proof_atomic_rmw_u8!(atomic_xchg_wrapper, check_atomic_xchg_relaxed, Relaxed);
+    proof_atomic_rmw_u8!(atomic_xchg_wrapper, check_atomic_xchg_acquire, Acquire);
+    proof_atomic_rmw_u8!(atomic_xchg_wrapper, check_atomic_xchg_release, Release);
+    proof_atomic_rmw_u8!(atomic_xchg_wrapper, check_atomic_xchg_acqrel, AcqRel);
+    proof_atomic_rmw_u8!(atomic_xchg_wrapper, check_atomic_xchg_seqcst, SeqCst);
+
+    proof_atomic_rmw_u8!(atomic_xadd_wrapper, check_atomic_xadd_relaxed, Relaxed, two_ty);
+    proof_atomic_rmw_u8!(atomic_xadd_wrapper, check_atomic_xadd_acquire, Acquire, two_ty);
+    proof_atomic_rmw_u8!(atomic_xadd_wrapper, check_atomic_xadd_release, Release, two_ty);
+    proof_atomic_rmw_u8!(atomic_xadd_wrapper, check_atomic_xadd_acqrel, AcqRel, two_ty);
+    proof_atomic_rmw_u8!(atomic_xadd_wrapper, check_atomic_xadd_seqcst, SeqCst, two_ty);
+
+    proof_atomic_rmw_u8!(atomic_xsub_wrapper, check_atomic_xsub_relaxed, Relaxed, two_ty);
+    proof_atomic_rmw_u8!(atomic_xsub_wrapper, check_atomic_xsub_acquire, Acquire, two_ty);
+    proof_atomic_rmw_u8!(atomic_xsub_wrapper, check_atomic_xsub_release, Release, two_ty);
+    proof_atomic_rmw_u8!(atomic_xsub_wrapper, check_atomic_xsub_acqrel, AcqRel, two_ty);
+    proof_atomic_rmw_u8!(atomic_xsub_wrapper, check_atomic_xsub_seqcst, SeqCst, two_ty);
+
+    proof_atomic_rmw_u8!(atomic_and_wrapper, check_atomic_and_relaxed, Relaxed, two_ty);
+    proof_atomic_rmw_u8!(atomic_and_wrapper, check_atomic_and_acquire, Acquire, two_ty);
+    proof_atomic_rmw_u8!(atomic_and_wrapper, check_atomic_and_release, Release, two_ty);
+    proof_atomic_rmw_u8!(atomic_and_wrapper, check_atomic_and_acqrel, AcqRel, two_ty);
+    proof_atomic_rmw_u8!(atomic_and_wrapper, check_atomic_and_seqcst, SeqCst, two_ty);
+
+    proof_atomic_rmw_u8!(atomic_nand_wrapper, check_atomic_nand_relaxed, Relaxed, two_ty);
+    proof_atomic_rmw_u8!(atomic_nand_wrapper, check_atomic_nand_acquire, Acquire, two_ty);
+    proof_atomic_rmw_u8!(atomic_nand_wrapper, check_atomic_nand_release, Release, two_ty);
+    proof_atomic_rmw_u8!(atomic_nand_wrapper, check_atomic_nand_acqrel, AcqRel, two_ty);
+    proof_atomic_rmw_u8!(atomic_nand_wrapper, check_atomic_nand_seqcst, SeqCst, two_ty);
+
+    proof_atomic_rmw_u8!(atomic_or_wrapper, check_atomic_or_relaxed, Relaxed, two_ty);
+    proof_atomic_rmw_u8!(atomic_or_wrapper, check_atomic_or_acquire, Acquire, two_ty);
+    proof_atomic_rmw_u8!(atomic_or_wrapper, check_atomic_or_release, Release, two_ty);
+    proof_atomic_rmw_u8!(atomic_or_wrapper, check_atomic_or_acqrel, AcqRel, two_ty);
+    proof_atomic_rmw_u8!(atomic_or_wrapper, check_atomic_or_seqcst, SeqCst, two_ty);
+
+    proof_atomic_rmw_u8!(atomic_xor_wrapper, check_atomic_xor_relaxed, Relaxed, two_ty);
+    proof_atomic_rmw_u8!(atomic_xor_wrapper, check_atomic_xor_acquire, Acquire, two_ty);
+    proof_atomic_rmw_u8!(atomic_xor_wrapper, check_atomic_xor_release, Release, two_ty);
+    proof_atomic_rmw_u8!(atomic_xor_wrapper, check_atomic_xor_acqrel, AcqRel, two_ty);
+    proof_atomic_rmw_u8!(atomic_xor_wrapper, check_atomic_xor_seqcst, SeqCst, two_ty);
+
+    macro_rules! proof_atomic_minmax_ord {
+        ($wrapper:ident, $name:ident, $ty:ty, $ord:ident) => {
+            #[kani::proof_for_contract($wrapper)]
+            fn $name() {
+                let mut val: $ty = kani::any();
+                unsafe {
+                    let _ = $wrapper::<$ty, { AtomicOrdering::$ord }>(
+                        &mut val as *mut $ty,
+                        kani::any(),
+                    );
+                }
+            }
+        };
+    }
+
+    proof_atomic_minmax_ord!(atomic_max_wrapper, check_atomic_max_relaxed, i8, Relaxed);
+    proof_atomic_minmax_ord!(atomic_max_wrapper, check_atomic_max_acquire, i8, Acquire);
+    proof_atomic_minmax_ord!(atomic_max_wrapper, check_atomic_max_release, i8, Release);
+    proof_atomic_minmax_ord!(atomic_max_wrapper, check_atomic_max_acqrel, i8, AcqRel);
+    proof_atomic_minmax_ord!(atomic_max_wrapper, check_atomic_max_seqcst, i8, SeqCst);
+
+    proof_atomic_minmax_ord!(atomic_min_wrapper, check_atomic_min_relaxed, i8, Relaxed);
+    proof_atomic_minmax_ord!(atomic_min_wrapper, check_atomic_min_acquire, i8, Acquire);
+    proof_atomic_minmax_ord!(atomic_min_wrapper, check_atomic_min_release, i8, Release);
+    proof_atomic_minmax_ord!(atomic_min_wrapper, check_atomic_min_acqrel, i8, AcqRel);
+    proof_atomic_minmax_ord!(atomic_min_wrapper, check_atomic_min_seqcst, i8, SeqCst);
+
+    proof_atomic_minmax_ord!(atomic_umax_wrapper, check_atomic_umax_relaxed, u8, Relaxed);
+    proof_atomic_minmax_ord!(atomic_umax_wrapper, check_atomic_umax_acquire, u8, Acquire);
+    proof_atomic_minmax_ord!(atomic_umax_wrapper, check_atomic_umax_release, u8, Release);
+    proof_atomic_minmax_ord!(atomic_umax_wrapper, check_atomic_umax_acqrel, u8, AcqRel);
+    proof_atomic_minmax_ord!(atomic_umax_wrapper, check_atomic_umax_seqcst, u8, SeqCst);
+
+    proof_atomic_minmax_ord!(atomic_umin_wrapper, check_atomic_umin_relaxed, u8, Relaxed);
+    proof_atomic_minmax_ord!(atomic_umin_wrapper, check_atomic_umin_acquire, u8, Acquire);
+    proof_atomic_minmax_ord!(atomic_umin_wrapper, check_atomic_umin_release, u8, Release);
+    proof_atomic_minmax_ord!(atomic_umin_wrapper, check_atomic_umin_acqrel, u8, AcqRel);
+    proof_atomic_minmax_ord!(atomic_umin_wrapper, check_atomic_umin_seqcst, u8, SeqCst);
+
+    macro_rules! proof_atomic_cxchg_ord {
+        ($wrapper:ident, $name:ident, $succ:ident, $fail:ident) => {
+            #[kani::proof_for_contract($wrapper)]
+            fn $name() {
+                let mut val: u8 = kani::any();
+                unsafe {
+                    let _ = $wrapper::<u8, { AtomicOrdering::$succ }, { AtomicOrdering::$fail }>(
+                        &mut val as *mut u8,
+                        kani::any(),
+                        kani::any(),
+                    );
+                }
+            }
+        };
+    }
+
+    proof_atomic_cxchg_ord!(
+        atomic_cxchg_wrapper,
+        check_atomic_cxchg_relaxed_relaxed,
+        Relaxed,
+        Relaxed
+    );
+    proof_atomic_cxchg_ord!(
+        atomic_cxchg_wrapper,
+        check_atomic_cxchg_relaxed_acquire,
+        Relaxed,
+        Acquire
+    );
+    proof_atomic_cxchg_ord!(
+        atomic_cxchg_wrapper,
+        check_atomic_cxchg_relaxed_seqcst,
+        Relaxed,
+        SeqCst
+    );
+    proof_atomic_cxchg_ord!(
+        atomic_cxchg_wrapper,
+        check_atomic_cxchg_acquire_relaxed,
+        Acquire,
+        Relaxed
+    );
+    proof_atomic_cxchg_ord!(
+        atomic_cxchg_wrapper,
+        check_atomic_cxchg_acquire_acquire,
+        Acquire,
+        Acquire
+    );
+    proof_atomic_cxchg_ord!(
+        atomic_cxchg_wrapper,
+        check_atomic_cxchg_acquire_seqcst,
+        Acquire,
+        SeqCst
+    );
+    proof_atomic_cxchg_ord!(
+        atomic_cxchg_wrapper,
+        check_atomic_cxchg_release_relaxed,
+        Release,
+        Relaxed
+    );
+    proof_atomic_cxchg_ord!(
+        atomic_cxchg_wrapper,
+        check_atomic_cxchg_release_acquire,
+        Release,
+        Acquire
+    );
+    proof_atomic_cxchg_ord!(
+        atomic_cxchg_wrapper,
+        check_atomic_cxchg_release_seqcst,
+        Release,
+        SeqCst
+    );
+    proof_atomic_cxchg_ord!(
+        atomic_cxchg_wrapper,
+        check_atomic_cxchg_acqrel_relaxed,
+        AcqRel,
+        Relaxed
+    );
+    proof_atomic_cxchg_ord!(
+        atomic_cxchg_wrapper,
+        check_atomic_cxchg_acqrel_acquire,
+        AcqRel,
+        Acquire
+    );
+    proof_atomic_cxchg_ord!(atomic_cxchg_wrapper, check_atomic_cxchg_acqrel_seqcst, AcqRel, SeqCst);
+    proof_atomic_cxchg_ord!(
+        atomic_cxchg_wrapper,
+        check_atomic_cxchg_seqcst_relaxed,
+        SeqCst,
+        Relaxed
+    );
+    proof_atomic_cxchg_ord!(
+        atomic_cxchg_wrapper,
+        check_atomic_cxchg_seqcst_acquire,
+        SeqCst,
+        Acquire
+    );
+    proof_atomic_cxchg_ord!(atomic_cxchg_wrapper, check_atomic_cxchg_seqcst_seqcst, SeqCst, SeqCst);
+
+    proof_atomic_cxchg_ord!(
+        atomic_cxchgweak_wrapper,
+        check_atomic_cxchgweak_relaxed_relaxed,
+        Relaxed,
+        Relaxed
+    );
+    proof_atomic_cxchg_ord!(
+        atomic_cxchgweak_wrapper,
+        check_atomic_cxchgweak_relaxed_acquire,
+        Relaxed,
+        Acquire
+    );
+    proof_atomic_cxchg_ord!(
+        atomic_cxchgweak_wrapper,
+        check_atomic_cxchgweak_relaxed_seqcst,
+        Relaxed,
+        SeqCst
+    );
+    proof_atomic_cxchg_ord!(
+        atomic_cxchgweak_wrapper,
+        check_atomic_cxchgweak_acquire_relaxed,
+        Acquire,
+        Relaxed
+    );
+    proof_atomic_cxchg_ord!(
+        atomic_cxchgweak_wrapper,
+        check_atomic_cxchgweak_acquire_acquire,
+        Acquire,
+        Acquire
+    );
+    proof_atomic_cxchg_ord!(
+        atomic_cxchgweak_wrapper,
+        check_atomic_cxchgweak_acquire_seqcst,
+        Acquire,
+        SeqCst
+    );
+    proof_atomic_cxchg_ord!(
+        atomic_cxchgweak_wrapper,
+        check_atomic_cxchgweak_release_relaxed,
+        Release,
+        Relaxed
+    );
+    proof_atomic_cxchg_ord!(
+        atomic_cxchgweak_wrapper,
+        check_atomic_cxchgweak_release_acquire,
+        Release,
+        Acquire
+    );
+    proof_atomic_cxchg_ord!(
+        atomic_cxchgweak_wrapper,
+        check_atomic_cxchgweak_release_seqcst,
+        Release,
+        SeqCst
+    );
+    proof_atomic_cxchg_ord!(
+        atomic_cxchgweak_wrapper,
+        check_atomic_cxchgweak_acqrel_relaxed,
+        AcqRel,
+        Relaxed
+    );
+    proof_atomic_cxchg_ord!(
+        atomic_cxchgweak_wrapper,
+        check_atomic_cxchgweak_acqrel_acquire,
+        AcqRel,
+        Acquire
+    );
+    proof_atomic_cxchg_ord!(
+        atomic_cxchgweak_wrapper,
+        check_atomic_cxchgweak_acqrel_seqcst,
+        AcqRel,
+        SeqCst
+    );
+    proof_atomic_cxchg_ord!(
+        atomic_cxchgweak_wrapper,
+        check_atomic_cxchgweak_seqcst_relaxed,
+        SeqCst,
+        Relaxed
+    );
+    proof_atomic_cxchg_ord!(
+        atomic_cxchgweak_wrapper,
+        check_atomic_cxchgweak_seqcst_acquire,
+        SeqCst,
+        Acquire
+    );
+    proof_atomic_cxchg_ord!(
+        atomic_cxchgweak_wrapper,
+        check_atomic_cxchgweak_seqcst_seqcst,
+        SeqCst,
+        SeqCst
+    );
 }
diff --git a/library/core/src/sync/atomic.rs b/library/core/src/sync/atomic.rs
index 0c5552a0b81cc..70230dba847a9 100644
--- a/library/core/src/sync/atomic.rs
+++ b/library/core/src/sync/atomic.rs
@@ -242,10 +242,16 @@
 // are just normal values that get loaded/stored, but not dereferenced.
 #![allow(clippy::not_unsafe_ptr_arg_deref)]
 
+use safety::requires;
+
 use self::Ordering::*;
 use crate::cell::UnsafeCell;
 use crate::hint::spin_loop;
 use crate::intrinsics::AtomicOrdering as AO;
+#[cfg(kani)]
+use crate::kani;
+#[cfg(kani)]
+use crate::ub_checks;
 use crate::{fmt, intrinsics};
 
 trait Sealed {}
@@ -571,6 +577,9 @@ impl AtomicBool {
     #[inline]
     #[stable(feature = "atomic_from_ptr", since = "1.75.0")]
     #[rustc_const_stable(feature = "const_atomic_from_ptr", since = "1.84.0")]
+    // Cast to `AtomicBool` so the predicate uses this type's alignment (not `bool`'s).
+    #[requires(ub_checks::can_dereference(ptr as *const AtomicBool))]
+    #[requires(ub_checks::can_write(ptr as *mut AtomicBool))]
     pub const unsafe fn from_ptr<'a>(ptr: *mut bool) -> &'a AtomicBool {
         // SAFETY: guaranteed by the caller
         unsafe { &*ptr.cast() }
@@ -721,6 +730,7 @@ impl AtomicBool {
     #[inline]
     #[stable(feature = "rust1", since = "1.0.0")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+    #[requires(order == Relaxed || order == Acquire || order == SeqCst)]
     pub 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.
@@ -750,6 +760,8 @@ impl AtomicBool {
     #[stable(feature = "rust1", since = "1.0.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.v.get()))]
+    #[requires(order == Relaxed || order == Release || order == SeqCst)]
     pub 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.
@@ -913,6 +925,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]
+    #[cfg_attr(kani, kani::modifies(self.v.get()))]
+    #[requires(failure != Release && failure != AcqRel)]
     pub fn compare_exchange(
         &self,
         current: bool,
@@ -1009,6 +1023,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]
+    #[cfg_attr(kani, kani::modifies(self.v.get()))]
+    #[requires(failure != Release && failure != AcqRel)]
     pub fn compare_exchange_weak(
         &self,
         current: bool,
@@ -1543,6 +1559,9 @@ 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")]
+    // Cast to `AtomicPtr<T>` so the predicate uses this type's alignment.
+    #[requires(ub_checks::can_dereference(ptr as *const AtomicPtr<T>))]
+    #[requires(ub_checks::can_write(ptr as *mut AtomicPtr<T>))]
     pub const unsafe fn from_ptr<'a>(ptr: *mut *mut T) -> &'a AtomicPtr<T> {
         // SAFETY: guaranteed by the caller
         unsafe { &*ptr.cast() }
@@ -1720,6 +1739,7 @@ impl<T> AtomicPtr<T> {
     #[inline]
     #[stable(feature = "rust1", since = "1.0.0")]
     #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+    #[requires(order == Relaxed || order == Acquire || order == SeqCst)]
     pub fn load(&self, order: Ordering) -> *mut T {
         // SAFETY: data races are prevented by atomic intrinsics.
         unsafe { atomic_load(self.p.get(), order) }
@@ -1750,6 +1770,8 @@ impl<T> AtomicPtr<T> {
     #[stable(feature = "rust1", since = "1.0.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.p.get()))]
+    #[requires(order == Relaxed || order == Release || order == SeqCst)]
     pub fn store(&self, ptr: *mut T, order: Ordering) {
         // SAFETY: data races are prevented by atomic intrinsics.
         unsafe {
@@ -1902,6 +1924,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]
+    #[cfg_attr(kani, kani::modifies(self.p.get()))]
+    #[requires(failure != Release && failure != AcqRel)]
     pub fn compare_exchange(
         &self,
         current: *mut T,
@@ -1966,6 +1990,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]
+    #[cfg_attr(kani, kani::modifies(self.p.get()))]
+    #[requires(failure != Release && failure != AcqRel)]
     pub fn compare_exchange_weak(
         &self,
         current: *mut T,
@@ -2738,6 +2764,10 @@ 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")]
+            // Cast to `$atomic_type` so alignment matches the atomic, which can
+            // be stricter than `$int_type` on some targets.
+            #[requires(ub_checks::can_dereference(ptr as *const $atomic_type))]
+            #[requires(ub_checks::can_write(ptr as *mut $atomic_type))]
             pub const unsafe fn from_ptr<'a>(ptr: *mut $int_type) -> &'a $atomic_type {
                 // SAFETY: guaranteed by the caller
                 unsafe { &*ptr.cast() }
@@ -2915,6 +2945,7 @@ macro_rules! atomic_int {
             #[inline]
             #[$stable]
             #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+            #[requires(order == Relaxed || order == Acquire || order == SeqCst)]
             pub fn load(&self, order: Ordering) -> $int_type {
                 // SAFETY: data races are prevented by atomic intrinsics.
                 unsafe { atomic_load(self.v.get(), order) }
@@ -2943,6 +2974,8 @@ macro_rules! atomic_int {
             #[$stable]
             #[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.v.get()))]
+            #[requires(order == Relaxed || order == Release || order == SeqCst)]
             pub fn store(&self, val: $int_type, order: Ordering) {
                 // SAFETY: data races are prevented by atomic intrinsics.
                 unsafe { atomic_store(self.v.get(), val, order); }
@@ -3106,6 +3139,8 @@ macro_rules! atomic_int {
             #[$cfg_cas]
             #[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.v.get()))]
+            #[requires(failure != Release && failure != AcqRel)]
             pub fn compare_exchange(&self,
                                     current: $int_type,
                                     new: $int_type,
@@ -3170,6 +3205,8 @@ macro_rules! atomic_int {
             #[$cfg_cas]
             #[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.v.get()))]
+            #[requires(failure != Release && failure != AcqRel)]
             pub fn compare_exchange_weak(&self,
                                          current: $int_type,
                                          new: $int_type,
@@ -3985,6 +4022,9 @@ fn strongest_failure_ordering(order: Ordering) -> Ordering {
 
 #[inline]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+#[cfg_attr(kani, kani::modifies(dst))]
+#[requires(ub_checks::can_write(dst))]
+#[requires(order == Relaxed || order == Release || order == SeqCst)]
 unsafe fn atomic_store<T: Copy>(dst: *mut T, val: T, order: Ordering) {
     // SAFETY: the caller must uphold the safety contract for `atomic_store`.
     unsafe {
@@ -4000,6 +4040,8 @@ unsafe fn atomic_store<T: Copy>(dst: *mut T, val: T, order: Ordering) {
 
 #[inline]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+#[requires(ub_checks::can_dereference(dst))]
+#[requires(order == Relaxed || order == Acquire || order == SeqCst)]
 unsafe fn atomic_load<T: Copy>(dst: *const T, order: Ordering) -> T {
     // SAFETY: the caller must uphold the safety contract for `atomic_load`.
     unsafe {
@@ -4016,6 +4058,9 @@ unsafe fn atomic_load<T: Copy>(dst: *const T, order: Ordering) -> T {
 #[inline]
 #[cfg(target_has_atomic)]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+#[cfg_attr(kani, kani::modifies(dst))]
+#[requires(ub_checks::can_dereference(dst as *const T))]
+#[requires(ub_checks::can_write(dst))]
 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 {
@@ -4033,6 +4078,9 @@ unsafe fn atomic_swap<T: Copy>(dst: *mut T, val: T, order: Ordering) -> T {
 #[inline]
 #[cfg(target_has_atomic)]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+#[cfg_attr(kani, kani::modifies(dst))]
+#[requires(ub_checks::can_dereference(dst as *const T))]
+#[requires(ub_checks::can_write(dst))]
 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 {
@@ -4050,6 +4098,9 @@ unsafe fn atomic_add<T: Copy, U: Copy>(dst: *mut T, val: U, order: Ordering) ->
 #[inline]
 #[cfg(target_has_atomic)]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+#[cfg_attr(kani, kani::modifies(dst))]
+#[requires(ub_checks::can_dereference(dst as *const T))]
+#[requires(ub_checks::can_write(dst))]
 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 {
@@ -4069,6 +4120,10 @@ unsafe fn atomic_sub<T: Copy, U: Copy>(dst: *mut T, val: U, order: Ordering) ->
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
 #[unstable(feature = "core_intrinsics", issue = "none")]
 #[doc(hidden)]
+#[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)]
 pub unsafe fn atomic_compare_exchange<T: Copy>(
     dst: *mut T,
     old: T,
@@ -4134,6 +4189,10 @@ pub unsafe fn atomic_compare_exchange<T: Copy>(
 #[inline]
 #[cfg(target_has_atomic)]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+#[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)]
 unsafe fn atomic_compare_exchange_weak<T: Copy>(
     dst: *mut T,
     old: T,
@@ -4199,6 +4258,9 @@ unsafe fn atomic_compare_exchange_weak<T: Copy>(
 #[inline]
 #[cfg(target_has_atomic)]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+#[cfg_attr(kani, kani::modifies(dst))]
+#[requires(ub_checks::can_dereference(dst as *const T))]
+#[requires(ub_checks::can_write(dst))]
 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 {
@@ -4215,6 +4277,9 @@ unsafe fn atomic_and<T: Copy, U: Copy>(dst: *mut T, val: U, order: Ordering) ->
 #[inline]
 #[cfg(target_has_atomic)]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+#[cfg_attr(kani, kani::modifies(dst))]
+#[requires(ub_checks::can_dereference(dst as *const T))]
+#[requires(ub_checks::can_write(dst))]
 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 {
@@ -4231,6 +4296,9 @@ unsafe fn atomic_nand<T: Copy, U: Copy>(dst: *mut T, val: U, order: Ordering) ->
 #[inline]
 #[cfg(target_has_atomic)]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+#[cfg_attr(kani, kani::modifies(dst))]
+#[requires(ub_checks::can_dereference(dst as *const T))]
+#[requires(ub_checks::can_write(dst))]
 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 {
@@ -4247,6 +4315,9 @@ unsafe fn atomic_or<T: Copy, U: Copy>(dst: *mut T, val: U, order: Ordering) -> T
 #[inline]
 #[cfg(target_has_atomic)]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+#[cfg_attr(kani, kani::modifies(dst))]
+#[requires(ub_checks::can_dereference(dst as *const T))]
+#[requires(ub_checks::can_write(dst))]
 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 {
@@ -4264,6 +4335,9 @@ unsafe fn atomic_xor<T: Copy, U: Copy>(dst: *mut T, val: U, order: Ordering) ->
 #[inline]
 #[cfg(target_has_atomic)]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+#[cfg_attr(kani, kani::modifies(dst))]
+#[requires(ub_checks::can_dereference(dst as *const T))]
+#[requires(ub_checks::can_write(dst))]
 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 {
@@ -4281,6 +4355,9 @@ unsafe fn atomic_max<T: Copy>(dst: *mut T, val: T, order: Ordering) -> T {
 #[inline]
 #[cfg(target_has_atomic)]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+#[cfg_attr(kani, kani::modifies(dst))]
+#[requires(ub_checks::can_dereference(dst as *const T))]
+#[requires(ub_checks::can_write(dst))]
 unsafe fn atomic_min<T: Copy>(dst: *mut T, val: T, order: Ordering) -> T {
     // SAFETY: the caller must uphold the safety contract for `atomic_min`
     unsafe {
@@ -4298,6 +4375,9 @@ unsafe fn atomic_min<T: Copy>(dst: *mut T, val: T, order: Ordering) -> T {
 #[inline]
 #[cfg(target_has_atomic)]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+#[cfg_attr(kani, kani::modifies(dst))]
+#[requires(ub_checks::can_dereference(dst as *const T))]
+#[requires(ub_checks::can_write(dst))]
 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 {
@@ -4315,6 +4395,9 @@ unsafe fn atomic_umax<T: Copy>(dst: *mut T, val: T, order: Ordering) -> T {
 #[inline]
 #[cfg(target_has_atomic)]
 #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces
+#[cfg_attr(kani, kani::modifies(dst))]
+#[requires(ub_checks::can_dereference(dst as *const T))]
+#[requires(ub_checks::can_write(dst))]
 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 {
@@ -4609,3 +4692,302 @@ 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::*;
+    use crate::kani;
+
+    impl kani::Arbitrary for Ordering {
+        fn any() -> Self {
+            match kani::any::<u8>() {
+                0 => Relaxed,
+                1 => Release,
+                2 => Acquire,
+                3 => AcqRel,
+                _ => SeqCst,
+            }
+        }
+    }
+
+    /// Pointer into `buf` at a nondeterministic byte offset.
+    ///
+    /// The offset may be misaligned for `T` or too close to the end of `buf` to
+    /// hold a `T`. `proof_for_contract` assumes the callee's `requires`, so only
+    /// pointers that satisfy alignment and validity are executed.
+    fn ptr_at_offset<T>(buf: &mut [u8; 64]) -> *mut T {
+        let offset = kani::any_where(|o: &usize| *o < 64);
+        buf.as_mut_ptr().wrapping_add(offset).cast::<T>()
+    }
+
+    // Write proofs use a live stack object. `wrapping_add` pointers lose
+    // provenance, so CBMC's assignable check fails even when `can_write` is
+    // assumed. `proof_for_contract` still assumes the callee's `requires`.
+
+    // --- Part 1: `from_ptr` ---
+
+    #[kani::proof_for_contract(AtomicBool::from_ptr)]
+    fn check_atomic_bool_from_ptr() {
+        let mut buf: [bool; 16] = kani::any();
+        let offset = kani::any_where(|o: &usize| *o < 16);
+        let ptr = buf.as_mut_ptr().wrapping_add(offset);
+        unsafe {
+            let _ = AtomicBool::from_ptr(ptr);
+        }
+    }
+
+    macro_rules! from_ptr_proof {
+        ($name:ident, $atomic:ty, $int:ty) => {
+            #[kani::proof_for_contract(<$atomic>::from_ptr)]
+            fn $name() {
+                let mut buf: [u8; 64] = kani::any();
+                let ptr = ptr_at_offset::<$int>(&mut buf);
+                unsafe {
+                    let _ = <$atomic>::from_ptr(ptr);
+                }
+            }
+        };
+    }
+
+    #[cfg(target_has_atomic_load_store = "8")]
+    from_ptr_proof!(check_atomic_i8_from_ptr, AtomicI8, i8);
+    #[cfg(target_has_atomic_load_store = "8")]
+    from_ptr_proof!(check_atomic_u8_from_ptr, AtomicU8, u8);
+    #[cfg(target_has_atomic_load_store = "16")]
+    from_ptr_proof!(check_atomic_i16_from_ptr, AtomicI16, i16);
+    #[cfg(target_has_atomic_load_store = "16")]
+    from_ptr_proof!(check_atomic_u16_from_ptr, AtomicU16, u16);
+    #[cfg(target_has_atomic_load_store = "32")]
+    from_ptr_proof!(check_atomic_i32_from_ptr, AtomicI32, i32);
+    #[cfg(target_has_atomic_load_store = "32")]
+    from_ptr_proof!(check_atomic_u32_from_ptr, AtomicU32, u32);
+    #[cfg(target_has_atomic_load_store = "64")]
+    from_ptr_proof!(check_atomic_i64_from_ptr, AtomicI64, i64);
+    #[cfg(target_has_atomic_load_store = "64")]
+    from_ptr_proof!(check_atomic_u64_from_ptr, AtomicU64, u64);
+    #[cfg(target_has_atomic_load_store = "128")]
+    from_ptr_proof!(check_atomic_i128_from_ptr, AtomicI128, i128);
+    #[cfg(target_has_atomic_load_store = "128")]
+    from_ptr_proof!(check_atomic_u128_from_ptr, AtomicU128, u128);
+    #[cfg(target_has_atomic_load_store = "ptr")]
+    from_ptr_proof!(check_atomic_isize_from_ptr, AtomicIsize, isize);
+    #[cfg(target_has_atomic_load_store = "ptr")]
+    from_ptr_proof!(check_atomic_usize_from_ptr, AtomicUsize, usize);
+
+    // `AtomicPtr<T>`: T sizes 0, 1, 2, 4, and a non-power-of-two (3).
+    macro_rules! atomic_ptr_from_ptr_proof {
+        ($name:ident, $t:ty) => {
+            #[cfg(target_has_atomic_load_store = "ptr")]
+            #[kani::proof_for_contract(AtomicPtr::<$t>::from_ptr)]
+            fn $name() {
+                let mut buf: [u8; 64] = kani::any();
+                let ptr = ptr_at_offset::<*mut $t>(&mut buf);
+                unsafe {
+                    let _ = AtomicPtr::<$t>::from_ptr(ptr);
+                }
+            }
+        };
+    }
+
+    atomic_ptr_from_ptr_proof!(check_atomic_ptr_from_ptr_zst, ());
+    atomic_ptr_from_ptr_proof!(check_atomic_ptr_from_ptr_u8, u8);
+    atomic_ptr_from_ptr_proof!(check_atomic_ptr_from_ptr_u16, u16);
+    atomic_ptr_from_ptr_proof!(check_atomic_ptr_from_ptr_u32, u32);
+    atomic_ptr_from_ptr_proof!(check_atomic_ptr_from_ptr_odd, [u8; 3]);
+
+    // --- Part 2: unsafe helpers ---
+
+    #[kani::proof_for_contract(atomic_store)]
+    fn check_atomic_store_u8() {
+        let mut val: u8 = kani::any();
+        unsafe {
+            atomic_store(&mut val as *mut u8, kani::any(), kani::any());
+        }
+    }
+
+    #[kani::proof_for_contract(atomic_store)]
+    fn check_atomic_store_i32() {
+        let mut val: i32 = kani::any();
+        unsafe {
+            atomic_store(&mut val as *mut i32, kani::any(), kani::any());
+        }
+    }
+
+    #[kani::proof_for_contract(atomic_load)]
+    fn check_atomic_load_u8() {
+        let val: u8 = kani::any();
+        unsafe {
+            let _ = atomic_load(&val as *const u8, kani::any());
+        }
+    }
+
+    #[kani::proof_for_contract(atomic_load)]
+    fn check_atomic_load_i32() {
+        let val: i32 = kani::any();
+        unsafe {
+            let _ = atomic_load(&val as *const i32, kani::any());
+        }
+    }
+
+    macro_rules! rmw_proof {
+        ($contract:ident, $name:ident, $ty:ty) => {
+            #[cfg(target_has_atomic)]
+            #[kani::proof_for_contract($contract)]
+            fn $name() {
+                let mut val: $ty = kani::any();
+                unsafe {
+                    let _ = $contract::<$ty>(&mut val as *mut $ty, kani::any::<$ty>(), kani::any());
+                }
+            }
+        };
+        ($contract:ident, $name:ident, $ty:ty, $u:ty) => {
+            #[cfg(target_has_atomic)]
+            #[kani::proof_for_contract($contract)]
+            fn $name() {
+                let mut val: $ty = kani::any();
+                unsafe {
+                    let _ =
+                        $contract::<$ty, $u>(&mut val as *mut $ty, kani::any::<$u>(), kani::any());
+                }
+            }
+        };
+    }
+
+    rmw_proof!(atomic_swap, check_atomic_swap_u8, u8);
+    rmw_proof!(atomic_swap, check_atomic_swap_i32, i32);
+    rmw_proof!(atomic_add, check_atomic_add_u8, u8, u8);
+    rmw_proof!(atomic_add, check_atomic_add_i32, i32, i32);
+    rmw_proof!(atomic_sub, check_atomic_sub_u8, u8, u8);
+    rmw_proof!(atomic_sub, check_atomic_sub_i32, i32, i32);
+    rmw_proof!(atomic_and, check_atomic_and_u8, u8, u8);
+    rmw_proof!(atomic_nand, check_atomic_nand_u8, u8, u8);
+    rmw_proof!(atomic_or, check_atomic_or_u8, u8, u8);
+    rmw_proof!(atomic_xor, check_atomic_xor_u8, u8, u8);
+    rmw_proof!(atomic_max, check_atomic_max_i8, i8);
+    rmw_proof!(atomic_max, check_atomic_max_i32, i32);
+    rmw_proof!(atomic_min, check_atomic_min_i8, i8);
+    rmw_proof!(atomic_umax, check_atomic_umax_u8, u8);
+    rmw_proof!(atomic_umin, check_atomic_umin_u8, u8);
+
+    #[cfg(target_has_atomic)]
+    #[kani::proof_for_contract(atomic_compare_exchange)]
+    fn check_atomic_compare_exchange_u8() {
+        let mut val: u8 = kani::any();
+        unsafe {
+            let _ = atomic_compare_exchange(
+                &mut val as *mut u8,
+                kani::any(),
+                kani::any(),
+                kani::any(),
+                kani::any(),
+            );
+        }
+    }
+
+    #[cfg(target_has_atomic)]
+    #[kani::proof_for_contract(atomic_compare_exchange_weak)]
+    fn check_atomic_compare_exchange_weak_u8() {
+        let mut val: u8 = kani::any();
+        unsafe {
+            let _ = atomic_compare_exchange_weak(
+                &mut val as *mut u8,
+                kani::any(),
+                kani::any(),
+                kani::any(),
+                kani::any(),
+            );
+        }
+    }
+
+    #[cfg(target_has_atomic)]
+    #[kani::proof_for_contract(atomic_add)]
+    fn check_atomic_add_ptr() {
+        let mut val = kani::any::<usize>() as *mut u8;
+        unsafe {
+            let _ = atomic_add::<*mut u8, usize>(
+                &mut val as *mut *mut u8,
+                kani::any::<usize>(),
+                kani::any(),
+            );
+        }
+    }
+
+    // --- Optional: panic-ordering contracts on safe methods ---
+
+    #[kani::proof_for_contract(AtomicBool::store)]
+    fn check_atomic_bool_store() {
+        let atomic = AtomicBool::new(kani::any());
+        atomic.store(kani::any(), kani::any());
+    }
+
+    #[kani::proof_for_contract(AtomicBool::load)]
+    fn check_atomic_bool_load() {
+        let atomic = AtomicBool::new(kani::any());
+        let _ = atomic.load(kani::any());
+    }
+
+    #[cfg(target_has_atomic = "8")]
+    #[kani::proof_for_contract(AtomicBool::compare_exchange)]
+    fn check_atomic_bool_compare_exchange() {
+        let atomic = AtomicBool::new(kani::any());
+        let _ = atomic.compare_exchange(kani::any(), kani::any(), kani::any(), kani::any());
+    }
+
+    #[cfg(target_has_atomic_load_store = "32")]
+    #[kani::proof_for_contract(AtomicI32::store)]
+    fn check_atomic_i32_store() {
+        let atomic = AtomicI32::new(kani::any());
+        atomic.store(kani::any(), kani::any());
+    }
+
+    #[cfg(target_has_atomic_load_store = "32")]
+    #[kani::proof_for_contract(AtomicI32::load)]
+    fn check_atomic_i32_load() {
+        let atomic = AtomicI32::new(kani::any());
+        let _ = atomic.load(kani::any());
+    }
+
+    #[cfg(all(target_has_atomic_load_store = "32", target_has_atomic = "32"))]
+    #[kani::proof_for_contract(AtomicI32::compare_exchange)]
+    fn check_atomic_i32_compare_exchange() {
+        let atomic = AtomicI32::new(kani::any());
+        let _ = atomic.compare_exchange(kani::any(), kani::any(), kani::any(), kani::any());
+    }
+
+    #[cfg(target_has_atomic_load_store = "ptr")]
+    #[kani::proof_for_contract(AtomicPtr::<u8>::store)]
+    fn check_atomic_ptr_store() {
+        let atomic = AtomicPtr::<u8>::new(kani::any::<usize>() as *mut u8);
+        atomic.store(kani::any::<usize>() as *mut u8, kani::any());
+    }
+
+    #[cfg(target_has_atomic_load_store = "ptr")]
+    #[kani::proof_for_contract(AtomicPtr::<u8>::load)]
+    fn check_atomic_ptr_load() {
+        let atomic = AtomicPtr::<u8>::new(kani::any::<usize>() as *mut u8);
+        let _ = atomic.load(kani::any());
+    }
+
+    #[kani::proof]
+    #[kani::should_panic]
+    fn atomic_bool_store_panics_on_acquire() {
+        let atomic = AtomicBool::new(false);
+        atomic.store(true, Acquire);
+    }
+
+    #[kani::proof]
+    #[kani::should_panic]
+    fn atomic_bool_load_panics_on_release() {
+        let atomic = AtomicBool::new(false);
+        let _ = atomic.load(Release);
+    }
+
+    #[cfg(target_has_atomic = "8")]
+    #[kani::proof]
+    #[kani::should_panic]
+    fn atomic_bool_compare_exchange_panics_on_release_failure() {
+        let atomic = AtomicBool::new(false);
+        let _ = atomic.compare_exchange(false, true, Relaxed, Release);
+    }
+}