diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml
index fd949f8eef552..0c68593f003fb 100644
--- a/.github/workflows/kani.yml
+++ b/.github/workflows/kani.yml
@@ -81,6 +81,7 @@ jobs:
       - name: Run Kani Verification
         run: |
           scripts/run-kani.sh --run autoharness --kani-args \
+            --include-pattern alloc::__default_lib_allocator:: \
             --include-pattern alloc::layout::Layout::from_size_align \
             --include-pattern ascii::ascii_char::AsciiChar::from_u8 \
             --include-pattern char::convert::from_u32_unchecked \
diff --git a/library/std/src/alloc.rs b/library/std/src/alloc.rs
index 75971ac90e783..1240416fd1da2 100644
--- a/library/std/src/alloc.rs
+++ b/library/std/src/alloc.rs
@@ -56,6 +56,8 @@
 #![deny(unsafe_op_in_unsafe_fn)]
 #![stable(feature = "alloc_module", since = "1.28.0")]
 
+#[cfg(kani)]
+use core::kani;
 use core::ptr::NonNull;
 use core::sync::atomic::{AtomicPtr, Ordering};
 use core::{hint, mem, ptr};
@@ -63,6 +65,7 @@ use core::{hint, mem, ptr};
 #[stable(feature = "alloc_module", since = "1.28.0")]
 #[doc(inline)]
 pub use alloc_crate::alloc::*;
+use safety::requires;
 
 /// The default memory allocator provided by the operating system.
 ///
@@ -150,6 +153,10 @@ impl System {
     }
 
     // SAFETY: Same as `Allocator::grow`
+    #[requires(new_layout.size() >= old_layout.size())]
+    #[requires(ptr.as_ptr().is_aligned_to(old_layout.align()))]
+    #[requires(old_layout.size() == 0 || old_layout.align() != 0)]
+    #[requires(new_layout.size() == 0 || new_layout.align() != 0)]
     #[inline]
     unsafe fn grow_impl(
         &self,
@@ -212,6 +219,7 @@ unsafe impl Allocator for System {
         self.alloc_impl(layout, true)
     }
 
+    #[requires(layout.size() != 0)]
     #[inline]
     unsafe fn deallocate(&self, ptr: NonNull<u8>, layout: Layout) {
         if layout.size() != 0 {
@@ -221,6 +229,7 @@ unsafe impl Allocator for System {
         }
     }
 
+    #[requires(new_layout.size() >= old_layout.size())]
     #[inline]
     unsafe fn grow(
         &self,
@@ -232,6 +241,7 @@ unsafe impl Allocator for System {
         unsafe { self.grow_impl(ptr, old_layout, new_layout, false) }
     }
 
+    #[requires(new_layout.size() >= old_layout.size())]
     #[inline]
     unsafe fn grow_zeroed(
         &self,
@@ -243,6 +253,7 @@ unsafe impl Allocator for System {
         unsafe { self.grow_impl(ptr, old_layout, new_layout, true) }
     }
 
+    #[requires(new_layout.size() <= old_layout.size())]
     #[inline]
     unsafe fn shrink(
         &self,
@@ -382,6 +393,11 @@ pub fn rust_oom(layout: Layout) -> ! {
 #[allow(unused_attributes)]
 #[unstable(feature = "alloc_internals", issue = "none")]
 pub mod __default_lib_allocator {
+    #[cfg(kani)]
+    use core::kani;
+
+    use safety::requires;
+
     use super::{GlobalAlloc, Layout, System};
     // These magic symbol names are used as a fallback for implementing the
     // `__rust_alloc` etc symbols (see `src/liballoc/alloc.rs`) when there is
@@ -393,6 +409,7 @@ pub mod __default_lib_allocator {
     // linkage directives are provided as part of the current compiler allocator
     // ABI
 
+    #[requires(align.is_power_of_two())]
     #[rustc_std_internal_symbol]
     pub unsafe extern "C" fn __rdl_alloc(size: usize, align: usize) -> *mut u8 {
         // SAFETY: see the guarantees expected by `Layout::from_size_align` and
@@ -403,6 +420,7 @@ pub mod __default_lib_allocator {
         }
     }
 
+    #[requires(align.is_power_of_two())]
     #[rustc_std_internal_symbol]
     pub unsafe extern "C" fn __rdl_dealloc(ptr: *mut u8, size: usize, align: usize) {
         // SAFETY: see the guarantees expected by `Layout::from_size_align` and
@@ -410,6 +428,7 @@ pub mod __default_lib_allocator {
         unsafe { System.dealloc(ptr, Layout::from_size_align_unchecked(size, align)) }
     }
 
+    #[requires(align.is_power_of_two())]
     #[rustc_std_internal_symbol]
     pub unsafe extern "C" fn __rdl_realloc(
         ptr: *mut u8,
@@ -425,6 +444,7 @@ pub mod __default_lib_allocator {
         }
     }
 
+    #[requires(align.is_power_of_two())]
     #[rustc_std_internal_symbol]
     pub unsafe extern "C" fn __rdl_alloc_zeroed(size: usize, align: usize) -> *mut u8 {
         // SAFETY: see the guarantees expected by `Layout::from_size_align` and