diff --git a/library/core/src/ptr/alignment.rs b/library/core/src/ptr/alignment.rs
index e5f5bf6a50313..d51f2ef7edff3 100644
--- a/library/core/src/ptr/alignment.rs
+++ b/library/core/src/ptr/alignment.rs
@@ -1,4 +1,4 @@
-use safety::requires;
+use safety::{ensures, requires};
 use crate::num::NonZero;
 #[cfg(debug_assertions)]
 use crate::ub_checks::assert_unsafe_precondition;
@@ -48,6 +48,8 @@ impl Alignment {
     #[unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[inline]
+    #[requires(mem::align_of::<T>().is_power_of_two())]
+    #[ensures(|result| result.as_usize().is_power_of_two())]
     pub const fn of<T>() -> Self {
         // SAFETY: rustc ensures that type alignment is always a power of two.
         unsafe { Alignment::new_unchecked(mem::align_of::<T>()) }
@@ -60,6 +62,8 @@ impl Alignment {
     #[unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[inline]
+    #[ensures(|result| align.is_power_of_two() == result.is_some())]
+    #[ensures(|result| result.is_none() || result.unwrap().as_usize() == align)]
     pub const fn new(align: usize) -> Option<Self> {
         if align.is_power_of_two() {
             // SAFETY: Just checked it only has one bit set
@@ -80,8 +84,9 @@ impl Alignment {
     #[unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[inline]
-    #[requires(align > 0)]
-    #[requires((align & (align - 1)) == 0)]
+    #[requires(align > 0 && (align & (align - 1)) == 0)]
+    #[ensures(|result| result.as_usize() == align)]
+    #[ensures(|result| result.as_usize().is_power_of_two())]
     pub const unsafe fn new_unchecked(align: usize) -> Self {
         #[cfg(debug_assertions)]
         assert_unsafe_precondition!(
@@ -99,6 +104,7 @@ impl Alignment {
     #[unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[inline]
+    #[ensures(|result| result.is_power_of_two())]
     pub const fn as_usize(self) -> usize {
         self.0 as usize
     }
@@ -107,6 +113,8 @@ impl Alignment {
     #[unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[inline]
+    #[ensures(|result| result.get().is_power_of_two())]
+    #[ensures(|result| result.get() == self.as_usize())]
     pub const fn as_nonzero(self) -> NonZero<usize> {
         // SAFETY: All the discriminants are non-zero.
         unsafe { NonZero::new_unchecked(self.as_usize()) }
@@ -128,6 +136,9 @@ impl Alignment {
     #[unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[inline]
+    #[requires(self.as_usize().is_power_of_two())]
+    #[ensures(|result| (*result as usize) < mem::size_of::<usize>() * 8)]
+    #[ensures(|result| 1usize << *result == self.as_usize())]
     pub const fn log2(self) -> u32 {
         self.as_nonzero().trailing_zeros()
     }
@@ -158,6 +169,9 @@ impl Alignment {
     #[unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[rustc_const_unstable(feature = "ptr_alignment_type", issue = "102070")]
     #[inline]
+    #[ensures(|result| *result > 0)]
+    #[ensures(|result| *result == !(self.as_usize() -1))]
+    #[ensures(|result| self.as_usize() & *result == self.as_usize())]
     pub const fn mask(self) -> usize {
         // SAFETY: The alignment is always nonzero, and therefore decrementing won't overflow.
         !(unsafe { self.as_usize().unchecked_sub(1) })
@@ -370,3 +384,68 @@ enum AlignmentEnum {
     _Align1Shl62 = 1 << 62,
     _Align1Shl63 = 1 << 63,
 }
+
+#[cfg(kani)]
+#[unstable(feature="kani", issue="none")]
+mod verify {
+    use super::*;
+
+    impl kani::Arbitrary for Alignment {
+        fn any() -> Self {
+            let align = kani::any_where(|a: &usize| a.is_power_of_two());
+            unsafe { mem::transmute::<usize, Alignment>(align) }
+        }
+    }
+
+    // pub const fn of<T>() -> Self
+    #[kani::proof_for_contract(Alignment::of)]
+    pub fn check_of_i32() {
+        let _ = Alignment::of::<i32>();
+    }
+
+    // pub const fn new(align: usize) -> Option<Self>
+    #[kani::proof_for_contract(Alignment::new)]
+    pub fn check_new() {
+        let a = kani::any::<usize>();
+        let _ = Alignment::new(a);
+    }
+
+    // pub const unsafe fn new_unchecked(align: usize) -> Self
+    #[kani::proof_for_contract(Alignment::new_unchecked)]
+    pub fn check_new_unchecked() {
+        let a = kani::any::<usize>();
+        unsafe {
+            let _ = Alignment::new_unchecked(a);
+        }
+    }
+
+    // pub const fn as_usize(self) -> usize
+    #[kani::proof_for_contract(Alignment::as_usize)]
+    pub fn check_as_usize() {
+        let a = kani::any::<usize>();
+        if let Some(alignment) = Alignment::new(a) {
+            assert_eq!(alignment.as_usize(), a);
+        }
+    }
+
+    // pub const fn as_nonzero(self) -> NonZero<usize>
+    #[kani::proof_for_contract(Alignment::as_nonzero)]
+    pub fn check_as_nonzero() {
+        let alignment = kani::any::<Alignment>();
+        let _ = alignment.as_nonzero();
+    }
+
+    // pub const fn log2(self) -> u32
+    #[kani::proof_for_contract(Alignment::log2)]
+    pub fn check_log2() {
+        let alignment = kani::any::<Alignment>();
+        let _ = alignment.log2();
+    }
+
+    // pub const fn mask(self) -> usize
+    #[kani::proof_for_contract(Alignment::mask)]
+    pub fn check_mask() {
+        let alignment = kani::any::<Alignment>();
+        let _ = alignment.mask();
+    }
+}