diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index 4e16f35c7f68..2f104d7112eb 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -622,16 +622,9 @@ impl<'tcx> GotocCtx<'tcx> {
             "wrapping_mul" => codegen_wrapping_op!(mul),
             "wrapping_sub" => codegen_wrapping_op!(sub),
             "write_bytes" => {
-                let dst = fargs.remove(0).cast_to(Type::void_pointer());
-                let val = fargs.remove(0).cast_to(Type::c_int());
-                let count = fargs.remove(0);
-                let ty = self.monomorphize(instance.substs.type_at(0));
-                let layout = self.layout_of(ty);
-                let sz = Expr::int_constant(layout.size.bytes(), Type::size_t());
-                let e = BuiltinFn::Memset.call(vec![dst, val, count.mul(sz)], loc);
-                self.codegen_expr_to_place(p, e)
+                assert!(self.place_ty(p).is_unit());
+                self.codegen_write_bytes(instance, intrinsic, fargs, loc)
             }
-
             // Unimplemented
             _ => codegen_unimplemented_intrinsic!(
                 "https://github.com/model-checking/kani/issues/new/choose"
@@ -1188,4 +1181,48 @@ impl<'tcx> GotocCtx<'tcx> {
         let expr = dst.dereference().assign(src, loc.clone());
         Stmt::block(vec![align_check, expr], loc)
     }
+
+    /// Sets `count * size_of::<T>()` bytes of memory starting at `dst` to `val`
+    /// https://doc.rust-lang.org/std/ptr/fn.write_bytes.html
+    ///
+    /// Undefined behavior if any of these conditions are violated:
+    ///  * `dst` must be valid for writes (done by memset writable check)
+    ///  * `dst` must be properly aligned (done by `align_check` below)
+    /// In addition, we check that computing `bytes` (i.e., the third argument
+    /// for the `memset` call) would not overflow
+    fn codegen_write_bytes(
+        &mut self,
+        instance: Instance<'tcx>,
+        intrinsic: &str,
+        mut fargs: Vec<Expr>,
+        loc: Location,
+    ) -> Stmt {
+        let dst = fargs.remove(0).cast_to(Type::void_pointer());
+        let val = fargs.remove(0).cast_to(Type::c_int());
+        let count = fargs.remove(0);
+
+        // Check that `dst` is properly aligned
+        let ty = self.monomorphize(instance.substs.type_at(0));
+        let align = self.is_aligned(ty, dst.clone());
+        let align_check = self.codegen_assert(
+            align,
+            PropertyClass::DefaultAssertion,
+            "`dst` is properly aligned",
+            loc,
+        );
+
+        // Check that computing `bytes` would not overflow
+        let layout = self.layout_of(ty);
+        let size = Expr::int_constant(layout.size.bytes(), Type::size_t());
+        let bytes = count.mul_overflow(size);
+        let overflow_check = self.codegen_assert(
+            bytes.overflowed.not(),
+            PropertyClass::ArithmeticOverflow,
+            format!("{}: attempt to compute `bytes` which would overflow", intrinsic).as_str(),
+            loc,
+        );
+
+        let memset_call = BuiltinFn::Memset.call(vec![dst, val, bytes.result], loc);
+        Stmt::block(vec![align_check, overflow_check, memset_call.as_stmt(loc)], loc)
+    }
 }
diff --git a/tests/expected/intrinsics/write_bytes/out-of-bounds/expected b/tests/expected/intrinsics/write_bytes/out-of-bounds/expected
new file mode 100644
index 000000000000..d69010f53d0c
--- /dev/null
+++ b/tests/expected/intrinsics/write_bytes/out-of-bounds/expected
@@ -0,0 +1,2 @@
+FAILURE\
+memset destination region writeable
\ No newline at end of file
diff --git a/tests/expected/intrinsics/write_bytes/out-of-bounds/main.rs b/tests/expected/intrinsics/write_bytes/out-of-bounds/main.rs
new file mode 100644
index 000000000000..7bd5ea7ea0ea
--- /dev/null
+++ b/tests/expected/intrinsics/write_bytes/out-of-bounds/main.rs
@@ -0,0 +1,19 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `write_bytes` fails if an out-of-bounds write is made.
+
+// This test is a modified version of the example in
+// https://doc.rust-lang.org/std/ptr/fn.write_bytes.html
+#![feature(core_intrinsics)]
+use std::intrinsics::write_bytes;
+
+#[kani::proof]
+fn main() {
+    let mut vec = vec![0u32; 4];
+    unsafe {
+        let vec_ptr = vec.as_mut_ptr().add(4);
+        write_bytes(vec_ptr, 0xfe, 1);
+    }
+    assert_eq!(vec, [0, 0, 0, 0]);
+}
diff --git a/tests/expected/intrinsics/write_bytes/overflow/expected b/tests/expected/intrinsics/write_bytes/overflow/expected
new file mode 100644
index 000000000000..4fb5bfd4c9ee
--- /dev/null
+++ b/tests/expected/intrinsics/write_bytes/overflow/expected
@@ -0,0 +1,2 @@
+FAILURE\
+write_bytes: attempt to compute `bytes` which would overflow
\ No newline at end of file
diff --git a/tests/expected/intrinsics/write_bytes/overflow/main.rs b/tests/expected/intrinsics/write_bytes/overflow/main.rs
new file mode 100644
index 000000000000..0e2ff04a90b9
--- /dev/null
+++ b/tests/expected/intrinsics/write_bytes/overflow/main.rs
@@ -0,0 +1,20 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `write_bytes` triggers the overflow check.
+
+// This test is a modified version of the example in
+// https://doc.rust-lang.org/std/ptr/fn.write_bytes.html
+#![feature(core_intrinsics)]
+use std::intrinsics::write_bytes;
+
+#[kani::proof]
+fn main() {
+    let mut vec = vec![0u32; 4];
+    unsafe {
+        let vec_ptr = vec.as_mut_ptr();
+        // Passing `usize::MAX + 1` is guaranteed to
+        // overflow when computing the number of bytes
+        write_bytes(vec_ptr, 0xfe, usize::MAX / 4 + 1);
+    }
+}
diff --git a/tests/expected/intrinsics/write_bytes/unaligned/expected b/tests/expected/intrinsics/write_bytes/unaligned/expected
new file mode 100644
index 000000000000..0fe63b4113d4
--- /dev/null
+++ b/tests/expected/intrinsics/write_bytes/unaligned/expected
@@ -0,0 +1,2 @@
+FAILURE\
+`dst` is properly aligned
\ No newline at end of file
diff --git a/tests/expected/intrinsics/write_bytes/unaligned/main.rs b/tests/expected/intrinsics/write_bytes/unaligned/main.rs
new file mode 100644
index 000000000000..4a941a56c39d
--- /dev/null
+++ b/tests/expected/intrinsics/write_bytes/unaligned/main.rs
@@ -0,0 +1,22 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `write_bytes` fails when `dst` is not aligned.
+
+// This test is a modified version of the example in
+// https://doc.rust-lang.org/std/ptr/fn.write_bytes.html
+use std::intrinsics::write_bytes;
+
+#[kani::proof]
+fn main() {
+    let mut vec = vec![0u32; 4];
+    unsafe {
+        let vec_ptr = vec.as_mut_ptr();
+        // Obtain an unaligned pointer by casting into `*mut u8`,
+        // adding an offset of 1 and casting back into `*mut u32`
+        let vec_ptr_u8: *mut u8 = vec_ptr as *mut u8;
+        let unaligned_ptr = vec_ptr_u8.add(1) as *mut u32;
+        write_bytes(unaligned_ptr, 0xfe, 2);
+    }
+    assert_eq!(vec, [0xfefefe00, 0xfefefefe, 0x000000fe, 0]);
+}
diff --git a/tests/kani/Intrinsics/WriteBytes/main.rs b/tests/kani/Intrinsics/WriteBytes/main.rs
new file mode 100644
index 000000000000..395c1c03c355
--- /dev/null
+++ b/tests/kani/Intrinsics/WriteBytes/main.rs
@@ -0,0 +1,19 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Checks that `write_bytes` works as expected.
+
+// This test is a modified version of the example in
+// https://doc.rust-lang.org/std/ptr/fn.write_bytes.html
+#![feature(core_intrinsics)]
+use std::intrinsics::write_bytes;
+
+#[kani::proof]
+fn main() {
+    let mut vec = vec![0u32; 4];
+    unsafe {
+        let vec_ptr = vec.as_mut_ptr();
+        write_bytes(vec_ptr, 0xfe, 2);
+    }
+    assert_eq!(vec, [0xfefefefe, 0xfefefefe, 0, 0]);
+}