diff --git a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/builtin.rs b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/builtin.rs
index 129add00023f..16065de74bf3 100644
--- a/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/builtin.rs
+++ b/compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/builtin.rs
@@ -37,6 +37,7 @@ pub enum BuiltinFn {
     Log2f,
     Logf,
     Malloc,
+    Memcmp,
     Memcpy,
     Memmove,
     Memset,
@@ -93,6 +94,7 @@ impl ToString for BuiltinFn {
             Log2f => "log2f",
             Logf => "logf",
             Malloc => "malloc",
+            Memcmp => "memcmp",
             Memcpy => "memcpy",
             Memmove => "memmove",
             Memset => "memset",
@@ -151,6 +153,7 @@ impl BuiltinFn {
             Log2f => vec![Type::float()],
             Logf => vec![Type::float()],
             Malloc => vec![Type::size_t()],
+            Memcmp => vec![Type::void_pointer(), Type::void_pointer(), Type::size_t()],
             Memcpy => vec![Type::void_pointer(), Type::void_pointer(), Type::size_t()],
             Memmove => vec![Type::void_pointer(), Type::void_pointer(), Type::size_t()],
             Memset => vec![Type::void_pointer(), Type::c_int(), Type::size_t()],
@@ -206,6 +209,7 @@ impl BuiltinFn {
             Log2f => Type::float(),
             Logf => Type::float(),
             Malloc => Type::void_pointer(),
+            Memcmp => Type::c_int(),
             Memcpy => Type::void_pointer(),
             Memmove => Type::void_pointer(),
             Memset => Type::void_pointer(),
@@ -262,6 +266,7 @@ impl BuiltinFn {
             Log2f,
             Logf,
             Malloc,
+            Memcmp,
             Memcpy,
             Memmove,
             Memset,
diff --git a/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs b/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs
index be8d91874a5d..21384762c370 100644
--- a/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs
+++ b/compiler/rustc_codegen_llvm/src/gotoc/intrinsic.rs
@@ -360,6 +360,7 @@ impl<'tcx> GotocCtx<'tcx> {
             "ptr_guaranteed_eq" => codegen_intrinsic_boolean_binop!(eq),
             "ptr_guaranteed_ne" => codegen_intrinsic_boolean_binop!(neq),
             "ptr_offset_from" => self.codegen_ptr_offset_from(fargs, p, loc),
+            "raw_eq" => self.codegen_intrinsic_raw_eq(instance, fargs, p, loc),
             "rintf32" => codegen_simple_intrinsic!(Rintf),
             "rintf64" => codegen_simple_intrinsic!(Rint),
             "rotate_left" => codegen_intrinsic_binop!(rol),
@@ -666,6 +667,33 @@ impl<'tcx> GotocCtx<'tcx> {
         self.codegen_expr_to_place(p, expr)
     }
 
+    // `raw_eq` determines whether the raw bytes of two values are equal.
+    // https://stdrs.dev/nightly/x86_64-pc-windows-gnu/std/intrinsics/fn.raw_eq.html
+    //
+    // The implementation below calls `memcmp` and returns equal if the result is zero.
+    //
+    // TODO: Handle more cases in this intrinsic by looking into the parameters' layouts.
+    // TODO: Fix soundness issues in this intrinsic. It's UB to call `raw_eq` if any of
+    // the bytes in the first or second arguments are uninitialized.
+    fn codegen_intrinsic_raw_eq(
+        &mut self,
+        instance: Instance<'tcx>,
+        mut fargs: Vec<Expr>,
+        p: &Place<'tcx>,
+        loc: Location,
+    ) -> Stmt {
+        let ty = self.monomorphize(instance.substs.type_at(0));
+        let dst = fargs.remove(0).cast_to(Type::void_pointer());
+        let val = fargs.remove(0).cast_to(Type::void_pointer());
+        let layout = self.layout_of(ty);
+        let sz = Expr::int_constant(layout.size.bytes(), Type::size_t());
+        let e = BuiltinFn::Memcmp
+            .call(vec![dst, val, sz], loc)
+            .eq(Type::c_int().zero())
+            .cast_to(Type::c_bool());
+        self.codegen_expr_to_place(p, e)
+    }
+
     /// This function computes the size and alignment of a dynamically-sized type.
     /// The implementations follows closely the SSA implementation found in
     /// rustc_codegen_ssa::glue::size_and_align_of_dst.
diff --git a/src/test/cbmc/Intrinsics/raw_eq.rs b/src/test/cbmc/Intrinsics/raw_eq.rs
new file mode 100644
index 000000000000..bff99565568c
--- /dev/null
+++ b/src/test/cbmc/Intrinsics/raw_eq.rs
@@ -0,0 +1,28 @@
+// Copyright Amazon.com, Inc. or its affiliates. All Rights Reserved.
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+#![feature(core_intrinsics)]
+#![feature(const_intrinsic_raw_eq)]
+#![deny(const_err)]
+
+pub fn main() {
+    // Check that we get the expected results for the `raw_eq` intrinsic
+    use std::intrinsics::raw_eq;
+
+    let raw_eq_i32_true: bool = unsafe { raw_eq(&42_i32, &42) };
+    assert!(raw_eq_i32_true);
+
+    let raw_eq_i32_false: bool = unsafe { raw_eq(&4_i32, &2) };
+    assert!(!raw_eq_i32_false);
+
+    let raw_eq_char_true: bool = unsafe { raw_eq(&'a', &'a') };
+    assert!(raw_eq_char_true);
+
+    let raw_eq_char_false: bool = unsafe { raw_eq(&'a', &'A') };
+    assert!(!raw_eq_char_false);
+
+    let raw_eq_array_true: bool = unsafe { raw_eq(&[13_u8, 42], &[13, 42]) };
+    assert!(raw_eq_array_true);
+
+    const raw_eq_array_false: bool = unsafe { raw_eq(&[13_u8, 42], &[42, 13]) };
+    assert!(!raw_eq_array_false);
+}