diff --git a/library/core/src/alloc/layout.rs b/library/core/src/alloc/layout.rs
index 0b92767c93205..c63db5aa0aa2f 100644
--- a/library/core/src/alloc/layout.rs
+++ b/library/core/src/alloc/layout.rs
@@ -4,12 +4,16 @@
 // collections, resulting in having to optimize down excess IR multiple times.
 // Your performance intuition is useless. Run perf.
 
+use safety::requires;
 use crate::cmp;
 use crate::error::Error;
 use crate::fmt;
 use crate::mem;
 use crate::ptr::{Alignment, NonNull};
 
+#[cfg(kani)]
+use crate::kani;
+
 // While this function is used in one place and its implementation
 // could be inlined, the previous attempts to do so made rustc
 // slower:
@@ -117,6 +121,7 @@ impl Layout {
     #[must_use]
     #[inline]
     #[rustc_allow_const_fn_unstable(ptr_alignment_type)]
+    #[requires(Layout::from_size_align(size, align).is_ok())]
     pub const unsafe fn from_size_align_unchecked(size: usize, align: usize) -> Self {
         // SAFETY: the caller is required to uphold the preconditions.
         unsafe { Layout { size, align: Alignment::new_unchecked(align) } }
@@ -492,3 +497,21 @@ impl fmt::Display for LayoutError {
         f.write_str("invalid parameters to Layout::from_size_align")
     }
 }
+
+#[cfg(kani)]
+#[unstable(feature="kani", issue="none")]
+mod verify {
+    use super::*;
+
+    #[kani::proof_for_contract(Layout::from_size_align_unchecked)]
+    pub fn check_from_size_align_unchecked() {
+        let s = kani::any::<usize>();
+        let a = kani::any::<usize>();
+
+        unsafe {
+            let layout = Layout::from_size_align_unchecked(s, a);
+            assert_eq!(layout.size(), s);
+            assert_eq!(layout.align(), a);
+        }
+    }
+}
diff --git a/library/core/src/ptr/alignment.rs b/library/core/src/ptr/alignment.rs
index 68fce3960c78c..e5f5bf6a50313 100644
--- a/library/core/src/ptr/alignment.rs
+++ b/library/core/src/ptr/alignment.rs
@@ -1,8 +1,12 @@
+use safety::requires;
 use crate::num::NonZero;
 #[cfg(debug_assertions)]
 use crate::ub_checks::assert_unsafe_precondition;
 use crate::{cmp, fmt, hash, mem, num};
 
+#[cfg(kani)]
+use crate::kani;
+
 /// A type storing a `usize` which is a power of two, and thus
 /// represents a possible alignment in the Rust abstract machine.
 ///
@@ -76,6 +80,8 @@ 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)]
     pub const unsafe fn new_unchecked(align: usize) -> Self {
         #[cfg(debug_assertions)]
         assert_unsafe_precondition!(