diff --git a/cprover_bindings/src/goto_program/builtin.rs b/cprover_bindings/src/goto_program/builtin.rs
index dc703ce83edc..258691b9ade4 100644
--- a/cprover_bindings/src/goto_program/builtin.rs
+++ b/cprover_bindings/src/goto_program/builtin.rs
@@ -47,6 +47,7 @@ pub enum BuiltinFn {
     Memset,
     Nearbyint,
     Nearbyintf,
+    Posixmemalign,
     Pow,
     Powf,
     Powi,
@@ -109,6 +110,7 @@ impl ToString for BuiltinFn {
             Memset => "memset",
             Nearbyint => "nearbyint",
             Nearbyintf => "nearbyintf",
+            Posixmemalign => "posix_memalign",
             Pow => "pow",
             Powf => "powf",
             Powi => "__builtin_powi",
@@ -173,6 +175,7 @@ impl BuiltinFn {
             Memset => vec![Type::void_pointer(), Type::c_int(), Type::size_t()],
             Nearbyint => vec![Type::double()],
             Nearbyintf => vec![Type::float()],
+            Posixmemalign => vec![Type::void_pointer(), Type::size_t(), Type::size_t()],
             Powf => vec![Type::float(), Type::float()],
             Powi => vec![Type::double(), Type::c_int()],
             Powif => vec![Type::float(), Type::c_int()],
@@ -234,6 +237,7 @@ impl BuiltinFn {
             Memset => Type::void_pointer(),
             Nearbyint => Type::double(),
             Nearbyintf => Type::float(),
+            Posixmemalign => Type::c_int(),
             Pow => Type::double(),
             Powf => Type::float(),
             Powi => Type::double(),
@@ -296,6 +300,7 @@ impl BuiltinFn {
             Memset,
             Nearbyint,
             Nearbyintf,
+            Posixmemalign,
             Pow,
             Powf,
             Powi,
diff --git a/tests/kani/LibC/posix_memalign.rs b/tests/kani/LibC/posix_memalign.rs
new file mode 100644
index 000000000000..dc4aa5aeaae0
--- /dev/null
+++ b/tests/kani/LibC/posix_memalign.rs
@@ -0,0 +1,46 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+//! Check support for `posix_memalign`.
+
+#![feature(rustc_private)]
+#![feature(allocator_api)]
+extern crate libc;
+
+use std::alloc::{Allocator, Layout, System};
+use std::ptr;
+
+#[repr(C, align(32))]
+struct MyStruct {
+    data: [u128; 10],
+}
+
+#[kani::proof]
+fn alloc_zeroed() {
+    let layout = Layout::new::<MyStruct>();
+    let ptr = System.allocate_zeroed(layout).unwrap();
+    assert_eq!(unsafe { ptr.as_ref()[0] }, 0);
+}
+
+// Source rust/src/libstd/sys/unix/alloc.rs
+unsafe fn aligned_malloc(layout: &Layout) -> *mut u8 {
+    let mut out = ptr::null_mut();
+    let ret = libc::posix_memalign(&mut out, layout.align(), layout.size());
+    if ret != 0 { ptr::null_mut() } else { out as *mut u8 }
+}
+
+#[kani::proof]
+fn aligned_malloc_main() {
+    let mut layout = Layout::from_size_align(0, 1);
+    let _mem = unsafe { aligned_malloc(&layout.unwrap()) };
+}
+
+#[kani::proof]
+fn posix_memalign_incorrect_alignment() {
+    let mut out = ptr::null_mut();
+    let small_page_size = 1;
+    let size = 4;
+    assert_eq!(unsafe { libc::posix_memalign(&mut out, small_page_size, size) }, libc::EINVAL);
+    let incorrect_page_size = 13;
+    assert_eq!(unsafe { libc::posix_memalign(&mut out, incorrect_page_size, size) }, libc::EINVAL);
+}