diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs
index 0aa306f803a70..b805c8e3b55ac 100644
--- a/library/core/src/ptr/non_null.rs
+++ b/library/core/src/ptr/non_null.rs
@@ -294,6 +294,7 @@ impl<T: ?Sized> NonNull<T> {
     #[must_use]
     #[inline]
     #[stable(feature = "strict_provenance", since = "CURRENT_RUSTC_VERSION")]
+    #[ensures(|result| result.get() == self.as_ptr() as *const() as usize)]
     pub fn addr(self) -> NonZero<usize> {
         // SAFETY: The pointer is guaranteed by the type to be non-null,
         // meaning that the address will be non-zero.
@@ -567,6 +568,11 @@ impl<T: ?Sized> NonNull<T> {
     #[must_use = "returns a new pointer rather than modifying its argument"]
     #[stable(feature = "non_null_convenience", since = "1.80.0")]
     #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")]
+    #[requires(count.checked_mul(core::mem::size_of::<T>()).is_some() 
+        && count * core::mem::size_of::<T>() <= isize::MAX as usize
+        && (self.pointer as isize).checked_add(count as isize * core::mem::size_of::<T>() as isize).is_some() // check wrapping add
+        && kani::mem::same_allocation(self.pointer, self.pointer.wrapping_offset(count as isize)))]
+    #[ensures(|result: &NonNull<T>| result.as_ptr() == self.as_ptr().offset(count as isize))]
     pub const unsafe fn add(self, count: usize) -> Self
     where
         T: Sized,
@@ -1208,6 +1214,36 @@ impl<T: ?Sized> NonNull<T> {
     #[must_use]
     #[stable(feature = "non_null_convenience", since = "1.80.0")]
     #[rustc_const_unstable(feature = "const_align_offset", issue = "90962")]
+    #[ensures(|result| {
+        // Post-condition reference: https://github.com/model-checking/verify-rust-std/pull/69/files
+        let stride = crate::mem::size_of::<T>();
+        // ZSTs
+        if stride == 0 {
+            if self.pointer.addr() % align == 0 { 
+                return *result == 0;
+            } else { 
+                return *result == usize::MAX;
+            }
+        }
+        // In this case, the pointer cannot be aligned
+        if (align % stride == 0) && (self.pointer.addr() % stride != 0) {
+            return *result == usize::MAX;
+        }
+        // Checking if the answer should indeed be usize::MAX when align % stride != 0
+        // requires computing gcd(a, stride), which is too expensive without
+        // quantifiers (https://model-checking.github.io/kani/rfc/rfcs/0010-quantifiers.html).
+        // This should be updated once quantifiers are available.
+        if (align % stride != 0 && *result == usize::MAX) { 
+            return true; 
+        }
+        // If we reach this case, either:
+        //  - align % stride == 0 and self.pointer.addr() % stride == 0, so it is definitely possible to align the pointer
+        //  - align % stride != 0 and result != usize::MAX, so align_offset is claiming that it's possible to align the pointer
+        // Check that applying the returned result does indeed produce an aligned address
+        let product = usize::wrapping_mul(*result, stride);
+        let new_addr = usize::wrapping_add(product, self.pointer.addr());
+        *result != usize::MAX && new_addr % align == 0
+    })]
     pub const fn align_offset(self, align: usize) -> usize
     where
         T: Sized,
@@ -1811,6 +1847,7 @@ impl<T: ?Sized> From<&T> for NonNull<T> {
 mod verify {
     use super::*;
     use crate::ptr::null_mut;
+    use kani::PointerGenerator;
 
     // pub const unsafe fn new_unchecked(ptr: *mut T) -> Self
     #[kani::proof_for_contract(NonNull::new_unchecked)]
@@ -1821,7 +1858,7 @@ mod verify {
         }
     }
 
-    // pub const unsafe fn new(ptr: *mut T) -> Option<Self>
+    // pub const fn new(ptr: *mut T) -> Option<Self>
     #[kani::proof_for_contract(NonNull::new)]
     pub fn non_null_check_new() {
         let mut x: i32 = kani::any();
@@ -1829,4 +1866,56 @@ mod verify {
         let maybe_null_ptr =  if kani::any() { xptr as *mut i32 } else { null_mut() };
         let _ = NonNull::new(maybe_null_ptr);
     }
+
+    // pub const unsafe fn add(self, count: usize) -> Self
+    #[kani::proof_for_contract(NonNull::add)]
+    pub fn non_null_check_add() {
+        const SIZE: usize = 100000;
+        let mut generator = PointerGenerator::<100000>::new();
+        let raw_ptr: *mut i8 = generator.any_in_bounds().ptr;
+        let ptr = unsafe { NonNull::new(raw_ptr).unwrap()};
+        // Create a non-deterministic count value
+        let count: usize = kani::any();  
+        
+        unsafe {
+            let result = ptr.add(count);
+        }
+    }
+
+    // pub fn addr(self) -> NonZero<usize>
+    #[kani::proof_for_contract(NonNull::addr)]
+    pub fn non_null_check_addr() {  
+        // Create NonNull pointer & get pointer address
+        let x = kani::any::<usize>() as *mut i32;
+        let Some(nonnull_xptr) = NonNull::new(x) else { return; };
+        let address = nonnull_xptr.addr();
+    }
+
+    // pub fn align_offset(self, align: usize) -> usize
+    #[kani::proof_for_contract(NonNull::align_offset)]
+    pub fn non_null_check_align_offset() {
+        // Create NonNull pointer
+        let x = kani::any::<usize>() as *mut i32;
+        let Some(nonnull_xptr) = NonNull::new(x) else { return; };
+    
+        // Call align_offset with valid align value
+        let align: usize = kani::any();
+        kani::assume(align.is_power_of_two());
+        nonnull_xptr.align_offset(align);
+    }
+
+    // pub fn align_offset(self, align: usize) -> usize
+    #[kani::should_panic]
+    #[kani::proof_for_contract(NonNull::align_offset)]
+    pub fn non_null_check_align_offset_negative() {
+        // Create NonNull pointer
+        let x = kani::any::<usize>() as *mut i8;
+        let Some(nonnull_xptr) = NonNull::new(x) else { return; };
+
+        // Generate align value that is not necessarily a power of two
+        let invalid_align: usize = kani::any();
+    
+        // Trigger panic
+        let offset = nonnull_xptr.align_offset(invalid_align);
+    }
 }