diff --git a/.github/workflows/toolchain-upgrade.yml b/.github/workflows/toolchain-upgrade.yml
index b11f4e6b591a..76c3a5484414 100644
--- a/.github/workflows/toolchain-upgrade.yml
+++ b/.github/workflows/toolchain-upgrade.yml
@@ -64,7 +64,7 @@ jobs:
                 https://github.com/rust-lang/rust/commit/${{ env.next_toolchain_hash }}. The log
                 for this commit range is:
 
-                ${{ env.git_log }}`
+                ` + process.env.git_log
             })
 
       - name: Create Issue
diff --git a/.github/workflows/verify-std-check.yml b/.github/workflows/verify-std-check.yml
index 1bad09cd3c6d..6935b2bb4073 100644
--- a/.github/workflows/verify-std-check.yml
+++ b/.github/workflows/verify-std-check.yml
@@ -59,7 +59,7 @@ jobs:
         continue-on-error: true
         run: |
           kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \
-            -Z mem-predicates -Z ptr-to-ref-cast-checks
+            -Z mem-predicates
 
       # If the head failed, check if it's a new failure.
       - name: Checkout base
@@ -77,7 +77,7 @@ jobs:
         continue-on-error: true
         run: |
           kani verify-std -Z unstable-options ./library --target-dir ${{ runner.temp }} -Z function-contracts \
-            -Z mem-predicates -Z ptr-to-ref-cast-checks
+            -Z mem-predicates
 
       - name: Compare PR results
         if: steps.check-head.outcome != 'success' && steps.check-head.outcome != steps.check-base.outcome
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 47ae290853a3..d36def1a45f1 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -4,6 +4,46 @@ This file contains notable changes (e.g. breaking changes, major changes, etc.)
 
 This file was introduced starting Kani 0.23.0, so it only contains changes from version 0.23.0 onwards.
 
+## [0.54.0]
+
+### Major Changes
+* We added support for slices in the `#[kani::modifies(...)]` clauses when using function contracts.
+* We introduce an `#[safety_constraint(...)]` attribute helper for the `Arbitrary` and `Invariant` macros.
+* We enabled support for concrete playback for harness that contains stubs or function contracts.
+* We added support for log2*, log10*, powif*, fma*, and sqrt* intrisincs.
+
+### Breaking Changes
+* The `-Z ptr-to-ref-cast-checks` option has been removed, and pointer validity checks when casting raw pointers to references are now run by default.
+
+## What's Changed
+* Make Kani reject mutable pointer casts if padding is incompatible and memory initialization is checked by @artemagvanian in https://github.com/model-checking/kani/pull/3332
+* Fix visibility of some Kani intrinsics by @artemagvanian in https://github.com/model-checking/kani/pull/3323
+* Function Contracts: Modify Slices by @pi314mm in https://github.com/model-checking/kani/pull/3295
+* Support for disabling automatically generated pointer checks to avoid reinstrumentation by @artemagvanian in https://github.com/model-checking/kani/pull/3344
+* Add support for global transformations by @artemagvanian in https://github.com/model-checking/kani/pull/3348
+* Enable an `#[safety_constraint(...)]` attribute helper for the `Arbitrary` and `Invariant` macros by @adpaco-aws in https://github.com/model-checking/kani/pull/3283
+* Fix contract handling of promoted constants and constant static by @celinval in https://github.com/model-checking/kani/pull/3305
+* Bump CBMC Viewer to 3.9 by @tautschnig in https://github.com/model-checking/kani/pull/3373
+* Update to CBMC version 6.1.1 by @tautschnig in https://github.com/model-checking/kani/pull/2995
+* Define a struct-level `#[safety_constraint(...)]` attribute by @adpaco-aws in https://github.com/model-checking/kani/pull/3270
+* Enable concrete playback for contract and stubs by @celinval in https://github.com/model-checking/kani/pull/3389
+* Add code scanner tool by @celinval in https://github.com/model-checking/kani/pull/3120
+* Enable contracts in associated functions by @celinval in https://github.com/model-checking/kani/pull/3363
+* Enable log2*, log10* intrinsics by @tautschnig in https://github.com/model-checking/kani/pull/3001
+* Enable powif* intrinsics by @tautschnig in https://github.com/model-checking/kani/pull/2999
+* Enable fma* intrinsics by @tautschnig in https://github.com/model-checking/kani/pull/3002
+* Enable sqrt* intrinsics by @tautschnig in https://github.com/model-checking/kani/pull/3000
+* Remove assigns clause for ZST pointers by @carolynzech in https://github.com/model-checking/kani/pull/3417
+* Instrumentation for delayed UB stemming from uninitialized memory by @artemagvanian in https://github.com/model-checking/kani/pull/3374
+* Unify kani library and kani core logic by @jaisnan in https://github.com/model-checking/kani/pull/3333
+* Stabilize pointer-to-reference cast validity checks by @artemagvanian in https://github.com/model-checking/kani/pull/3426
+* Rust toolchain upgraded to `nightly-2024-08-07` by @jaisnan @qinheping @tautschnig @feliperodri
+
+## New Contributors
+* @carolynzech made their first contribution in https://github.com/model-checking/kani/pull/3387
+
+**Full Changelog**: https://github.com/model-checking/kani/compare/kani-0.53.0...kani-0.54.0
+
 ## [0.53.0]
 
 ### Major Changes
diff --git a/Cargo.lock b/Cargo.lock
index dcd7b057b3d8..12c28c49c1bf 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -92,7 +92,7 @@ checksum = "b048fb63fd8b5923fc5aa7b340d8e156aec7ec02f0c78fa8a6ddc2613f6f71de"
 
 [[package]]
 name = "build-kani"
-version = "0.53.0"
+version = "0.54.0"
 dependencies = [
  "anyhow",
  "cargo_metadata",
@@ -234,7 +234,7 @@ dependencies = [
 
 [[package]]
 name = "cprover_bindings"
-version = "0.53.0"
+version = "0.54.0"
 dependencies = [
  "lazy_static",
  "linear-map",
@@ -432,14 +432,15 @@ checksum = "49f1f14873335454500d59611f1cf4a4b0f786f9ac11f4312a78e4cf2566695b"
 
 [[package]]
 name = "kani"
-version = "0.53.0"
+version = "0.54.0"
 dependencies = [
+ "kani_core",
  "kani_macros",
 ]
 
 [[package]]
 name = "kani-compiler"
-version = "0.53.0"
+version = "0.54.0"
 dependencies = [
  "clap",
  "cprover_bindings",
@@ -460,7 +461,7 @@ dependencies = [
 
 [[package]]
 name = "kani-driver"
-version = "0.53.0"
+version = "0.54.0"
 dependencies = [
  "anyhow",
  "cargo_metadata",
@@ -488,7 +489,7 @@ dependencies = [
 
 [[package]]
 name = "kani-verifier"
-version = "0.53.0"
+version = "0.54.0"
 dependencies = [
  "anyhow",
  "home",
@@ -497,14 +498,14 @@ dependencies = [
 
 [[package]]
 name = "kani_core"
-version = "0.53.0"
+version = "0.54.0"
 dependencies = [
  "kani_macros",
 ]
 
 [[package]]
 name = "kani_macros"
-version = "0.53.0"
+version = "0.54.0"
 dependencies = [
  "proc-macro-error",
  "proc-macro2",
@@ -514,7 +515,7 @@ dependencies = [
 
 [[package]]
 name = "kani_metadata"
-version = "0.53.0"
+version = "0.54.0"
 dependencies = [
  "clap",
  "cprover_bindings",
@@ -990,9 +991,9 @@ dependencies = [
 
 [[package]]
 name = "serde_test"
-version = "1.0.176"
+version = "1.0.177"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "5a2f49ace1498612d14f7e0b8245519584db8299541dfe31a06374a828d620ab"
+checksum = "7f901ee573cab6b3060453d2d5f0bae4e6d628c23c0a962ff9b5f1d7c8d4f1ed"
 dependencies = [
  "serde",
 ]
@@ -1033,7 +1034,7 @@ checksum = "3c5e1a9a646d36c3599cd173a41282daf47c44583ad367b8e6837255952e5c67"
 
 [[package]]
 name = "std"
-version = "0.53.0"
+version = "0.54.0"
 dependencies = [
  "kani",
 ]
@@ -1097,15 +1098,15 @@ dependencies = [
 
 [[package]]
 name = "tempfile"
-version = "3.11.0"
+version = "3.12.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "b8fcd239983515c23a32fb82099f97d0b11b8c72f654ed659363a95c3dad7a53"
+checksum = "04cbcdd0c794ebb0d4cf35e88edd2f7d2c4c3e9a5a6dab322839b321c6a87a64"
 dependencies = [
  "cfg-if",
  "fastrand",
  "once_cell",
  "rustix",
- "windows-sys 0.52.0",
+ "windows-sys 0.59.0",
 ]
 
 [[package]]
diff --git a/Cargo.toml b/Cargo.toml
index 68b5bcc20ff3..f2301983fcb4 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani-verifier"
-version = "0.53.0"
+version = "0.54.0"
 edition = "2021"
 description = "A bit-precise model checker for Rust."
 readme = "README.md"
diff --git a/cprover_bindings/Cargo.toml b/cprover_bindings/Cargo.toml
index aced9e5b9b65..c53ffb207fcf 100644
--- a/cprover_bindings/Cargo.toml
+++ b/cprover_bindings/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "cprover_bindings"
-version = "0.53.0"
+version = "0.54.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
diff --git a/kani-compiler/Cargo.toml b/kani-compiler/Cargo.toml
index 23389c156302..24ed00f54338 100644
--- a/kani-compiler/Cargo.toml
+++ b/kani-compiler/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani-compiler"
-version = "0.53.0"
+version = "0.54.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
diff --git a/kani-compiler/src/args.rs b/kani-compiler/src/args.rs
index 3efc5c0f4f61..3fa74b0e5aba 100644
--- a/kani-compiler/src/args.rs
+++ b/kani-compiler/src/args.rs
@@ -82,9 +82,6 @@ pub enum ExtraChecks {
     /// Check that produced values are valid except for uninitialized values.
     /// See https://github.com/model-checking/kani/issues/920.
     Validity,
-    /// Check pointer validity when casting pointers to references.
-    /// See https://github.com/model-checking/kani/issues/2975.
-    PtrToRefCast,
     /// Check for using uninitialized memory.
     Uninit,
 }
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
index c4d5396f1fe8..421d79e943c4 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs
@@ -5,6 +5,7 @@ use super::typ;
 use super::{bb_label, PropertyClass};
 use crate::codegen_cprover_gotoc::codegen::ty_stable::pointee_type_stable;
 use crate::codegen_cprover_gotoc::{utils, GotocCtx};
+use crate::intrinsics::Intrinsic;
 use crate::unwrap_or_return_codegen_unimplemented_stmt;
 use cbmc::goto_program::{
     ArithmeticOverflowResult, BinaryOperator, BuiltinFn, Expr, Location, Stmt, Type,
@@ -114,7 +115,7 @@ impl<'tcx> GotocCtx<'tcx> {
         span: Span,
     ) -> Stmt {
         let intrinsic_name = instance.intrinsic_name().unwrap();
-        let intrinsic = intrinsic_name.as_str();
+        let intrinsic_str = intrinsic_name.as_str();
         let loc = self.codegen_span_stable(span);
         debug!(?instance, "codegen_intrinsic");
         debug!(?fargs, "codegen_intrinsic");
@@ -163,7 +164,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 let div_overflow_check = self.codegen_assert_assume(
                     div_does_not_overflow,
                     PropertyClass::ArithmeticOverflow,
-                    format!("attempt to compute {} which would overflow", intrinsic).as_str(),
+                    format!("attempt to compute {} which would overflow", intrinsic_str).as_str(),
                     loc,
                 );
                 let res = a.$f(b);
@@ -257,7 +258,7 @@ impl<'tcx> GotocCtx<'tcx> {
         macro_rules! codegen_atomic_binop {
             ($op: ident) => {{
                 let loc = self.codegen_span_stable(span);
-                self.store_concurrent_construct(intrinsic, loc);
+                self.store_concurrent_construct(intrinsic_str, loc);
                 let var1_ref = fargs.remove(0);
                 let var1 = var1_ref.dereference();
                 let (tmp, decl_stmt) =
@@ -280,7 +281,7 @@ impl<'tcx> GotocCtx<'tcx> {
         macro_rules! unstable_codegen {
             ($($tt:tt)*) => {{
                 let expr = self.codegen_unimplemented_expr(
-                    &format!("'{}' intrinsic", intrinsic),
+                    &format!("'{}' intrinsic", intrinsic_str),
                     cbmc_ret_ty,
                     loc,
                     "https://github.com/model-checking/kani/issues/new/choose",
@@ -289,342 +290,273 @@ impl<'tcx> GotocCtx<'tcx> {
             }};
         }
 
-        if let Some(stripped) = intrinsic.strip_prefix("simd_shuffle") {
-            assert!(fargs.len() == 3, "`simd_shuffle` had unexpected arguments {fargs:?}");
-            let n: u64 = self.simd_shuffle_length(stripped, farg_types, span);
-            return self.codegen_intrinsic_simd_shuffle(fargs, place, farg_types, ret_ty, n, span);
-        }
+        let intrinsic = Intrinsic::from_instance(&instance);
 
         match intrinsic {
-            "add_with_overflow" => {
+            Intrinsic::AddWithOverflow => {
                 self.codegen_op_with_overflow(BinaryOperator::OverflowResultPlus, fargs, place, loc)
             }
-            "arith_offset" => self.codegen_offset(intrinsic, instance, fargs, place, loc),
-            "assert_inhabited" => self.codegen_assert_intrinsic(instance, intrinsic, span),
-            "assert_mem_uninitialized_valid" => {
-                self.codegen_assert_intrinsic(instance, intrinsic, span)
+            Intrinsic::ArithOffset => {
+                self.codegen_offset(intrinsic_str, instance, fargs, place, loc)
+            }
+            Intrinsic::AssertInhabited => {
+                self.codegen_assert_intrinsic(instance, intrinsic_str, span)
+            }
+            Intrinsic::AssertMemUninitializedValid => {
+                self.codegen_assert_intrinsic(instance, intrinsic_str, span)
+            }
+            Intrinsic::AssertZeroValid => {
+                self.codegen_assert_intrinsic(instance, intrinsic_str, span)
             }
-            "assert_zero_valid" => self.codegen_assert_intrinsic(instance, intrinsic, span),
             // https://doc.rust-lang.org/core/intrinsics/fn.assume.html
             // Informs the optimizer that a condition is always true.
             // If the condition is false, the behavior is undefined.
-            "assume" => self.codegen_assert_assume(
+            Intrinsic::Assume => self.codegen_assert_assume(
                 fargs.remove(0).cast_to(Type::bool()),
                 PropertyClass::Assume,
                 "assumption failed",
                 loc,
             ),
-            "atomic_and_seqcst" => codegen_atomic_binop!(bitand),
-            "atomic_and_acquire" => codegen_atomic_binop!(bitand),
-            "atomic_and_acqrel" => codegen_atomic_binop!(bitand),
-            "atomic_and_release" => codegen_atomic_binop!(bitand),
-            "atomic_and_relaxed" => codegen_atomic_binop!(bitand),
-            name if name.starts_with("atomic_cxchg") => {
-                self.codegen_atomic_cxchg(intrinsic, fargs, place, loc)
+            Intrinsic::AtomicAnd(_) => codegen_atomic_binop!(bitand),
+            Intrinsic::AtomicCxchg(_) | Intrinsic::AtomicCxchgWeak(_) => {
+                self.codegen_atomic_cxchg(intrinsic_str, fargs, place, loc)
             }
-            "atomic_fence_seqcst" => self.codegen_atomic_noop(intrinsic, loc),
-            "atomic_fence_acquire" => self.codegen_atomic_noop(intrinsic, loc),
-            "atomic_fence_acqrel" => self.codegen_atomic_noop(intrinsic, loc),
-            "atomic_fence_release" => self.codegen_atomic_noop(intrinsic, loc),
-            "atomic_load_seqcst" => self.codegen_atomic_load(intrinsic, fargs, place, loc),
-            "atomic_load_acquire" => self.codegen_atomic_load(intrinsic, fargs, place, loc),
-            "atomic_load_relaxed" => self.codegen_atomic_load(intrinsic, fargs, place, loc),
-            "atomic_load_unordered" => self.codegen_atomic_load(intrinsic, fargs, place, loc),
-            "atomic_max_seqcst" => codegen_atomic_binop!(max),
-            "atomic_max_acquire" => codegen_atomic_binop!(max),
-            "atomic_max_acqrel" => codegen_atomic_binop!(max),
-            "atomic_max_release" => codegen_atomic_binop!(max),
-            "atomic_max_relaxed" => codegen_atomic_binop!(max),
-            "atomic_min_seqcst" => codegen_atomic_binop!(min),
-            "atomic_min_acquire" => codegen_atomic_binop!(min),
-            "atomic_min_acqrel" => codegen_atomic_binop!(min),
-            "atomic_min_release" => codegen_atomic_binop!(min),
-            "atomic_min_relaxed" => codegen_atomic_binop!(min),
-            "atomic_nand_seqcst" => codegen_atomic_binop!(bitnand),
-            "atomic_nand_acquire" => codegen_atomic_binop!(bitnand),
-            "atomic_nand_acqrel" => codegen_atomic_binop!(bitnand),
-            "atomic_nand_release" => codegen_atomic_binop!(bitnand),
-            "atomic_nand_relaxed" => codegen_atomic_binop!(bitnand),
-            "atomic_or_seqcst" => codegen_atomic_binop!(bitor),
-            "atomic_or_acquire" => codegen_atomic_binop!(bitor),
-            "atomic_or_acqrel" => codegen_atomic_binop!(bitor),
-            "atomic_or_release" => codegen_atomic_binop!(bitor),
-            "atomic_or_relaxed" => codegen_atomic_binop!(bitor),
-            "atomic_singlethreadfence_seqcst" => self.codegen_atomic_noop(intrinsic, loc),
-            "atomic_singlethreadfence_acquire" => self.codegen_atomic_noop(intrinsic, loc),
-            "atomic_singlethreadfence_acqrel" => self.codegen_atomic_noop(intrinsic, loc),
-            "atomic_singlethreadfence_release" => self.codegen_atomic_noop(intrinsic, loc),
-            "atomic_store_seqcst" => self.codegen_atomic_store(intrinsic, fargs, place, loc),
-            "atomic_store_release" => self.codegen_atomic_store(intrinsic, fargs, place, loc),
-            "atomic_store_relaxed" => self.codegen_atomic_store(intrinsic, fargs, place, loc),
-            "atomic_store_unordered" => self.codegen_atomic_store(intrinsic, fargs, place, loc),
-            "atomic_umax_seqcst" => codegen_atomic_binop!(max),
-            "atomic_umax_acquire" => codegen_atomic_binop!(max),
-            "atomic_umax_acqrel" => codegen_atomic_binop!(max),
-            "atomic_umax_release" => codegen_atomic_binop!(max),
-            "atomic_umax_relaxed" => codegen_atomic_binop!(max),
-            "atomic_umin_seqcst" => codegen_atomic_binop!(min),
-            "atomic_umin_acquire" => codegen_atomic_binop!(min),
-            "atomic_umin_acqrel" => codegen_atomic_binop!(min),
-            "atomic_umin_release" => codegen_atomic_binop!(min),
-            "atomic_umin_relaxed" => codegen_atomic_binop!(min),
-            "atomic_xadd_seqcst" => codegen_atomic_binop!(plus),
-            "atomic_xadd_acquire" => codegen_atomic_binop!(plus),
-            "atomic_xadd_acqrel" => codegen_atomic_binop!(plus),
-            "atomic_xadd_release" => codegen_atomic_binop!(plus),
-            "atomic_xadd_relaxed" => codegen_atomic_binop!(plus),
-            "atomic_xchg_seqcst" => self.codegen_atomic_store(intrinsic, fargs, place, loc),
-            "atomic_xchg_acquire" => self.codegen_atomic_store(intrinsic, fargs, place, loc),
-            "atomic_xchg_acqrel" => self.codegen_atomic_store(intrinsic, fargs, place, loc),
-            "atomic_xchg_release" => self.codegen_atomic_store(intrinsic, fargs, place, loc),
-            "atomic_xchg_relaxed" => self.codegen_atomic_store(intrinsic, fargs, place, loc),
-            "atomic_xor_seqcst" => codegen_atomic_binop!(bitxor),
-            "atomic_xor_acquire" => codegen_atomic_binop!(bitxor),
-            "atomic_xor_acqrel" => codegen_atomic_binop!(bitxor),
-            "atomic_xor_release" => codegen_atomic_binop!(bitxor),
-            "atomic_xor_relaxed" => codegen_atomic_binop!(bitxor),
-            "atomic_xsub_seqcst" => codegen_atomic_binop!(sub),
-            "atomic_xsub_acquire" => codegen_atomic_binop!(sub),
-            "atomic_xsub_acqrel" => codegen_atomic_binop!(sub),
-            "atomic_xsub_release" => codegen_atomic_binop!(sub),
-            "atomic_xsub_relaxed" => codegen_atomic_binop!(sub),
-            "bitreverse" => {
+
+            Intrinsic::AtomicFence(_) => self.codegen_atomic_noop(intrinsic_str, loc),
+            Intrinsic::AtomicLoad(_) => self.codegen_atomic_load(intrinsic_str, fargs, place, loc),
+            Intrinsic::AtomicMax(_) => codegen_atomic_binop!(max),
+            Intrinsic::AtomicMin(_) => codegen_atomic_binop!(min),
+            Intrinsic::AtomicNand(_) => codegen_atomic_binop!(bitnand),
+            Intrinsic::AtomicOr(_) => codegen_atomic_binop!(bitor),
+            Intrinsic::AtomicSingleThreadFence(_) => self.codegen_atomic_noop(intrinsic_str, loc),
+            Intrinsic::AtomicStore(_) => {
+                self.codegen_atomic_store(intrinsic_str, fargs, place, loc)
+            }
+            Intrinsic::AtomicUmax(_) => codegen_atomic_binop!(max),
+            Intrinsic::AtomicUmin(_) => codegen_atomic_binop!(min),
+            Intrinsic::AtomicXadd(_) => codegen_atomic_binop!(plus),
+            Intrinsic::AtomicXchg(_) => self.codegen_atomic_store(intrinsic_str, fargs, place, loc),
+            Intrinsic::AtomicXor(_) => codegen_atomic_binop!(bitxor),
+            Intrinsic::AtomicXsub(_) => codegen_atomic_binop!(sub),
+            Intrinsic::Bitreverse => {
                 self.codegen_expr_to_place_stable(place, fargs.remove(0).bitreverse(), loc)
             }
             // black_box is an identity function that hints to the compiler
             // to be maximally pessimistic to limit optimizations
-            "black_box" => self.codegen_expr_to_place_stable(place, fargs.remove(0), loc),
-            "breakpoint" => Stmt::skip(loc),
-            "bswap" => self.codegen_expr_to_place_stable(place, fargs.remove(0).bswap(), loc),
-            "caller_location" => self.codegen_unimplemented_stmt(
-                intrinsic,
-                loc,
-                "https://github.com/model-checking/kani/issues/374",
-            ),
-            "catch_unwind" => self.codegen_unimplemented_stmt(
-                intrinsic,
-                loc,
-                "https://github.com/model-checking/kani/issues/267",
-            ),
-            "ceilf32" => codegen_simple_intrinsic!(Ceilf),
-            "ceilf64" => codegen_simple_intrinsic!(Ceil),
-            "compare_bytes" => self.codegen_compare_bytes(fargs, place, loc),
-            "copy" => self.codegen_copy(intrinsic, false, fargs, farg_types, Some(place), loc),
-            "copy_nonoverlapping" => unreachable!(
-                "Expected `core::intrinsics::unreachable` to be handled by `StatementKind::CopyNonOverlapping`"
-            ),
-            "copysignf32" => codegen_simple_intrinsic!(Copysignf),
-            "copysignf64" => codegen_simple_intrinsic!(Copysign),
-            "cosf32" => codegen_simple_intrinsic!(Cosf),
-            "cosf64" => codegen_simple_intrinsic!(Cos),
-            "ctlz" => codegen_count_intrinsic!(ctlz, true),
-            "ctlz_nonzero" => codegen_count_intrinsic!(ctlz, false),
-            "ctpop" => self.codegen_ctpop(place, span, fargs.remove(0), farg_types[0]),
-            "cttz" => codegen_count_intrinsic!(cttz, true),
-            "cttz_nonzero" => codegen_count_intrinsic!(cttz, false),
-            "discriminant_value" => {
+            Intrinsic::BlackBox => self.codegen_expr_to_place_stable(place, fargs.remove(0), loc),
+            Intrinsic::Breakpoint => Stmt::skip(loc),
+            Intrinsic::Bswap => {
+                self.codegen_expr_to_place_stable(place, fargs.remove(0).bswap(), loc)
+            }
+            Intrinsic::CeilF32 => codegen_simple_intrinsic!(Ceilf),
+            Intrinsic::CeilF64 => codegen_simple_intrinsic!(Ceil),
+            Intrinsic::CompareBytes => self.codegen_compare_bytes(fargs, place, loc),
+            Intrinsic::Copy => {
+                self.codegen_copy(intrinsic_str, false, fargs, farg_types, Some(place), loc)
+            }
+            Intrinsic::CopySignF32 => codegen_simple_intrinsic!(Copysignf),
+            Intrinsic::CopySignF64 => codegen_simple_intrinsic!(Copysign),
+            Intrinsic::CosF32 => codegen_simple_intrinsic!(Cosf),
+            Intrinsic::CosF64 => codegen_simple_intrinsic!(Cos),
+            Intrinsic::Ctlz => codegen_count_intrinsic!(ctlz, true),
+            Intrinsic::CtlzNonZero => codegen_count_intrinsic!(ctlz, false),
+            Intrinsic::Ctpop => self.codegen_ctpop(place, span, fargs.remove(0), farg_types[0]),
+            Intrinsic::Cttz => codegen_count_intrinsic!(cttz, true),
+            Intrinsic::CttzNonZero => codegen_count_intrinsic!(cttz, false),
+            Intrinsic::DiscriminantValue => {
                 let sig = instance.ty().kind().fn_sig().unwrap().skip_binder();
                 let ty = pointee_type_stable(sig.inputs()[0]).unwrap();
                 let e = self.codegen_get_discriminant(fargs.remove(0).dereference(), ty, ret_ty);
                 self.codegen_expr_to_place_stable(place, e, loc)
             }
-            "exact_div" => self.codegen_exact_div(fargs, place, loc),
-            "exp2f32" => codegen_simple_intrinsic!(Exp2f),
-            "exp2f64" => codegen_simple_intrinsic!(Exp2),
-            "expf32" => codegen_simple_intrinsic!(Expf),
-            "expf64" => codegen_simple_intrinsic!(Exp),
-            "fabsf32" => codegen_simple_intrinsic!(Fabsf),
-            "fabsf64" => codegen_simple_intrinsic!(Fabs),
-            "fadd_fast" => {
+            Intrinsic::ExactDiv => self.codegen_exact_div(fargs, place, loc),
+            Intrinsic::Exp2F32 => codegen_simple_intrinsic!(Exp2f),
+            Intrinsic::Exp2F64 => codegen_simple_intrinsic!(Exp2),
+            Intrinsic::ExpF32 => codegen_simple_intrinsic!(Expf),
+            Intrinsic::ExpF64 => codegen_simple_intrinsic!(Exp),
+            Intrinsic::FabsF32 => codegen_simple_intrinsic!(Fabsf),
+            Intrinsic::FabsF64 => codegen_simple_intrinsic!(Fabs),
+            Intrinsic::FaddFast => {
                 let fargs_clone = fargs.clone();
                 let binop_stmt = codegen_intrinsic_binop!(plus);
-                self.add_finite_args_checks(intrinsic, fargs_clone, binop_stmt, span)
+                self.add_finite_args_checks(intrinsic_str, fargs_clone, binop_stmt, span)
             }
-            "fdiv_fast" => {
+            Intrinsic::FdivFast => {
                 let fargs_clone = fargs.clone();
                 let binop_stmt = codegen_intrinsic_binop!(div);
-                self.add_finite_args_checks(intrinsic, fargs_clone, binop_stmt, span)
+                self.add_finite_args_checks(intrinsic_str, fargs_clone, binop_stmt, span)
             }
-            "floorf32" => codegen_simple_intrinsic!(Floorf),
-            "floorf64" => codegen_simple_intrinsic!(Floor),
-            "fmaf32" => codegen_simple_intrinsic!(Fmaf),
-            "fmaf64" => codegen_simple_intrinsic!(Fma),
-            "fmul_fast" => {
+            Intrinsic::FloorF32 => codegen_simple_intrinsic!(Floorf),
+            Intrinsic::FloorF64 => codegen_simple_intrinsic!(Floor),
+            Intrinsic::FmafF32 => codegen_simple_intrinsic!(Fmaf),
+            Intrinsic::FmafF64 => codegen_simple_intrinsic!(Fma),
+            Intrinsic::FmulFast => {
                 let fargs_clone = fargs.clone();
                 let binop_stmt = codegen_intrinsic_binop!(mul);
-                self.add_finite_args_checks(intrinsic, fargs_clone, binop_stmt, span)
+                self.add_finite_args_checks(intrinsic_str, fargs_clone, binop_stmt, span)
             }
-            "forget" => Stmt::skip(loc),
-            "fsub_fast" => {
+            Intrinsic::Forget => Stmt::skip(loc),
+            Intrinsic::FsubFast => {
                 let fargs_clone = fargs.clone();
                 let binop_stmt = codegen_intrinsic_binop!(sub);
-                self.add_finite_args_checks(intrinsic, fargs_clone, binop_stmt, span)
+                self.add_finite_args_checks(intrinsic_str, fargs_clone, binop_stmt, span)
             }
-            "is_val_statically_known" => {
+            Intrinsic::IsValStaticallyKnown => {
                 // Returning false is sound according do this intrinsic's documentation:
                 // https://doc.rust-lang.org/nightly/std/intrinsics/fn.is_val_statically_known.html
                 self.codegen_expr_to_place_stable(place, Expr::c_false(), loc)
             }
-            "likely" => self.codegen_expr_to_place_stable(place, fargs.remove(0), loc),
-            "log10f32" => codegen_simple_intrinsic!(Log10f),
-            "log10f64" => codegen_simple_intrinsic!(Log10),
-            "log2f32" => codegen_simple_intrinsic!(Log2f),
-            "log2f64" => codegen_simple_intrinsic!(Log2),
-            "logf32" => codegen_simple_intrinsic!(Logf),
-            "logf64" => codegen_simple_intrinsic!(Log),
-            "maxnumf32" => codegen_simple_intrinsic!(Fmaxf),
-            "maxnumf64" => codegen_simple_intrinsic!(Fmax),
-            "min_align_of" => codegen_intrinsic_const!(),
-            "min_align_of_val" => codegen_size_align!(align),
-            "minnumf32" => codegen_simple_intrinsic!(Fminf),
-            "minnumf64" => codegen_simple_intrinsic!(Fmin),
-            "mul_with_overflow" => {
+            Intrinsic::Likely => self.codegen_expr_to_place_stable(place, fargs.remove(0), loc),
+            Intrinsic::Log10F32 => codegen_simple_intrinsic!(Log10f),
+            Intrinsic::Log10F64 => codegen_simple_intrinsic!(Log10),
+            Intrinsic::Log2F32 => codegen_simple_intrinsic!(Log2f),
+            Intrinsic::Log2F64 => codegen_simple_intrinsic!(Log2),
+            Intrinsic::LogF32 => codegen_simple_intrinsic!(Logf),
+            Intrinsic::LogF64 => codegen_simple_intrinsic!(Log),
+            Intrinsic::MaxNumF32 => codegen_simple_intrinsic!(Fmaxf),
+            Intrinsic::MaxNumF64 => codegen_simple_intrinsic!(Fmax),
+            Intrinsic::MinAlignOf => codegen_intrinsic_const!(),
+            Intrinsic::MinAlignOfVal => codegen_size_align!(align),
+            Intrinsic::MinNumF32 => codegen_simple_intrinsic!(Fminf),
+            Intrinsic::MinNumF64 => codegen_simple_intrinsic!(Fmin),
+            Intrinsic::MulWithOverflow => {
                 self.codegen_op_with_overflow(BinaryOperator::OverflowResultMult, fargs, place, loc)
             }
-            "nearbyintf32" => codegen_simple_intrinsic!(Nearbyintf),
-            "nearbyintf64" => codegen_simple_intrinsic!(Nearbyint),
-            "needs_drop" => codegen_intrinsic_const!(),
-            // As of https://github.com/rust-lang/rust/pull/110822 the `offset` intrinsic is lowered to `mir::BinOp::Offset`
-            "offset" => unreachable!(
-                "Expected `core::intrinsics::unreachable` to be handled by `BinOp::OffSet`"
-            ),
-            "powf32" => codegen_simple_intrinsic!(Powf),
-            "powf64" => codegen_simple_intrinsic!(Pow),
-            "powif32" => codegen_simple_intrinsic!(Powif),
-            "powif64" => codegen_simple_intrinsic!(Powi),
-            "pref_align_of" => codegen_intrinsic_const!(),
-            "ptr_guaranteed_cmp" => self.codegen_ptr_guaranteed_cmp(fargs, place, loc),
-            "ptr_offset_from" => self.codegen_ptr_offset_from(fargs, place, loc),
-            "ptr_offset_from_unsigned" => self.codegen_ptr_offset_from_unsigned(fargs, place, loc),
-            "raw_eq" => self.codegen_intrinsic_raw_eq(instance, fargs, place, loc),
-            "retag_box_to_raw" => self.codegen_retag_box_to_raw(fargs, place, loc),
-            "rintf32" => codegen_simple_intrinsic!(Rintf),
-            "rintf64" => codegen_simple_intrinsic!(Rint),
-            "rotate_left" => codegen_intrinsic_binop!(rol),
-            "rotate_right" => codegen_intrinsic_binop!(ror),
-            "roundf32" => codegen_simple_intrinsic!(Roundf),
-            "roundf64" => codegen_simple_intrinsic!(Round),
-            "saturating_add" => codegen_intrinsic_binop_with_mm!(saturating_add),
-            "saturating_sub" => codegen_intrinsic_binop_with_mm!(saturating_sub),
-            "sinf32" => codegen_simple_intrinsic!(Sinf),
-            "sinf64" => codegen_simple_intrinsic!(Sin),
-            "simd_add" => self.codegen_simd_op_with_overflow(
+            Intrinsic::NearbyIntF32 => codegen_simple_intrinsic!(Nearbyintf),
+            Intrinsic::NearbyIntF64 => codegen_simple_intrinsic!(Nearbyint),
+            Intrinsic::NeedsDrop => codegen_intrinsic_const!(),
+            Intrinsic::PowF32 => codegen_simple_intrinsic!(Powf),
+            Intrinsic::PowF64 => codegen_simple_intrinsic!(Pow),
+            Intrinsic::PowIF32 => codegen_simple_intrinsic!(Powif),
+            Intrinsic::PowIF64 => codegen_simple_intrinsic!(Powi),
+            Intrinsic::PrefAlignOf => codegen_intrinsic_const!(),
+            Intrinsic::PtrGuaranteedCmp => self.codegen_ptr_guaranteed_cmp(fargs, place, loc),
+            Intrinsic::PtrOffsetFrom => self.codegen_ptr_offset_from(fargs, place, loc),
+            Intrinsic::PtrOffsetFromUnsigned => {
+                self.codegen_ptr_offset_from_unsigned(fargs, place, loc)
+            }
+            Intrinsic::RawEq => self.codegen_intrinsic_raw_eq(instance, fargs, place, loc),
+            Intrinsic::RetagBoxToRaw => self.codegen_retag_box_to_raw(fargs, place, loc),
+            Intrinsic::RintF32 => codegen_simple_intrinsic!(Rintf),
+            Intrinsic::RintF64 => codegen_simple_intrinsic!(Rint),
+            Intrinsic::RotateLeft => codegen_intrinsic_binop!(rol),
+            Intrinsic::RotateRight => codegen_intrinsic_binop!(ror),
+            Intrinsic::RoundF32 => codegen_simple_intrinsic!(Roundf),
+            Intrinsic::RoundF64 => codegen_simple_intrinsic!(Round),
+            Intrinsic::SaturatingAdd => codegen_intrinsic_binop_with_mm!(saturating_add),
+            Intrinsic::SaturatingSub => codegen_intrinsic_binop_with_mm!(saturating_sub),
+            Intrinsic::SinF32 => codegen_simple_intrinsic!(Sinf),
+            Intrinsic::SinF64 => codegen_simple_intrinsic!(Sin),
+            Intrinsic::SimdAdd => self.codegen_simd_op_with_overflow(
                 Expr::plus,
                 Expr::add_overflow_p,
                 fargs,
-                intrinsic,
+                intrinsic_str,
                 place,
                 loc,
             ),
-            "simd_and" => codegen_intrinsic_binop!(bitand),
+            Intrinsic::SimdAnd => codegen_intrinsic_binop!(bitand),
             // TODO: `simd_rem` doesn't check for overflow cases for floating point operands.
             // <https://github.com/model-checking/kani/pull/2645>
-            "simd_div" | "simd_rem" => {
-                self.codegen_simd_div_with_overflow(fargs, intrinsic, place, loc)
+            Intrinsic::SimdDiv | Intrinsic::SimdRem => {
+                self.codegen_simd_div_with_overflow(fargs, intrinsic_str, place, loc)
             }
-            "simd_eq" => {
+            Intrinsic::SimdEq => {
                 self.codegen_simd_cmp(Expr::vector_eq, fargs, place, span, farg_types, ret_ty)
             }
-            "simd_extract" => {
+            Intrinsic::SimdExtract => {
                 self.codegen_intrinsic_simd_extract(fargs, place, farg_types, ret_ty, span)
             }
-            "simd_ge" => {
+            Intrinsic::SimdGe => {
                 self.codegen_simd_cmp(Expr::vector_ge, fargs, place, span, farg_types, ret_ty)
             }
-            "simd_gt" => {
+            Intrinsic::SimdGt => {
                 self.codegen_simd_cmp(Expr::vector_gt, fargs, place, span, farg_types, ret_ty)
             }
-            "simd_insert" => {
+            Intrinsic::SimdInsert => {
                 self.codegen_intrinsic_simd_insert(fargs, place, cbmc_ret_ty, farg_types, span, loc)
             }
-            "simd_le" => {
+            Intrinsic::SimdLe => {
                 self.codegen_simd_cmp(Expr::vector_le, fargs, place, span, farg_types, ret_ty)
             }
-            "simd_lt" => {
+            Intrinsic::SimdLt => {
                 self.codegen_simd_cmp(Expr::vector_lt, fargs, place, span, farg_types, ret_ty)
             }
-            "simd_mul" => self.codegen_simd_op_with_overflow(
+            Intrinsic::SimdMul => self.codegen_simd_op_with_overflow(
                 Expr::mul,
                 Expr::mul_overflow_p,
                 fargs,
-                intrinsic,
+                intrinsic_str,
                 place,
                 loc,
             ),
-            "simd_ne" => {
+            Intrinsic::SimdNe => {
                 self.codegen_simd_cmp(Expr::vector_neq, fargs, place, span, farg_types, ret_ty)
             }
-            "simd_or" => codegen_intrinsic_binop!(bitor),
-            "simd_shl" | "simd_shr" => {
-                self.codegen_simd_shift_with_distance_check(fargs, intrinsic, place, loc)
+            Intrinsic::SimdOr => codegen_intrinsic_binop!(bitor),
+            Intrinsic::SimdShl | Intrinsic::SimdShr => {
+                self.codegen_simd_shift_with_distance_check(fargs, intrinsic_str, place, loc)
+            }
+            Intrinsic::SimdShuffle(stripped) => {
+                let n: u64 = self.simd_shuffle_length(stripped.as_str(), farg_types, span);
+                self.codegen_intrinsic_simd_shuffle(fargs, place, farg_types, ret_ty, n, span)
             }
-            // "simd_shuffle#" => handled in an `if` preceding this match
-            "simd_sub" => self.codegen_simd_op_with_overflow(
+            Intrinsic::SimdSub => self.codegen_simd_op_with_overflow(
                 Expr::sub,
                 Expr::sub_overflow_p,
                 fargs,
-                intrinsic,
+                intrinsic_str,
                 place,
                 loc,
             ),
-            "simd_xor" => codegen_intrinsic_binop!(bitxor),
-            "size_of" => unreachable!(),
-            "size_of_val" => codegen_size_align!(size),
-            "sqrtf32" => codegen_simple_intrinsic!(Sqrtf),
-            "sqrtf64" => codegen_simple_intrinsic!(Sqrt),
-            "sub_with_overflow" => self.codegen_op_with_overflow(
+            Intrinsic::SimdXor => codegen_intrinsic_binop!(bitxor),
+            Intrinsic::SizeOfVal => codegen_size_align!(size),
+            Intrinsic::SqrtF32 => codegen_simple_intrinsic!(Sqrtf),
+            Intrinsic::SqrtF64 => codegen_simple_intrinsic!(Sqrt),
+            Intrinsic::SubWithOverflow => self.codegen_op_with_overflow(
                 BinaryOperator::OverflowResultMinus,
                 fargs,
                 place,
                 loc,
             ),
-            "transmute" => self.codegen_intrinsic_transmute(fargs, ret_ty, place, loc),
-            "truncf32" => codegen_simple_intrinsic!(Truncf),
-            "truncf64" => codegen_simple_intrinsic!(Trunc),
-            "type_id" => codegen_intrinsic_const!(),
-            "type_name" => codegen_intrinsic_const!(),
-            "typed_swap" => self.codegen_swap(fargs, farg_types, loc),
-            "unaligned_volatile_load" => {
+            Intrinsic::Transmute => self.codegen_intrinsic_transmute(fargs, ret_ty, place, loc),
+            Intrinsic::TruncF32 => codegen_simple_intrinsic!(Truncf),
+            Intrinsic::TruncF64 => codegen_simple_intrinsic!(Trunc),
+            Intrinsic::TypeId => codegen_intrinsic_const!(),
+            Intrinsic::TypeName => codegen_intrinsic_const!(),
+            Intrinsic::TypedSwap => self.codegen_swap(fargs, farg_types, loc),
+            Intrinsic::UnalignedVolatileLoad => {
                 unstable_codegen!(self.codegen_expr_to_place_stable(
                     place,
                     fargs.remove(0).dereference(),
                     loc
                 ))
             }
-            "unchecked_add" | "unchecked_mul" | "unchecked_shl" | "unchecked_shr"
-            | "unchecked_sub" => {
-                unreachable!("Expected intrinsic `{intrinsic}` to be lowered before codegen")
-            }
-            "unchecked_div" => codegen_op_with_div_overflow_check!(div),
-            "unchecked_rem" => codegen_op_with_div_overflow_check!(rem),
-            "unlikely" => self.codegen_expr_to_place_stable(place, fargs.remove(0), loc),
-            "unreachable" => unreachable!(
-                "Expected `std::intrinsics::unreachable` to be handled by `TerminatorKind::Unreachable`"
-            ),
-            "volatile_copy_memory" => unstable_codegen!(codegen_intrinsic_copy!(Memmove)),
-            "volatile_copy_nonoverlapping_memory" => {
+            Intrinsic::UncheckedDiv => codegen_op_with_div_overflow_check!(div),
+            Intrinsic::UncheckedRem => codegen_op_with_div_overflow_check!(rem),
+            Intrinsic::Unlikely => self.codegen_expr_to_place_stable(place, fargs.remove(0), loc),
+            Intrinsic::VolatileCopyMemory => unstable_codegen!(codegen_intrinsic_copy!(Memmove)),
+            Intrinsic::VolatileCopyNonOverlappingMemory => {
                 unstable_codegen!(codegen_intrinsic_copy!(Memcpy))
             }
-            "volatile_load" => self.codegen_volatile_load(fargs, farg_types, place, loc),
-            "volatile_store" => {
+            Intrinsic::VolatileLoad => self.codegen_volatile_load(fargs, farg_types, place, loc),
+            Intrinsic::VolatileStore => {
                 assert!(self.place_ty_stable(place).kind().is_unit());
                 self.codegen_volatile_store(fargs, farg_types, loc)
             }
-            "vtable_size" => self.vtable_info(VTableInfo::Size, fargs, place, loc),
-            "vtable_align" => self.vtable_info(VTableInfo::Align, fargs, place, loc),
-            "wrapping_add" => codegen_wrapping_op!(plus),
-            "wrapping_mul" => codegen_wrapping_op!(mul),
-            "wrapping_sub" => codegen_wrapping_op!(sub),
-            "write_bytes" => {
+            Intrinsic::VtableSize => self.vtable_info(VTableInfo::Size, fargs, place, loc),
+            Intrinsic::VtableAlign => self.vtable_info(VTableInfo::Align, fargs, place, loc),
+            Intrinsic::WrappingAdd => codegen_wrapping_op!(plus),
+            Intrinsic::WrappingMul => codegen_wrapping_op!(mul),
+            Intrinsic::WrappingSub => codegen_wrapping_op!(sub),
+            Intrinsic::WriteBytes => {
                 assert!(self.place_ty_stable(place).kind().is_unit());
                 self.codegen_write_bytes(fargs, farg_types, loc)
             }
             // Unimplemented
-            _ => self.codegen_unimplemented_stmt(
-                intrinsic,
-                loc,
-                "https://github.com/model-checking/kani/issues/new/choose",
-            ),
+            Intrinsic::Unimplemented { name, issue_link } => {
+                self.codegen_unimplemented_stmt(&name, loc, &issue_link)
+            }
         }
     }
 
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index 4883c608f482..a30eeb7639ce 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -1,7 +1,6 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
-use crate::args::ExtraChecks;
 use crate::codegen_cprover_gotoc::codegen::place::ProjectedPlace;
 use crate::codegen_cprover_gotoc::codegen::ty_stable::pointee_type_stable;
 use crate::codegen_cprover_gotoc::codegen::PropertyClass;
@@ -730,18 +729,14 @@ impl<'tcx> GotocCtx<'tcx> {
             Rvalue::Repeat(op, sz) => self.codegen_rvalue_repeat(op, sz, loc),
             Rvalue::Ref(_, _, p) | Rvalue::AddressOf(_, p) => {
                 let place_ref = self.codegen_place_ref_stable(&p, loc);
-                if self.queries.args().ub_check.contains(&ExtraChecks::PtrToRefCast) {
-                    let place_ref_type = place_ref.typ().clone();
-                    match self.codegen_raw_ptr_deref_validity_check(&p, &loc) {
-                        Some(ptr_validity_check_expr) => Expr::statement_expression(
-                            vec![ptr_validity_check_expr, place_ref.as_stmt(loc)],
-                            place_ref_type,
-                            loc,
-                        ),
-                        None => place_ref,
-                    }
-                } else {
-                    place_ref
+                let place_ref_type = place_ref.typ().clone();
+                match self.codegen_raw_ptr_deref_validity_check(&p, &loc) {
+                    Some(ptr_validity_check_expr) => Expr::statement_expression(
+                        vec![ptr_validity_check_expr, place_ref.as_stmt(loc)],
+                        place_ref_type,
+                        loc,
+                    ),
+                    None => place_ref,
                 }
             }
             Rvalue::Len(p) => self.codegen_rvalue_len(p, loc),
diff --git a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
index e360cd491edd..3f17f4b87233 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/context/goto_ctx.rs
@@ -139,17 +139,6 @@ impl<'tcx> GotocCtx<'tcx> {
         sym
     }
 
-    // Generate a Symbol Expression representing a function variable from the MIR
-    pub fn gen_function_local_variable(
-        &mut self,
-        c: u64,
-        fname: &str,
-        t: Type,
-        loc: Location,
-    ) -> Symbol {
-        self.gen_stack_variable(c, fname, "var", t, loc)
-    }
-
     /// Given a counter `c` a function name `fname, and a prefix `prefix`, generates a new function local variable
     /// It is an error to reuse an existing `c`, `fname` `prefix` tuple.
     fn gen_stack_variable(
diff --git a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs
index c290f2bf6428..01f5ca4b3dce 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/utils/names.rs
@@ -45,10 +45,6 @@ impl<'tcx> GotocCtx<'tcx> {
         (name, base_name)
     }
 
-    pub fn initializer_fn_name(var_name: &str) -> String {
-        format!("{var_name}_init")
-    }
-
     /// The name for a tuple field
     pub fn tuple_fld_name(n: usize) -> String {
         format!("{n}")
diff --git a/kani-compiler/src/intrinsics.rs b/kani-compiler/src/intrinsics.rs
new file mode 100644
index 000000000000..9485d8525410
--- /dev/null
+++ b/kani-compiler/src/intrinsics.rs
@@ -0,0 +1,798 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! Single source of truth about which intrinsics we support.
+
+use stable_mir::{
+    mir::{mono::Instance, Mutability},
+    ty::{FloatTy, IntTy, RigidTy, TyKind, UintTy},
+};
+
+// Enumeration of all intrinsics we support right now, with the last option being a catch-all. This
+// way, adding an intrinsic would highlight all places where they are used.
+#[allow(unused)]
+#[derive(Clone, Debug)]
+pub enum Intrinsic {
+    AddWithOverflow,
+    ArithOffset,
+    AssertInhabited,
+    AssertMemUninitializedValid,
+    AssertZeroValid,
+    Assume,
+    AtomicAnd(String),
+    AtomicCxchg(String),
+    AtomicCxchgWeak(String),
+    AtomicFence(String),
+    AtomicLoad(String),
+    AtomicMax(String),
+    AtomicMin(String),
+    AtomicNand(String),
+    AtomicOr(String),
+    AtomicSingleThreadFence(String),
+    AtomicStore(String),
+    AtomicUmax(String),
+    AtomicUmin(String),
+    AtomicXadd(String),
+    AtomicXchg(String),
+    AtomicXor(String),
+    AtomicXsub(String),
+    Bitreverse,
+    BlackBox,
+    Breakpoint,
+    Bswap,
+    CeilF32,
+    CeilF64,
+    CompareBytes,
+    Copy,
+    CopySignF32,
+    CopySignF64,
+    CosF32,
+    CosF64,
+    Ctlz,
+    CtlzNonZero,
+    Ctpop,
+    Cttz,
+    CttzNonZero,
+    DiscriminantValue,
+    ExactDiv,
+    Exp2F32,
+    Exp2F64,
+    ExpF32,
+    ExpF64,
+    FabsF32,
+    FabsF64,
+    FaddFast,
+    FdivFast,
+    FloorF32,
+    FloorF64,
+    FmafF32,
+    FmafF64,
+    FmulFast,
+    Forget,
+    FsubFast,
+    IsValStaticallyKnown,
+    Likely,
+    Log10F32,
+    Log10F64,
+    Log2F32,
+    Log2F64,
+    LogF32,
+    LogF64,
+    MaxNumF32,
+    MaxNumF64,
+    MinAlignOf,
+    MinAlignOfVal,
+    MinNumF32,
+    MinNumF64,
+    MulWithOverflow,
+    NearbyIntF32,
+    NearbyIntF64,
+    NeedsDrop,
+    PowF32,
+    PowF64,
+    PowIF32,
+    PowIF64,
+    PrefAlignOf,
+    PtrGuaranteedCmp,
+    PtrOffsetFrom,
+    PtrOffsetFromUnsigned,
+    RawEq,
+    RetagBoxToRaw,
+    RintF32,
+    RintF64,
+    RotateLeft,
+    RotateRight,
+    RoundF32,
+    RoundF64,
+    SaturatingAdd,
+    SaturatingSub,
+    SinF32,
+    SinF64,
+    SimdAdd,
+    SimdAnd,
+    SimdDiv,
+    SimdRem,
+    SimdEq,
+    SimdExtract,
+    SimdGe,
+    SimdGt,
+    SimdInsert,
+    SimdLe,
+    SimdLt,
+    SimdMul,
+    SimdNe,
+    SimdOr,
+    SimdShl,
+    SimdShr,
+    SimdShuffle(String),
+    SimdSub,
+    SimdXor,
+    SizeOfVal,
+    SqrtF32,
+    SqrtF64,
+    SubWithOverflow,
+    Transmute,
+    TruncF32,
+    TruncF64,
+    TypeId,
+    TypeName,
+    TypedSwap,
+    UnalignedVolatileLoad,
+    UncheckedDiv,
+    UncheckedRem,
+    Unlikely,
+    VolatileCopyMemory,
+    VolatileCopyNonOverlappingMemory,
+    VolatileLoad,
+    VolatileStore,
+    VtableSize,
+    VtableAlign,
+    WrappingAdd,
+    WrappingMul,
+    WrappingSub,
+    WriteBytes,
+    Unimplemented { name: String, issue_link: String },
+}
+
+/// Assert that top-level types of a function signature match the given patterns.
+macro_rules! assert_sig_matches {
+    ($sig:expr, $($input_type:pat),* => $output_type:pat) => {
+        let inputs = $sig.inputs();
+        let output = $sig.output();
+        #[allow(unused_mut)]
+        let mut index = 0;
+        $(
+            #[allow(unused_assignments)]
+            {
+                assert!(matches!(inputs[index].kind(), TyKind::RigidTy($input_type)));
+                index += 1;
+            }
+        )*
+        assert!(inputs.len() == index);
+        assert!(matches!(output.kind(), TyKind::RigidTy($output_type)));
+    }
+}
+
+impl Intrinsic {
+    /// Create an intrinsic enum from a given intrinsic instance, shallowly validating the argument types.
+    pub fn from_instance(intrinsic_instance: &Instance) -> Self {
+        let intrinsic_str = intrinsic_instance.intrinsic_name().unwrap();
+        let sig = intrinsic_instance.ty().kind().fn_sig().unwrap().skip_binder();
+        match intrinsic_str.as_str() {
+            "add_with_overflow" => {
+                assert_sig_matches!(sig, _, _ => RigidTy::Tuple(_));
+                Self::AddWithOverflow
+            }
+            "arith_offset" => {
+                assert_sig_matches!(sig,
+                    RigidTy::RawPtr(_, Mutability::Not),
+                    RigidTy::Int(IntTy::Isize)
+                    => RigidTy::RawPtr(_, Mutability::Not));
+                Self::ArithOffset
+            }
+            "assert_inhabited" => {
+                assert_sig_matches!(sig, => RigidTy::Tuple(_));
+                Self::AssertInhabited
+            }
+            "assert_mem_uninitialized_valid" => {
+                assert_sig_matches!(sig, => RigidTy::Tuple(_));
+                Self::AssertMemUninitializedValid
+            }
+            "assert_zero_valid" => {
+                assert_sig_matches!(sig, => RigidTy::Tuple(_));
+                Self::AssertZeroValid
+            }
+            "assume" => {
+                assert_sig_matches!(sig, RigidTy::Bool => RigidTy::Tuple(_));
+                Self::Assume
+            }
+            "bitreverse" => {
+                assert_sig_matches!(sig, _ => _);
+                Self::Bitreverse
+            }
+            "black_box" => {
+                assert_sig_matches!(sig, _ => _);
+                Self::BlackBox
+            }
+            "breakpoint" => {
+                assert_sig_matches!(sig, => RigidTy::Tuple(_));
+                Self::Breakpoint
+            }
+            "bswap" => {
+                assert_sig_matches!(sig, _ => _);
+                Self::Bswap
+            }
+            "caller_location" => {
+                assert_sig_matches!(sig, => RigidTy::Ref(_, _, Mutability::Not));
+                Self::Unimplemented {
+                    name: intrinsic_str,
+                    issue_link: "https://github.com/model-checking/kani/issues/374".into(),
+                }
+            }
+            "catch_unwind" => {
+                assert_sig_matches!(sig, RigidTy::FnPtr(_), RigidTy::RawPtr(_, Mutability::Mut), RigidTy::FnPtr(_) => RigidTy::Int(IntTy::I32));
+                Self::Unimplemented {
+                    name: intrinsic_str,
+                    issue_link: "https://github.com/model-checking/kani/issues/267".into(),
+                }
+            }
+            "compare_bytes" => {
+                assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not), RigidTy::RawPtr(_, Mutability::Not), RigidTy::Uint(UintTy::Usize) => RigidTy::Int(IntTy::I32));
+                Self::CompareBytes
+            }
+            "copy" => {
+                assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not), RigidTy::RawPtr(_, Mutability::Mut), RigidTy::Uint(UintTy::Usize) => RigidTy::Tuple(_));
+                Self::Copy
+            }
+            "copy_nonoverlapping" => unreachable!(
+                "Expected `core::intrinsics::unreachable` to be handled by `StatementKind::CopyNonOverlapping`"
+            ),
+            "ctlz" => {
+                assert_sig_matches!(sig, _ => RigidTy::Uint(UintTy::U32));
+                Self::Ctlz
+            }
+            "ctlz_nonzero" => {
+                assert_sig_matches!(sig, _ => RigidTy::Uint(UintTy::U32));
+                Self::CtlzNonZero
+            }
+            "ctpop" => {
+                assert_sig_matches!(sig, _ => RigidTy::Uint(UintTy::U32));
+                Self::Ctpop
+            }
+            "cttz" => {
+                assert_sig_matches!(sig, _ => RigidTy::Uint(UintTy::U32));
+                Self::Cttz
+            }
+            "cttz_nonzero" => {
+                assert_sig_matches!(sig, _ => RigidTy::Uint(UintTy::U32));
+                Self::CttzNonZero
+            }
+            "discriminant_value" => {
+                assert_sig_matches!(sig, RigidTy::Ref(_, _, Mutability::Not) => _);
+                Self::DiscriminantValue
+            }
+            "exact_div" => {
+                assert_sig_matches!(sig, _, _ => _);
+                Self::ExactDiv
+            }
+            "fadd_fast" => {
+                assert_sig_matches!(sig, _, _ => _);
+                Self::FaddFast
+            }
+            "fdiv_fast" => {
+                assert_sig_matches!(sig, _, _ => _);
+                Self::FdivFast
+            }
+            "fmul_fast" => {
+                assert_sig_matches!(sig, _, _ => _);
+                Self::FmulFast
+            }
+            "forget" => {
+                assert_sig_matches!(sig, _ => RigidTy::Tuple(_));
+                Self::Forget
+            }
+            "fsub_fast" => {
+                assert_sig_matches!(sig, _, _ => _);
+                Self::FsubFast
+            }
+            "is_val_statically_known" => {
+                assert_sig_matches!(sig, _ => RigidTy::Bool);
+                Self::IsValStaticallyKnown
+            }
+            "likely" => {
+                assert_sig_matches!(sig, RigidTy::Bool => RigidTy::Bool);
+                Self::Likely
+            }
+            "min_align_of" => {
+                assert_sig_matches!(sig, => RigidTy::Uint(UintTy::Usize));
+                Self::MinAlignOf
+            }
+            "min_align_of_val" => {
+                assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => RigidTy::Uint(UintTy::Usize));
+                Self::MinAlignOfVal
+            }
+            "mul_with_overflow" => {
+                assert_sig_matches!(sig, _, _ => RigidTy::Tuple(_));
+                Self::MulWithOverflow
+            }
+            "needs_drop" => {
+                assert_sig_matches!(sig, => RigidTy::Bool);
+                Self::NeedsDrop
+            }
+            // As of https://github.com/rust-lang/rust/pull/110822 the `offset` intrinsic is lowered to `mir::BinOp::Offset`
+            "offset" => unreachable!(
+                "Expected `core::intrinsics::unreachable` to be handled by `BinOp::OffSet`"
+            ),
+            "pref_align_of" => {
+                assert_sig_matches!(sig, => RigidTy::Uint(UintTy::Usize));
+                Self::PrefAlignOf
+            }
+            "ptr_guaranteed_cmp" => {
+                assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not), RigidTy::RawPtr(_, Mutability::Not) => RigidTy::Uint(UintTy::U8));
+                Self::PtrGuaranteedCmp
+            }
+            "ptr_offset_from" => {
+                assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not), RigidTy::RawPtr(_, Mutability::Not) => RigidTy::Int(IntTy::Isize));
+                Self::PtrOffsetFrom
+            }
+            "ptr_offset_from_unsigned" => {
+                assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not), RigidTy::RawPtr(_, Mutability::Not) => RigidTy::Uint(UintTy::Usize));
+                Self::PtrOffsetFromUnsigned
+            }
+            "raw_eq" => {
+                assert_sig_matches!(sig, RigidTy::Ref(_, _, Mutability::Not), RigidTy::Ref(_, _, Mutability::Not) => RigidTy::Bool);
+                Self::RawEq
+            }
+            "rotate_left" => {
+                assert_sig_matches!(sig, _, RigidTy::Uint(UintTy::U32) => _);
+                Self::RotateLeft
+            }
+            "rotate_right" => {
+                assert_sig_matches!(sig, _, RigidTy::Uint(UintTy::U32) => _);
+                Self::RotateRight
+            }
+            "saturating_add" => {
+                assert_sig_matches!(sig, _, _ => _);
+                Self::SaturatingAdd
+            }
+            "saturating_sub" => {
+                assert_sig_matches!(sig, _, _ => _);
+                Self::SaturatingSub
+            }
+            "size_of" => unreachable!(),
+            "size_of_val" => {
+                assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => RigidTy::Uint(UintTy::Usize));
+                Self::SizeOfVal
+            }
+            "sub_with_overflow" => {
+                assert_sig_matches!(sig, _, _ => RigidTy::Tuple(_));
+                Self::SubWithOverflow
+            }
+            "transmute" => {
+                assert_sig_matches!(sig, _ => _);
+                Self::Transmute
+            }
+            "type_id" => {
+                assert_sig_matches!(sig, => RigidTy::Uint(UintTy::U128));
+                Self::TypeId
+            }
+            "type_name" => {
+                assert_sig_matches!(sig, => RigidTy::Ref(_, _, Mutability::Not));
+                Self::TypeName
+            }
+            "typed_swap" => {
+                assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), RigidTy::RawPtr(_, Mutability::Mut) => RigidTy::Tuple(_));
+                Self::TypedSwap
+            }
+            "unaligned_volatile_load" => {
+                assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => _);
+                Self::UnalignedVolatileLoad
+            }
+            "unchecked_add" | "unchecked_mul" | "unchecked_shl" | "unchecked_shr"
+            | "unchecked_sub" => {
+                unreachable!("Expected intrinsic `{intrinsic_str}` to be lowered before codegen")
+            }
+            "unchecked_div" => {
+                assert_sig_matches!(sig, _, _ => _);
+                Self::UncheckedDiv
+            }
+            "unchecked_rem" => {
+                assert_sig_matches!(sig, _, _ => _);
+                Self::UncheckedRem
+            }
+            "unlikely" => {
+                assert_sig_matches!(sig, RigidTy::Bool => RigidTy::Bool);
+                Self::Unlikely
+            }
+            "unreachable" => unreachable!(
+                "Expected `std::intrinsics::unreachable` to be handled by `TerminatorKind::Unreachable`"
+            ),
+            "volatile_copy_memory" => {
+                assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), RigidTy::RawPtr(_, Mutability::Not), RigidTy::Uint(UintTy::Usize) => RigidTy::Tuple(_));
+                Self::VolatileCopyMemory
+            }
+            "volatile_copy_nonoverlapping_memory" => {
+                assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), RigidTy::RawPtr(_, Mutability::Not), RigidTy::Uint(UintTy::Usize) => RigidTy::Tuple(_));
+                Self::VolatileCopyNonOverlappingMemory
+            }
+            "volatile_load" => {
+                assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => _);
+                Self::VolatileLoad
+            }
+            "volatile_store" => {
+                assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => RigidTy::Tuple(_));
+                Self::VolatileStore
+            }
+            "vtable_size" => {
+                assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => RigidTy::Uint(UintTy::Usize));
+                Self::VtableSize
+            }
+            "vtable_align" => {
+                assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => RigidTy::Uint(UintTy::Usize));
+                Self::VtableAlign
+            }
+            "wrapping_add" => {
+                assert_sig_matches!(sig, _, _ => _);
+                Self::WrappingAdd
+            }
+            "wrapping_mul" => {
+                assert_sig_matches!(sig, _, _ => _);
+                Self::WrappingMul
+            }
+            "wrapping_sub" => {
+                assert_sig_matches!(sig, _, _ => _);
+                Self::WrappingSub
+            }
+            "write_bytes" => {
+                assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), RigidTy::Uint(UintTy::U8), RigidTy::Uint(UintTy::Usize) => RigidTy::Tuple(_));
+                Self::WriteBytes
+            }
+            _ => try_match_atomic(intrinsic_instance)
+                .or_else(|| try_match_simd(intrinsic_instance))
+                .or_else(|| try_match_f32(intrinsic_instance))
+                .or_else(|| try_match_f64(intrinsic_instance))
+                .unwrap_or(Self::Unimplemented {
+                    name: intrinsic_str,
+                    issue_link: "https://github.com/model-checking/kani/issues/new/choose".into(),
+                }),
+        }
+    }
+}
+
+/// Match atomic intrinsics by instance, returning an instance of the intrinsics enum if the match
+/// is successful.
+fn try_match_atomic(intrinsic_instance: &Instance) -> Option<Intrinsic> {
+    let intrinsic_str = intrinsic_instance.intrinsic_name().unwrap();
+    let sig = intrinsic_instance.ty().kind().fn_sig().unwrap().skip_binder();
+    if let Some(suffix) = intrinsic_str.strip_prefix("atomic_and_") {
+        assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
+        Some(Intrinsic::AtomicAnd(suffix.into()))
+    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_cxchgweak_") {
+        assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _, _ => RigidTy::Tuple(_));
+        Some(Intrinsic::AtomicCxchgWeak(suffix.into()))
+    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_cxchg_") {
+        assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _, _ => RigidTy::Tuple(_));
+        Some(Intrinsic::AtomicCxchg(suffix.into()))
+    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_fence_") {
+        assert_sig_matches!(sig, => RigidTy::Tuple(_));
+        Some(Intrinsic::AtomicFence(suffix.into()))
+    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_load_") {
+        assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => _);
+        Some(Intrinsic::AtomicLoad(suffix.into()))
+    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_max_") {
+        assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
+        Some(Intrinsic::AtomicMax(suffix.into()))
+    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_min_") {
+        assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
+        Some(Intrinsic::AtomicMin(suffix.into()))
+    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_nand_") {
+        assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
+        Some(Intrinsic::AtomicNand(suffix.into()))
+    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_or_") {
+        assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
+        Some(Intrinsic::AtomicOr(suffix.into()))
+    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_singlethreadfence_") {
+        assert_sig_matches!(sig, => RigidTy::Tuple(_));
+        Some(Intrinsic::AtomicSingleThreadFence(suffix.into()))
+    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_store_") {
+        assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => RigidTy::Tuple(_));
+        Some(Intrinsic::AtomicStore(suffix.into()))
+    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_umax_") {
+        assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
+        Some(Intrinsic::AtomicUmax(suffix.into()))
+    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_umin_") {
+        assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
+        Some(Intrinsic::AtomicUmin(suffix.into()))
+    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xadd_") {
+        assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
+        Some(Intrinsic::AtomicXadd(suffix.into()))
+    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xchg_") {
+        assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
+        Some(Intrinsic::AtomicXchg(suffix.into()))
+    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xor_") {
+        assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
+        Some(Intrinsic::AtomicXor(suffix.into()))
+    } else if let Some(suffix) = intrinsic_str.strip_prefix("atomic_xsub_") {
+        assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => _);
+        Some(Intrinsic::AtomicXsub(suffix.into()))
+    } else {
+        None
+    }
+}
+
+/// Match SIMD intrinsics by instance, returning an instance of the intrinsics enum if the match
+/// is successful.
+fn try_match_simd(intrinsic_instance: &Instance) -> Option<Intrinsic> {
+    let intrinsic_str = intrinsic_instance.intrinsic_name().unwrap();
+    let sig = intrinsic_instance.ty().kind().fn_sig().unwrap().skip_binder();
+    match intrinsic_str.as_str() {
+        "simd_add" => {
+            assert_sig_matches!(sig, _, _ => _);
+            Some(Intrinsic::SimdAdd)
+        }
+        "simd_and" => {
+            assert_sig_matches!(sig, _, _ => _);
+            Some(Intrinsic::SimdAnd)
+        }
+        "simd_div" => {
+            assert_sig_matches!(sig, _, _ => _);
+            Some(Intrinsic::SimdDiv)
+        }
+        "simd_rem" => {
+            assert_sig_matches!(sig, _, _ => _);
+            Some(Intrinsic::SimdRem)
+        }
+        "simd_eq" => {
+            assert_sig_matches!(sig, _, _ => _);
+            Some(Intrinsic::SimdEq)
+        }
+        "simd_extract" => {
+            assert_sig_matches!(sig, _, RigidTy::Uint(UintTy::U32) => _);
+            Some(Intrinsic::SimdExtract)
+        }
+        "simd_ge" => {
+            assert_sig_matches!(sig, _, _ => _);
+            Some(Intrinsic::SimdGe)
+        }
+        "simd_gt" => {
+            assert_sig_matches!(sig, _, _ => _);
+            Some(Intrinsic::SimdGt)
+        }
+        "simd_insert" => {
+            assert_sig_matches!(sig, _, RigidTy::Uint(UintTy::U32), _ => _);
+            Some(Intrinsic::SimdInsert)
+        }
+        "simd_le" => {
+            assert_sig_matches!(sig, _, _ => _);
+            Some(Intrinsic::SimdLe)
+        }
+        "simd_lt" => {
+            assert_sig_matches!(sig, _, _ => _);
+            Some(Intrinsic::SimdLt)
+        }
+        "simd_mul" => {
+            assert_sig_matches!(sig, _, _ => _);
+            Some(Intrinsic::SimdMul)
+        }
+        "simd_ne" => {
+            assert_sig_matches!(sig, _, _ => _);
+            Some(Intrinsic::SimdNe)
+        }
+        "simd_or" => {
+            assert_sig_matches!(sig, _, _ => _);
+            Some(Intrinsic::SimdOr)
+        }
+        "simd_shl" => {
+            assert_sig_matches!(sig, _, _ => _);
+            Some(Intrinsic::SimdShl)
+        }
+        "simd_shr" => {
+            assert_sig_matches!(sig, _, _ => _);
+            Some(Intrinsic::SimdShr)
+        }
+        "simd_sub" => {
+            assert_sig_matches!(sig, _, _ => _);
+            Some(Intrinsic::SimdSub)
+        }
+        "simd_xor" => {
+            assert_sig_matches!(sig, _, _ => _);
+            Some(Intrinsic::SimdXor)
+        }
+        name => {
+            if let Some(suffix) = name.strip_prefix("simd_shuffle") {
+                assert_sig_matches!(sig, _, _, _ => _);
+                Some(Intrinsic::SimdShuffle(suffix.into()))
+            } else {
+                None
+            }
+        }
+    }
+}
+
+/// Match f32 arithmetic intrinsics by instance, returning an instance of the intrinsics enum if the match
+/// is successful.
+fn try_match_f32(intrinsic_instance: &Instance) -> Option<Intrinsic> {
+    let intrinsic_str = intrinsic_instance.intrinsic_name().unwrap();
+    let sig = intrinsic_instance.ty().kind().fn_sig().unwrap().skip_binder();
+    match intrinsic_str.as_str() {
+        "ceilf32" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
+            Some(Intrinsic::CeilF32)
+        }
+        "copysignf32" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32), RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
+            Some(Intrinsic::CopySignF32)
+        }
+        "cosf32" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
+            Some(Intrinsic::CosF32)
+        }
+        "exp2f32" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
+            Some(Intrinsic::Exp2F32)
+        }
+        "expf32" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
+            Some(Intrinsic::ExpF32)
+        }
+        "fabsf32" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
+            Some(Intrinsic::FabsF32)
+        }
+        "floorf32" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
+            Some(Intrinsic::FloorF32)
+        }
+        "fmaf32" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32), RigidTy::Float(FloatTy::F32), RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
+            Some(Intrinsic::FmafF32)
+        }
+        "log10f32" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
+            Some(Intrinsic::Log10F32)
+        }
+        "log2f32" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
+            Some(Intrinsic::Log2F32)
+        }
+        "logf32" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
+            Some(Intrinsic::LogF32)
+        }
+        "maxnumf32" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32), RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
+            Some(Intrinsic::MaxNumF32)
+        }
+        "minnumf32" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32), RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
+            Some(Intrinsic::MinNumF32)
+        }
+        "nearbyintf32" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
+            Some(Intrinsic::NearbyIntF32)
+        }
+        "powf32" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32), RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
+            Some(Intrinsic::PowF32)
+        }
+        "powif32" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32), RigidTy::Int(IntTy::I32) => RigidTy::Float(FloatTy::F32));
+            Some(Intrinsic::PowIF32)
+        }
+        "rintf32" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
+            Some(Intrinsic::RintF32)
+        }
+        "roundf32" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
+            Some(Intrinsic::RoundF32)
+        }
+        "sinf32" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
+            Some(Intrinsic::SinF32)
+        }
+        "sqrtf32" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
+            Some(Intrinsic::SqrtF32)
+        }
+        "truncf32" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F32) => RigidTy::Float(FloatTy::F32));
+            Some(Intrinsic::TruncF32)
+        }
+        _ => None,
+    }
+}
+
+/// Match f64 arithmetic intrinsics by instance, returning an instance of the intrinsics enum if the match
+/// is successful.
+fn try_match_f64(intrinsic_instance: &Instance) -> Option<Intrinsic> {
+    let intrinsic_str = intrinsic_instance.intrinsic_name().unwrap();
+    let sig = intrinsic_instance.ty().kind().fn_sig().unwrap().skip_binder();
+    match intrinsic_str.as_str() {
+        "ceilf64" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
+            Some(Intrinsic::CeilF64)
+        }
+        "copysignf64" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64), RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
+            Some(Intrinsic::CopySignF64)
+        }
+        "cosf64" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
+            Some(Intrinsic::CosF64)
+        }
+        "exp2f64" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
+            Some(Intrinsic::Exp2F64)
+        }
+        "expf64" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
+            Some(Intrinsic::ExpF64)
+        }
+        "fabsf64" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
+            Some(Intrinsic::FabsF64)
+        }
+        "floorf64" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
+            Some(Intrinsic::FloorF64)
+        }
+        "fmaf64" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64), RigidTy::Float(FloatTy::F64), RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
+            Some(Intrinsic::FmafF64)
+        }
+        "log10f64" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
+            Some(Intrinsic::Log10F64)
+        }
+        "log2f64" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
+            Some(Intrinsic::Log2F64)
+        }
+        "logf64" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
+            Some(Intrinsic::LogF64)
+        }
+        "maxnumf64" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64), RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
+            Some(Intrinsic::MaxNumF64)
+        }
+        "minnumf64" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64), RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
+            Some(Intrinsic::MinNumF64)
+        }
+        "nearbyintf64" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
+            Some(Intrinsic::NearbyIntF64)
+        }
+        "powf64" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64), RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
+            Some(Intrinsic::PowF64)
+        }
+        "powif64" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64), RigidTy::Int(IntTy::I32) => RigidTy::Float(FloatTy::F64));
+            Some(Intrinsic::PowIF64)
+        }
+        "rintf64" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
+            Some(Intrinsic::RintF64)
+        }
+        "roundf64" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
+            Some(Intrinsic::RoundF64)
+        }
+        "sinf64" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
+            Some(Intrinsic::SinF64)
+        }
+        "sqrtf64" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
+            Some(Intrinsic::SqrtF64)
+        }
+        "truncf64" => {
+            assert_sig_matches!(sig, RigidTy::Float(FloatTy::F64) => RigidTy::Float(FloatTy::F64));
+            Some(Intrinsic::TruncF64)
+        }
+        _ => None,
+    }
+}
diff --git a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs
index 640318ccb584..15593549b690 100644
--- a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs
+++ b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs
@@ -24,12 +24,14 @@
 //! Currently, the analysis is not field-sensitive: e.g., if a field of a place aliases to some
 //! other place, we treat it as if the place itself aliases to another place.
 
-use crate::kani_middle::{
-    points_to::{MemLoc, PointsToGraph},
-    reachability::CallGraph,
-    transform::RustcInternalMir,
+use crate::{
+    intrinsics::Intrinsic,
+    kani_middle::{
+        points_to::{MemLoc, PointsToGraph},
+        reachability::CallGraph,
+        transform::RustcInternalMir,
+    },
 };
-use rustc_ast::Mutability;
 use rustc_middle::{
     mir::{
         BasicBlock, BinOp, Body, CallReturnPlaces, Location, NonDivergingIntrinsic, Operand, Place,
@@ -202,161 +204,117 @@ impl<'a, 'tcx> Analysis<'tcx> for PointsToAnalysis<'a, 'tcx> {
             match instance.def {
                 // Intrinsics could introduce aliasing edges we care about, so need to handle them.
                 InstanceKind::Intrinsic(def_id) => {
-                    match self.tcx.intrinsic(def_id).unwrap().name.to_string().as_str() {
-                        name if name.starts_with("atomic") => {
-                            match name {
-                                // All `atomic_cxchg` intrinsics take `dst, old, src` as arguments.
-                                // This is equivalent to `destination = *dst; *dst = src`.
-                                name if name.starts_with("atomic_cxchg") => {
-                                    assert_eq!(
-                                        args.len(),
-                                        3,
-                                        "Unexpected number of arguments for `{name}`"
-                                    );
-                                    assert!(matches!(
-                                        args[0].node.ty(self.body, self.tcx).kind(),
-                                        TyKind::RawPtr(_, Mutability::Mut)
-                                    ));
-                                    let src_set =
-                                        self.successors_for_operand(state, args[2].node.clone());
-                                    let dst_set =
-                                        self.successors_for_deref(state, args[0].node.clone());
-                                    let destination_set =
-                                        state.resolve_place(*destination, self.instance);
-                                    state.extend(&destination_set, &state.successors(&dst_set));
-                                    state.extend(&dst_set, &src_set);
-                                }
-                                // All `atomic_load` intrinsics take `src` as an argument.
-                                // This is equivalent to `destination = *src`.
-                                name if name.starts_with("atomic_load") => {
-                                    assert_eq!(
-                                        args.len(),
-                                        1,
-                                        "Unexpected number of arguments for `{name}`"
-                                    );
-                                    assert!(matches!(
-                                        args[0].node.ty(self.body, self.tcx).kind(),
-                                        TyKind::RawPtr(_, Mutability::Not)
-                                    ));
-                                    let src_set =
-                                        self.successors_for_deref(state, args[0].node.clone());
-                                    let destination_set =
-                                        state.resolve_place(*destination, self.instance);
-                                    state.extend(&destination_set, &state.successors(&src_set));
-                                }
-                                // All `atomic_store` intrinsics take `dst, val` as arguments.
-                                // This is equivalent to `*dst = val`.
-                                name if name.starts_with("atomic_store") => {
-                                    assert_eq!(
-                                        args.len(),
-                                        2,
-                                        "Unexpected number of arguments for `{name}`"
-                                    );
-                                    assert!(matches!(
-                                        args[0].node.ty(self.body, self.tcx).kind(),
-                                        TyKind::RawPtr(_, Mutability::Mut)
-                                    ));
-                                    let dst_set =
-                                        self.successors_for_deref(state, args[0].node.clone());
-                                    let val_set =
-                                        self.successors_for_operand(state, args[1].node.clone());
-                                    state.extend(&dst_set, &val_set);
-                                }
-                                // All other `atomic` intrinsics take `dst, src` as arguments.
-                                // This is equivalent to `destination = *dst; *dst = src`.
-                                _ => {
-                                    assert_eq!(
-                                        args.len(),
-                                        2,
-                                        "Unexpected number of arguments for `{name}`"
-                                    );
-                                    assert!(matches!(
-                                        args[0].node.ty(self.body, self.tcx).kind(),
-                                        TyKind::RawPtr(_, Mutability::Mut)
-                                    ));
-                                    let src_set =
-                                        self.successors_for_operand(state, args[1].node.clone());
-                                    let dst_set =
-                                        self.successors_for_deref(state, args[0].node.clone());
-                                    let destination_set =
-                                        state.resolve_place(*destination, self.instance);
-                                    state.extend(&destination_set, &state.successors(&dst_set));
-                                    state.extend(&dst_set, &src_set);
-                                }
-                            };
-                        }
-                        // Similar to `copy_nonoverlapping`, argument order is `src`, `dst`, `count`.
-                        "copy" => {
-                            assert_eq!(args.len(), 3, "Unexpected number of arguments for `copy`");
-                            assert!(matches!(
-                                args[0].node.ty(self.body, self.tcx).kind(),
-                                TyKind::RawPtr(_, Mutability::Not)
-                            ));
-                            assert!(matches!(
-                                args[1].node.ty(self.body, self.tcx).kind(),
-                                TyKind::RawPtr(_, Mutability::Mut)
-                            ));
-                            self.apply_copy_effect(
-                                state,
-                                args[0].node.clone(),
-                                args[1].node.clone(),
-                            );
-                        }
-                        // Similar to `copy_nonoverlapping`, argument order is `dst`, `src`, `count`.
-                        "volatile_copy_memory" | "volatile_copy_nonoverlapping_memory" => {
-                            assert_eq!(args.len(), 3, "Unexpected number of arguments for `copy`");
-                            assert!(matches!(
-                                args[0].node.ty(self.body, self.tcx).kind(),
-                                TyKind::RawPtr(_, Mutability::Mut)
-                            ));
-                            assert!(matches!(
-                                args[1].node.ty(self.body, self.tcx).kind(),
-                                TyKind::RawPtr(_, Mutability::Not)
-                            ));
-                            self.apply_copy_effect(
-                                state,
-                                args[1].node.clone(),
-                                args[0].node.clone(),
-                            );
-                        }
-                        // Semantically equivalent to dest = *a
-                        "volatile_load" | "unaligned_volatile_load" => {
-                            assert_eq!(
-                                args.len(),
-                                1,
-                                "Unexpected number of arguments for `volatile_load`"
-                            );
-                            assert!(matches!(
-                                args[0].node.ty(self.body, self.tcx).kind(),
-                                TyKind::RawPtr(_, Mutability::Not)
-                            ));
-                            // Destination of the return value.
-                            let lvalue_set = state.resolve_place(*destination, self.instance);
-                            let rvalue_set = self.successors_for_deref(state, args[0].node.clone());
-                            state.extend(&lvalue_set, &state.successors(&rvalue_set));
-                        }
-                        // Semantically equivalent *a = b.
-                        "volatile_store" | "unaligned_volatile_store" => {
-                            assert_eq!(
-                                args.len(),
-                                2,
-                                "Unexpected number of arguments for `volatile_store`"
-                            );
-                            assert!(matches!(
-                                args[0].node.ty(self.body, self.tcx).kind(),
-                                TyKind::RawPtr(_, Mutability::Mut)
-                            ));
-                            let lvalue_set = self.successors_for_deref(state, args[0].node.clone());
-                            let rvalue_set =
-                                self.successors_for_operand(state, args[1].node.clone());
-                            state.extend(&lvalue_set, &rvalue_set);
-                        }
-                        _ => {
-                            // TODO: this probably does not handle all relevant intrinsics, so more
-                            // need to be added. For more information, see:
-                            // https://github.com/model-checking/kani/issues/3300
-                            if self.tcx.is_mir_available(def_id) {
-                                self.apply_regular_call_effect(state, instance, args, destination);
+                    // Check if the intrinsic has a body we can analyze.
+                    if self.tcx.is_mir_available(def_id) {
+                        self.apply_regular_call_effect(state, instance, args, destination);
+                    } else {
+                        // Check all of the other intrinsics.
+                        match Intrinsic::from_instance(&rustc_internal::stable(instance)) {
+                            intrinsic if is_identity_aliasing_intrinsic(intrinsic.clone()) => {
+                                // Treat the intrinsic as an aggregate, taking a union of all of the
+                                // arguments' aliases.
+                                let destination_set =
+                                    state.resolve_place(*destination, self.instance);
+                                let operands_set = args
+                                    .into_iter()
+                                    .flat_map(|operand| {
+                                        self.successors_for_operand(state, operand.node.clone())
+                                    })
+                                    .collect();
+                                state.extend(&destination_set, &operands_set);
+                            }
+                            // All `atomic_cxchg` intrinsics take `dst, old, src` as arguments.
+                            // This is equivalent to `destination = *dst; *dst = src`.
+                            Intrinsic::AtomicCxchg(_) | Intrinsic::AtomicCxchgWeak(_) => {
+                                let src_set =
+                                    self.successors_for_operand(state, args[2].node.clone());
+                                let dst_set =
+                                    self.successors_for_deref(state, args[0].node.clone());
+                                let destination_set =
+                                    state.resolve_place(*destination, self.instance);
+                                state.extend(&destination_set, &state.successors(&dst_set));
+                                state.extend(&dst_set, &src_set);
+                            }
+                            // All `atomic_load` intrinsics take `src` as an argument.
+                            // This is equivalent to `destination = *src`.
+                            Intrinsic::AtomicLoad(_) => {
+                                let src_set =
+                                    self.successors_for_deref(state, args[0].node.clone());
+                                let destination_set =
+                                    state.resolve_place(*destination, self.instance);
+                                state.extend(&destination_set, &state.successors(&src_set));
+                            }
+                            // All `atomic_store` intrinsics take `dst, val` as arguments.
+                            // This is equivalent to `*dst = val`.
+                            Intrinsic::AtomicStore(_) => {
+                                let dst_set =
+                                    self.successors_for_deref(state, args[0].node.clone());
+                                let val_set =
+                                    self.successors_for_operand(state, args[1].node.clone());
+                                state.extend(&dst_set, &val_set);
+                            }
+                            // All other `atomic` intrinsics take `dst, src` as arguments.
+                            // This is equivalent to `destination = *dst; *dst = src`.
+                            Intrinsic::AtomicAnd(_)
+                            | Intrinsic::AtomicMax(_)
+                            | Intrinsic::AtomicMin(_)
+                            | Intrinsic::AtomicNand(_)
+                            | Intrinsic::AtomicOr(_)
+                            | Intrinsic::AtomicUmax(_)
+                            | Intrinsic::AtomicUmin(_)
+                            | Intrinsic::AtomicXadd(_)
+                            | Intrinsic::AtomicXchg(_)
+                            | Intrinsic::AtomicXor(_)
+                            | Intrinsic::AtomicXsub(_) => {
+                                let src_set =
+                                    self.successors_for_operand(state, args[1].node.clone());
+                                let dst_set =
+                                    self.successors_for_deref(state, args[0].node.clone());
+                                let destination_set =
+                                    state.resolve_place(*destination, self.instance);
+                                state.extend(&destination_set, &state.successors(&dst_set));
+                                state.extend(&dst_set, &src_set);
+                            }
+                            // Similar to `copy_nonoverlapping`, argument order is `src`, `dst`, `count`.
+                            Intrinsic::Copy => {
+                                self.apply_copy_effect(
+                                    state,
+                                    args[0].node.clone(),
+                                    args[1].node.clone(),
+                                );
+                            }
+                            // Similar to `copy_nonoverlapping`, argument order is `dst`, `src`, `count`.
+                            Intrinsic::VolatileCopyMemory
+                            | Intrinsic::VolatileCopyNonOverlappingMemory => {
+                                self.apply_copy_effect(
+                                    state,
+                                    args[1].node.clone(),
+                                    args[0].node.clone(),
+                                );
+                            }
+                            // Semantically equivalent to dest = *a
+                            Intrinsic::VolatileLoad | Intrinsic::UnalignedVolatileLoad => {
+                                // Destination of the return value.
+                                let lvalue_set = state.resolve_place(*destination, self.instance);
+                                let rvalue_set =
+                                    self.successors_for_deref(state, args[0].node.clone());
+                                state.extend(&lvalue_set, &state.successors(&rvalue_set));
+                            }
+                            // Semantically equivalent *a = b.
+                            Intrinsic::VolatileStore => {
+                                let lvalue_set =
+                                    self.successors_for_deref(state, args[0].node.clone());
+                                let rvalue_set =
+                                    self.successors_for_operand(state, args[1].node.clone());
+                                state.extend(&lvalue_set, &rvalue_set);
+                            }
+                            Intrinsic::Unimplemented { .. } => {
+                                // This will be taken care of at the codegen level.
+                            }
+                            intrinsic => {
+                                unimplemented!(
+                                    "Kani does not support reasoning about aliasing in presence of intrinsic `{intrinsic:?}`. For more information about the state of uninitialized memory checks implementation, see: https://github.com/model-checking/kani/issues/3300."
+                                );
                             }
                         }
                     }
@@ -652,3 +610,136 @@ impl<'a, 'tcx> PointsToAnalysis<'a, 'tcx> {
         }
     }
 }
+
+/// Determines if the intrinsic does not influence aliasing beyond being treated as an identity
+/// function (i.e. propagate aliasing without changes).
+fn is_identity_aliasing_intrinsic(intrinsic: Intrinsic) -> bool {
+    match intrinsic {
+        Intrinsic::AddWithOverflow
+        | Intrinsic::ArithOffset
+        | Intrinsic::AssertInhabited
+        | Intrinsic::AssertMemUninitializedValid
+        | Intrinsic::AssertZeroValid
+        | Intrinsic::Assume
+        | Intrinsic::Bitreverse
+        | Intrinsic::BlackBox
+        | Intrinsic::Breakpoint
+        | Intrinsic::Bswap
+        | Intrinsic::CeilF32
+        | Intrinsic::CeilF64
+        | Intrinsic::CompareBytes
+        | Intrinsic::CopySignF32
+        | Intrinsic::CopySignF64
+        | Intrinsic::CosF32
+        | Intrinsic::CosF64
+        | Intrinsic::Ctlz
+        | Intrinsic::CtlzNonZero
+        | Intrinsic::Ctpop
+        | Intrinsic::Cttz
+        | Intrinsic::CttzNonZero
+        | Intrinsic::DiscriminantValue
+        | Intrinsic::ExactDiv
+        | Intrinsic::Exp2F32
+        | Intrinsic::Exp2F64
+        | Intrinsic::ExpF32
+        | Intrinsic::ExpF64
+        | Intrinsic::FabsF32
+        | Intrinsic::FabsF64
+        | Intrinsic::FaddFast
+        | Intrinsic::FdivFast
+        | Intrinsic::FloorF32
+        | Intrinsic::FloorF64
+        | Intrinsic::FmafF32
+        | Intrinsic::FmafF64
+        | Intrinsic::FmulFast
+        | Intrinsic::Forget
+        | Intrinsic::FsubFast
+        | Intrinsic::IsValStaticallyKnown
+        | Intrinsic::Likely
+        | Intrinsic::Log10F32
+        | Intrinsic::Log10F64
+        | Intrinsic::Log2F32
+        | Intrinsic::Log2F64
+        | Intrinsic::LogF32
+        | Intrinsic::LogF64
+        | Intrinsic::MaxNumF32
+        | Intrinsic::MaxNumF64
+        | Intrinsic::MinAlignOf
+        | Intrinsic::MinAlignOfVal
+        | Intrinsic::MinNumF32
+        | Intrinsic::MinNumF64
+        | Intrinsic::MulWithOverflow
+        | Intrinsic::NearbyIntF32
+        | Intrinsic::NearbyIntF64
+        | Intrinsic::NeedsDrop
+        | Intrinsic::PowF32
+        | Intrinsic::PowF64
+        | Intrinsic::PowIF32
+        | Intrinsic::PowIF64
+        | Intrinsic::PrefAlignOf
+        | Intrinsic::PtrGuaranteedCmp
+        | Intrinsic::PtrOffsetFrom
+        | Intrinsic::PtrOffsetFromUnsigned
+        | Intrinsic::RawEq
+        | Intrinsic::RintF32
+        | Intrinsic::RintF64
+        | Intrinsic::RotateLeft
+        | Intrinsic::RotateRight
+        | Intrinsic::RoundF32
+        | Intrinsic::RoundF64
+        | Intrinsic::SaturatingAdd
+        | Intrinsic::SaturatingSub
+        | Intrinsic::SinF32
+        | Intrinsic::SinF64
+        | Intrinsic::SizeOfVal
+        | Intrinsic::SqrtF32
+        | Intrinsic::SqrtF64
+        | Intrinsic::SubWithOverflow
+        | Intrinsic::TruncF32
+        | Intrinsic::TruncF64
+        | Intrinsic::TypeId
+        | Intrinsic::TypeName
+        | Intrinsic::UncheckedDiv
+        | Intrinsic::UncheckedRem
+        | Intrinsic::Unlikely
+        | Intrinsic::VtableSize
+        | Intrinsic::VtableAlign
+        | Intrinsic::WrappingAdd
+        | Intrinsic::WrappingMul
+        | Intrinsic::WrappingSub
+        | Intrinsic::WriteBytes => {
+            /* Intrinsics that do not interact with aliasing beyond propagating it. */
+            true
+        }
+        Intrinsic::SimdAdd
+        | Intrinsic::SimdAnd
+        | Intrinsic::SimdDiv
+        | Intrinsic::SimdRem
+        | Intrinsic::SimdEq
+        | Intrinsic::SimdExtract
+        | Intrinsic::SimdGe
+        | Intrinsic::SimdGt
+        | Intrinsic::SimdInsert
+        | Intrinsic::SimdLe
+        | Intrinsic::SimdLt
+        | Intrinsic::SimdMul
+        | Intrinsic::SimdNe
+        | Intrinsic::SimdOr
+        | Intrinsic::SimdShl
+        | Intrinsic::SimdShr
+        | Intrinsic::SimdShuffle(_)
+        | Intrinsic::SimdSub
+        | Intrinsic::SimdXor => {
+            /* SIMD operations */
+            true
+        }
+        Intrinsic::AtomicFence(_) | Intrinsic::AtomicSingleThreadFence(_) => {
+            /* Atomic fences */
+            true
+        }
+        _ => {
+            /* Everything else */
+            false
+        }
+    }
+}
diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs
index 3d110c4e9656..fa4e5eb1ad97 100644
--- a/kani-compiler/src/kani_middle/transform/body.rs
+++ b/kani-compiler/src/kani_middle/transform/body.rs
@@ -54,6 +54,7 @@ impl MutableBody {
         &self.locals
     }
 
+    #[allow(dead_code)]
     pub fn arg_count(&self) -> usize {
         self.arg_count
     }
@@ -330,6 +331,7 @@ impl MutableBody {
     /// `InsertPosition` is `InsertPosition::Before`, `source` will point to the same instruction as
     /// before. If `InsertPosition` is `InsertPosition::After`, `source` will point to the
     /// terminator of the newly inserted basic block.
+    #[allow(dead_code)]
     pub fn insert_bb(
         &mut self,
         mut bb: BasicBlock,
diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/initial_target_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/initial_target_visitor.rs
index 11ac412703ae..35d0e7041704 100644
--- a/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/initial_target_visitor.rs
+++ b/kani-compiler/src/kani_middle/transform/check_uninit/delayed_ub/initial_target_visitor.rs
@@ -4,14 +4,17 @@
 //! This module contains the visitor responsible for collecting initial analysis targets for delayed
 //! UB instrumentation.
 
-use crate::kani_middle::transform::check_uninit::ty_layout::tys_layout_equal_to_size;
+use crate::{
+    intrinsics::Intrinsic,
+    kani_middle::transform::check_uninit::ty_layout::tys_layout_equal_to_size,
+};
 use stable_mir::{
     mir::{
         alloc::GlobalAlloc,
         mono::{Instance, InstanceKind, StaticDef},
         visit::Location,
-        Body, CastKind, LocalDecl, MirVisitor, Mutability, NonDivergingIntrinsic, Operand, Place,
-        Rvalue, Statement, StatementKind, Terminator, TerminatorKind,
+        Body, CastKind, LocalDecl, MirVisitor, NonDivergingIntrinsic, Operand, Place, Rvalue,
+        Statement, StatementKind, Terminator, TerminatorKind,
     },
     ty::{ConstantKind, RigidTy, TyKind},
 };
@@ -101,34 +104,12 @@ impl MirVisitor for InitialTargetVisitor {
         if let TerminatorKind::Call { func, args, .. } = &term.kind {
             let instance = try_resolve_instance(self.body.locals(), func).unwrap();
             if instance.kind == InstanceKind::Intrinsic {
-                match instance.intrinsic_name().unwrap().as_str() {
-                    "copy" => {
-                        assert_eq!(args.len(), 3, "Unexpected number of arguments for `copy`");
-                        assert!(matches!(
-                            args[0].ty(self.body.locals()).unwrap().kind(),
-                            TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Not))
-                        ));
-                        assert!(matches!(
-                            args[1].ty(self.body.locals()).unwrap().kind(),
-                            TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Mut))
-                        ));
+                match Intrinsic::from_instance(&instance) {
+                    Intrinsic::Copy => {
                         // Here, `dst` is the second argument.
                         self.push_operand(&args[1]);
                     }
-                    "volatile_copy_memory" | "volatile_copy_nonoverlapping_memory" => {
-                        assert_eq!(
-                            args.len(),
-                            3,
-                            "Unexpected number of arguments for `volatile_copy`"
-                        );
-                        assert!(matches!(
-                            args[0].ty(self.body.locals()).unwrap().kind(),
-                            TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Mut))
-                        ));
-                        assert!(matches!(
-                            args[1].ty(self.body.locals()).unwrap().kind(),
-                            TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Not))
-                        ));
+                    Intrinsic::VolatileCopyMemory | Intrinsic::VolatileCopyNonOverlappingMemory => {
                         // Here, `dst` is the first argument.
                         self.push_operand(&args[0]);
                     }
diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs
index 837e14abc886..f682f93a261e 100644
--- a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs
+++ b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs
@@ -3,12 +3,15 @@
 //
 //! Visitor that collects all instructions relevant to uninitialized memory access.
 
-use crate::kani_middle::transform::{
-    body::{InsertPosition, MutableBody, SourceInstruction},
-    check_uninit::{
-        relevant_instruction::{InitRelevantInstruction, MemoryInitOp},
-        ty_layout::tys_layout_compatible_to_size,
-        TargetFinder,
+use crate::{
+    intrinsics::Intrinsic,
+    kani_middle::transform::{
+        body::{InsertPosition, MutableBody, SourceInstruction},
+        check_uninit::{
+            relevant_instruction::{InitRelevantInstruction, MemoryInitOp},
+            ty_layout::tys_layout_compatible_to_size,
+            TargetFinder,
+        },
     },
 };
 use stable_mir::{
@@ -16,8 +19,8 @@ use stable_mir::{
         alloc::GlobalAlloc,
         mono::{Instance, InstanceKind},
         visit::{Location, PlaceContext},
-        BasicBlockIdx, CastKind, LocalDecl, MirVisitor, Mutability, NonDivergingIntrinsic, Operand,
-        Place, PointerCoercion, ProjectionElem, Rvalue, Statement, StatementKind, Terminator,
+        BasicBlockIdx, CastKind, LocalDecl, MirVisitor, NonDivergingIntrinsic, Operand, Place,
+        PointerCoercion, ProjectionElem, Rvalue, Statement, StatementKind, Terminator,
         TerminatorKind,
     },
     ty::{ConstantKind, RigidTy, TyKind},
@@ -182,46 +185,30 @@ impl MirVisitor for CheckUninitVisitor {
                     };
                     match instance.kind {
                         InstanceKind::Intrinsic => {
-                            match instance.intrinsic_name().unwrap().as_str() {
-                                intrinsic_name if can_skip_intrinsic(intrinsic_name) => {
+                            match Intrinsic::from_instance(&instance) {
+                                intrinsic_name if can_skip_intrinsic(intrinsic_name.clone()) => {
                                     /* Intrinsics that can be safely skipped */
                                 }
-                                name if name.starts_with("atomic") => {
-                                    let num_args = match name {
-                                        // All `atomic_cxchg` intrinsics take `dst, old, src` as arguments.
-                                        name if name.starts_with("atomic_cxchg") => 3,
-                                        // All `atomic_load` intrinsics take `src` as an argument.
-                                        name if name.starts_with("atomic_load") => 1,
-                                        // All other `atomic` intrinsics take `dst, src` as arguments.
-                                        _ => 2,
-                                    };
-                                    assert_eq!(
-                                        args.len(),
-                                        num_args,
-                                        "Unexpected number of arguments for `{name}`"
-                                    );
-                                    assert!(matches!(
-                                        args[0].ty(&self.locals).unwrap().kind(),
-                                        TyKind::RigidTy(RigidTy::RawPtr(..))
-                                    ));
+                                Intrinsic::AtomicAnd(_)
+                                | Intrinsic::AtomicCxchg(_)
+                                | Intrinsic::AtomicCxchgWeak(_)
+                                | Intrinsic::AtomicLoad(_)
+                                | Intrinsic::AtomicMax(_)
+                                | Intrinsic::AtomicMin(_)
+                                | Intrinsic::AtomicNand(_)
+                                | Intrinsic::AtomicOr(_)
+                                | Intrinsic::AtomicStore(_)
+                                | Intrinsic::AtomicUmax(_)
+                                | Intrinsic::AtomicUmin(_)
+                                | Intrinsic::AtomicXadd(_)
+                                | Intrinsic::AtomicXchg(_)
+                                | Intrinsic::AtomicXor(_)
+                                | Intrinsic::AtomicXsub(_) => {
                                     self.push_target(MemoryInitOp::Check {
                                         operand: args[0].clone(),
                                     });
                                 }
-                                "compare_bytes" => {
-                                    assert_eq!(
-                                        args.len(),
-                                        3,
-                                        "Unexpected number of arguments for `compare_bytes`"
-                                    );
-                                    assert!(matches!(
-                                        args[0].ty(&self.locals).unwrap().kind(),
-                                        TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Not))
-                                    ));
-                                    assert!(matches!(
-                                        args[1].ty(&self.locals).unwrap().kind(),
-                                        TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Not))
-                                    ));
+                                Intrinsic::CompareBytes => {
                                     self.push_target(MemoryInitOp::CheckSliceChunk {
                                         operand: args[0].clone(),
                                         count: args[2].clone(),
@@ -231,22 +218,7 @@ impl MirVisitor for CheckUninitVisitor {
                                         count: args[2].clone(),
                                     });
                                 }
-                                "copy"
-                                | "volatile_copy_memory"
-                                | "volatile_copy_nonoverlapping_memory" => {
-                                    assert_eq!(
-                                        args.len(),
-                                        3,
-                                        "Unexpected number of arguments for `copy`"
-                                    );
-                                    assert!(matches!(
-                                        args[0].ty(&self.locals).unwrap().kind(),
-                                        TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Not))
-                                    ));
-                                    assert!(matches!(
-                                        args[1].ty(&self.locals).unwrap().kind(),
-                                        TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Mut))
-                                    ));
+                                Intrinsic::Copy => {
                                     self.push_target(MemoryInitOp::CheckSliceChunk {
                                         operand: args[0].clone(),
                                         count: args[2].clone(),
@@ -258,20 +230,20 @@ impl MirVisitor for CheckUninitVisitor {
                                         position: InsertPosition::After,
                                     });
                                 }
-                                "typed_swap" => {
-                                    assert_eq!(
-                                        args.len(),
-                                        2,
-                                        "Unexpected number of arguments for `typed_swap`"
-                                    );
-                                    assert!(matches!(
-                                        args[0].ty(&self.locals).unwrap().kind(),
-                                        TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Mut))
-                                    ));
-                                    assert!(matches!(
-                                        args[1].ty(&self.locals).unwrap().kind(),
-                                        TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Mut))
-                                    ));
+                                Intrinsic::VolatileCopyMemory
+                                | Intrinsic::VolatileCopyNonOverlappingMemory => {
+                                    self.push_target(MemoryInitOp::CheckSliceChunk {
+                                        operand: args[1].clone(),
+                                        count: args[2].clone(),
+                                    });
+                                    self.push_target(MemoryInitOp::SetSliceChunk {
+                                        operand: args[0].clone(),
+                                        count: args[2].clone(),
+                                        value: true,
+                                        position: InsertPosition::After,
+                                    });
+                                }
+                                Intrinsic::TypedSwap => {
                                     self.push_target(MemoryInitOp::Check {
                                         operand: args[0].clone(),
                                     });
@@ -279,46 +251,19 @@ impl MirVisitor for CheckUninitVisitor {
                                         operand: args[1].clone(),
                                     });
                                 }
-                                "volatile_load" | "unaligned_volatile_load" => {
-                                    assert_eq!(
-                                        args.len(),
-                                        1,
-                                        "Unexpected number of arguments for `volatile_load`"
-                                    );
-                                    assert!(matches!(
-                                        args[0].ty(&self.locals).unwrap().kind(),
-                                        TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Not))
-                                    ));
+                                Intrinsic::VolatileLoad | Intrinsic::UnalignedVolatileLoad => {
                                     self.push_target(MemoryInitOp::Check {
                                         operand: args[0].clone(),
                                     });
                                 }
-                                "volatile_store" => {
-                                    assert_eq!(
-                                        args.len(),
-                                        2,
-                                        "Unexpected number of arguments for `volatile_store`"
-                                    );
-                                    assert!(matches!(
-                                        args[0].ty(&self.locals).unwrap().kind(),
-                                        TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Mut))
-                                    ));
+                                Intrinsic::VolatileStore => {
                                     self.push_target(MemoryInitOp::Set {
                                         operand: args[0].clone(),
                                         value: true,
                                         position: InsertPosition::After,
                                     });
                                 }
-                                "write_bytes" => {
-                                    assert_eq!(
-                                        args.len(),
-                                        3,
-                                        "Unexpected number of arguments for `write_bytes`"
-                                    );
-                                    assert!(matches!(
-                                        args[0].ty(&self.locals).unwrap().kind(),
-                                        TyKind::RigidTy(RigidTy::RawPtr(_, Mutability::Mut))
-                                    ));
+                                Intrinsic::WriteBytes => {
                                     self.push_target(MemoryInitOp::SetSliceChunk {
                                         operand: args[0].clone(),
                                         count: args[2].clone(),
@@ -328,7 +273,7 @@ impl MirVisitor for CheckUninitVisitor {
                                 }
                                 intrinsic => {
                                     self.push_target(MemoryInitOp::Unsupported {
-                                    reason: format!("Kani does not support reasoning about memory initialization of intrinsic `{intrinsic}`."),
+                                    reason: format!("Kani does not support reasoning about memory initialization of intrinsic `{intrinsic:?}`."),
                                 });
                                 }
                             }
@@ -519,132 +464,131 @@ impl MirVisitor for CheckUninitVisitor {
 
 /// Determines if the intrinsic has no memory initialization related function and hence can be
 /// safely skipped.
-fn can_skip_intrinsic(intrinsic_name: &str) -> bool {
-    match intrinsic_name {
-        "add_with_overflow"
-        | "arith_offset"
-        | "assert_inhabited"
-        | "assert_mem_uninitialized_valid"
-        | "assert_zero_valid"
-        | "assume"
-        | "bitreverse"
-        | "black_box"
-        | "breakpoint"
-        | "bswap"
-        | "caller_location"
-        | "ceilf32"
-        | "ceilf64"
-        | "copysignf32"
-        | "copysignf64"
-        | "cosf32"
-        | "cosf64"
-        | "ctlz"
-        | "ctlz_nonzero"
-        | "ctpop"
-        | "cttz"
-        | "cttz_nonzero"
-        | "discriminant_value"
-        | "exact_div"
-        | "exp2f32"
-        | "exp2f64"
-        | "expf32"
-        | "expf64"
-        | "fabsf32"
-        | "fabsf64"
-        | "fadd_fast"
-        | "fdiv_fast"
-        | "floorf32"
-        | "floorf64"
-        | "fmaf32"
-        | "fmaf64"
-        | "fmul_fast"
-        | "forget"
-        | "fsub_fast"
-        | "is_val_statically_known"
-        | "likely"
-        | "log10f32"
-        | "log10f64"
-        | "log2f32"
-        | "log2f64"
-        | "logf32"
-        | "logf64"
-        | "maxnumf32"
-        | "maxnumf64"
-        | "min_align_of"
-        | "min_align_of_val"
-        | "minnumf32"
-        | "minnumf64"
-        | "mul_with_overflow"
-        | "nearbyintf32"
-        | "nearbyintf64"
-        | "needs_drop"
-        | "powf32"
-        | "powf64"
-        | "powif32"
-        | "powif64"
-        | "pref_align_of"
-        | "raw_eq"
-        | "rintf32"
-        | "rintf64"
-        | "rotate_left"
-        | "rotate_right"
-        | "roundf32"
-        | "roundf64"
-        | "saturating_add"
-        | "saturating_sub"
-        | "sinf32"
-        | "sinf64"
-        | "sqrtf32"
-        | "sqrtf64"
-        | "sub_with_overflow"
-        | "truncf32"
-        | "truncf64"
-        | "type_id"
-        | "type_name"
-        | "unchecked_div"
-        | "unchecked_rem"
-        | "unlikely"
-        | "vtable_size"
-        | "vtable_align"
-        | "wrapping_add"
-        | "wrapping_mul"
-        | "wrapping_sub" => {
+fn can_skip_intrinsic(intrinsic: Intrinsic) -> bool {
+    match intrinsic {
+        Intrinsic::AddWithOverflow
+        | Intrinsic::ArithOffset
+        | Intrinsic::AssertInhabited
+        | Intrinsic::AssertMemUninitializedValid
+        | Intrinsic::AssertZeroValid
+        | Intrinsic::Assume
+        | Intrinsic::Bitreverse
+        | Intrinsic::BlackBox
+        | Intrinsic::Breakpoint
+        | Intrinsic::Bswap
+        | Intrinsic::CeilF32
+        | Intrinsic::CeilF64
+        | Intrinsic::CopySignF32
+        | Intrinsic::CopySignF64
+        | Intrinsic::CosF32
+        | Intrinsic::CosF64
+        | Intrinsic::Ctlz
+        | Intrinsic::CtlzNonZero
+        | Intrinsic::Ctpop
+        | Intrinsic::Cttz
+        | Intrinsic::CttzNonZero
+        | Intrinsic::DiscriminantValue
+        | Intrinsic::ExactDiv
+        | Intrinsic::Exp2F32
+        | Intrinsic::Exp2F64
+        | Intrinsic::ExpF32
+        | Intrinsic::ExpF64
+        | Intrinsic::FabsF32
+        | Intrinsic::FabsF64
+        | Intrinsic::FaddFast
+        | Intrinsic::FdivFast
+        | Intrinsic::FloorF32
+        | Intrinsic::FloorF64
+        | Intrinsic::FmafF32
+        | Intrinsic::FmafF64
+        | Intrinsic::FmulFast
+        | Intrinsic::Forget
+        | Intrinsic::FsubFast
+        | Intrinsic::IsValStaticallyKnown
+        | Intrinsic::Likely
+        | Intrinsic::Log10F32
+        | Intrinsic::Log10F64
+        | Intrinsic::Log2F32
+        | Intrinsic::Log2F64
+        | Intrinsic::LogF32
+        | Intrinsic::LogF64
+        | Intrinsic::MaxNumF32
+        | Intrinsic::MaxNumF64
+        | Intrinsic::MinAlignOf
+        | Intrinsic::MinAlignOfVal
+        | Intrinsic::MinNumF32
+        | Intrinsic::MinNumF64
+        | Intrinsic::MulWithOverflow
+        | Intrinsic::NearbyIntF32
+        | Intrinsic::NearbyIntF64
+        | Intrinsic::NeedsDrop
+        | Intrinsic::PowF32
+        | Intrinsic::PowF64
+        | Intrinsic::PowIF32
+        | Intrinsic::PowIF64
+        | Intrinsic::PrefAlignOf
+        | Intrinsic::RawEq
+        | Intrinsic::RintF32
+        | Intrinsic::RintF64
+        | Intrinsic::RotateLeft
+        | Intrinsic::RotateRight
+        | Intrinsic::RoundF32
+        | Intrinsic::RoundF64
+        | Intrinsic::SaturatingAdd
+        | Intrinsic::SaturatingSub
+        | Intrinsic::SinF32
+        | Intrinsic::SinF64
+        | Intrinsic::SqrtF32
+        | Intrinsic::SqrtF64
+        | Intrinsic::SubWithOverflow
+        | Intrinsic::TruncF32
+        | Intrinsic::TruncF64
+        | Intrinsic::TypeId
+        | Intrinsic::TypeName
+        | Intrinsic::UncheckedDiv
+        | Intrinsic::UncheckedRem
+        | Intrinsic::Unlikely
+        | Intrinsic::VtableSize
+        | Intrinsic::VtableAlign
+        | Intrinsic::WrappingAdd
+        | Intrinsic::WrappingMul
+        | Intrinsic::WrappingSub => {
             /* Intrinsics that do not interact with memory initialization. */
             true
         }
-        "ptr_guaranteed_cmp" | "ptr_offset_from" | "ptr_offset_from_unsigned" | "size_of_val" => {
+        Intrinsic::PtrGuaranteedCmp
+        | Intrinsic::PtrOffsetFrom
+        | Intrinsic::PtrOffsetFromUnsigned
+        | Intrinsic::SizeOfVal => {
             /* AFAICS from the documentation, none of those require the pointer arguments to be actually initialized. */
             true
         }
-        name if name.starts_with("simd") => {
+        Intrinsic::SimdAdd
+        | Intrinsic::SimdAnd
+        | Intrinsic::SimdDiv
+        | Intrinsic::SimdRem
+        | Intrinsic::SimdEq
+        | Intrinsic::SimdExtract
+        | Intrinsic::SimdGe
+        | Intrinsic::SimdGt
+        | Intrinsic::SimdInsert
+        | Intrinsic::SimdLe
+        | Intrinsic::SimdLt
+        | Intrinsic::SimdMul
+        | Intrinsic::SimdNe
+        | Intrinsic::SimdOr
+        | Intrinsic::SimdShl
+        | Intrinsic::SimdShr
+        | Intrinsic::SimdShuffle(_)
+        | Intrinsic::SimdSub
+        | Intrinsic::SimdXor => {
             /* SIMD operations */
             true
         }
-        name if name.starts_with("atomic_fence")
-            || name.starts_with("atomic_singlethreadfence") =>
-        {
+        Intrinsic::AtomicFence(_) | Intrinsic::AtomicSingleThreadFence(_) => {
             /* Atomic fences */
             true
         }
-        "copy_nonoverlapping" => unreachable!(
-            "Expected `core::intrinsics::unreachable` to be handled by `StatementKind::CopyNonOverlapping`"
-        ),
-        "offset" => unreachable!(
-            "Expected `core::intrinsics::unreachable` to be handled by `BinOp::OffSet`"
-        ),
-        "unreachable" => unreachable!(
-            "Expected `std::intrinsics::unreachable` to be handled by `TerminatorKind::Unreachable`"
-        ),
-        "transmute" | "transmute_copy" | "unchecked_add" | "unchecked_mul" | "unchecked_shl"
-        | "size_of" | "unchecked_shr" | "unchecked_sub" => {
-            unreachable!("Expected intrinsic to be lowered before codegen")
-        }
-        "catch_unwind" => {
-            unimplemented!("")
-        }
-        "retag_box_to_raw" => {
-            unreachable!("This was removed in the latest Rust version.")
-        }
         _ => {
             /* Everything else */
             false
diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs
index 7f1fb144a09b..e47483fb4fa5 100644
--- a/kani-compiler/src/main.rs
+++ b/kani-compiler/src/main.rs
@@ -39,6 +39,7 @@ extern crate tempfile;
 mod args;
 #[cfg(feature = "cprover")]
 mod codegen_cprover_gotoc;
+mod intrinsics;
 mod kani_compiler;
 mod kani_middle;
 mod kani_queries;
diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml
index d58d686d7d43..c57ec8e8e2f2 100644
--- a/kani-driver/Cargo.toml
+++ b/kani-driver/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani-driver"
-version = "0.53.0"
+version = "0.54.0"
 edition = "2021"
 description = "Build a project with Kani and run all proof harnesses"
 license = "MIT OR Apache-2.0"
diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs
index bbeb5bfa417d..4b30fe877507 100644
--- a/kani-driver/src/call_single_file.rs
+++ b/kani-driver/src/call_single_file.rs
@@ -135,10 +135,6 @@ impl KaniSession {
             flags.push("--ub-check=validity".into())
         }
 
-        if self.args.common_args.unstable_features.contains(UnstableFeature::PtrToRefCastChecks) {
-            flags.push("--ub-check=ptr_to_ref_cast".into())
-        }
-
         if self.args.common_args.unstable_features.contains(UnstableFeature::UninitChecks) {
             // Automatically enable shadow memory, since the version of uninitialized memory checks
             // without non-determinism depends on it.
diff --git a/kani_metadata/Cargo.toml b/kani_metadata/Cargo.toml
index 816752a58e03..de91900d6d9c 100644
--- a/kani_metadata/Cargo.toml
+++ b/kani_metadata/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani_metadata"
-version = "0.53.0"
+version = "0.54.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
diff --git a/kani_metadata/src/unstable.rs b/kani_metadata/src/unstable.rs
index 68e4fba28819..120ab0a9e55c 100644
--- a/kani_metadata/src/unstable.rs
+++ b/kani_metadata/src/unstable.rs
@@ -89,8 +89,6 @@ pub enum UnstableFeature {
     ValidValueChecks,
     /// Ghost state and shadow memory APIs.
     GhostState,
-    /// Automatically check that pointers are valid when casting them to references.
-    PtrToRefCastChecks,
     /// Automatically check that uninitialized memory is not used.
     UninitChecks,
     /// Enable an unstable option or subcommand.
diff --git a/library/kani/Cargo.toml b/library/kani/Cargo.toml
index 91fee3dabf30..7d7ced8ee0b7 100644
--- a/library/kani/Cargo.toml
+++ b/library/kani/Cargo.toml
@@ -3,13 +3,15 @@
 
 [package]
 name = "kani"
-version = "0.53.0"
+version = "0.54.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
 
 [dependencies]
 kani_macros = { path = "../kani_macros" }
+kani_core = { path = "../kani_core" }
 
 [features]
 concrete_playback = []
+no_core=["kani_macros/no_core"]
diff --git a/library/kani/src/arbitrary.rs b/library/kani/src/arbitrary.rs
index 83b113d64927..f16f06165d29 100644
--- a/library/kani/src/arbitrary.rs
+++ b/library/kani/src/arbitrary.rs
@@ -4,151 +4,7 @@
 //! This module introduces the `Arbitrary` trait as well as implementation for
 //! primitive types and other std containers.
 
-use std::{
-    marker::{PhantomData, PhantomPinned},
-    num::*,
-};
-
-/// This trait should be used to generate symbolic variables that represent any valid value of
-/// its type.
-pub trait Arbitrary
-where
-    Self: Sized,
-{
-    fn any() -> Self;
-    fn any_array<const MAX_ARRAY_LENGTH: usize>() -> [Self; MAX_ARRAY_LENGTH] {
-        [(); MAX_ARRAY_LENGTH].map(|_| Self::any())
-    }
-}
-
-/// The given type can be represented by an unconstrained symbolic value of size_of::<T>.
-macro_rules! trivial_arbitrary {
-    ( $type: ty ) => {
-        impl Arbitrary for $type {
-            #[inline(always)]
-            fn any() -> Self {
-                // This size_of call does not use generic_const_exprs feature. It's inside a macro, and Self isn't generic.
-                unsafe { crate::any_raw_internal::<Self>() }
-            }
-            fn any_array<const MAX_ARRAY_LENGTH: usize>() -> [Self; MAX_ARRAY_LENGTH] {
-                unsafe { crate::any_raw_array::<Self, MAX_ARRAY_LENGTH>() }
-            }
-        }
-    };
-}
-
-trivial_arbitrary!(u8);
-trivial_arbitrary!(u16);
-trivial_arbitrary!(u32);
-trivial_arbitrary!(u64);
-trivial_arbitrary!(u128);
-trivial_arbitrary!(usize);
-
-trivial_arbitrary!(i8);
-trivial_arbitrary!(i16);
-trivial_arbitrary!(i32);
-trivial_arbitrary!(i64);
-trivial_arbitrary!(i128);
-trivial_arbitrary!(isize);
-
-// We do not constrain floating points values per type spec. Users must add assumptions to their
-// verification code if they want to eliminate NaN, infinite, or subnormal.
-trivial_arbitrary!(f32);
-trivial_arbitrary!(f64);
-
-// Similarly, we do not constraint values for non-standard floating types.
-trivial_arbitrary!(f16);
-trivial_arbitrary!(f128);
-
-trivial_arbitrary!(());
-
-impl Arbitrary for bool {
-    #[inline(always)]
-    fn any() -> Self {
-        let byte = u8::any();
-        crate::assume(byte < 2);
-        byte == 1
-    }
-}
-
-/// Validate that a char is not outside the ranges [0x0, 0xD7FF] and [0xE000, 0x10FFFF]
-/// Ref: <https://doc.rust-lang.org/stable/nomicon/what-unsafe-does.html>
-impl Arbitrary for char {
-    #[inline(always)]
-    fn any() -> Self {
-        // Generate an arbitrary u32 and constrain it to make it a valid representation of char.
-        let val = u32::any();
-        crate::assume(val <= 0xD7FF || (0xE000..=0x10FFFF).contains(&val));
-        unsafe { char::from_u32_unchecked(val) }
-    }
-}
-
-macro_rules! nonzero_arbitrary {
-    ( $type: ty, $base: ty ) => {
-        impl Arbitrary for $type {
-            #[inline(always)]
-            fn any() -> Self {
-                let val = <$base>::any();
-                crate::assume(val != 0);
-                unsafe { <$type>::new_unchecked(val) }
-            }
-        }
-    };
-}
-
-nonzero_arbitrary!(NonZeroU8, u8);
-nonzero_arbitrary!(NonZeroU16, u16);
-nonzero_arbitrary!(NonZeroU32, u32);
-nonzero_arbitrary!(NonZeroU64, u64);
-nonzero_arbitrary!(NonZeroU128, u128);
-nonzero_arbitrary!(NonZeroUsize, usize);
-
-nonzero_arbitrary!(NonZeroI8, i8);
-nonzero_arbitrary!(NonZeroI16, i16);
-nonzero_arbitrary!(NonZeroI32, i32);
-nonzero_arbitrary!(NonZeroI64, i64);
-nonzero_arbitrary!(NonZeroI128, i128);
-nonzero_arbitrary!(NonZeroIsize, isize);
-
-impl<T, const N: usize> Arbitrary for [T; N]
-where
-    T: Arbitrary,
-{
-    fn any() -> Self {
-        T::any_array()
-    }
-}
-
-impl<T> Arbitrary for Option<T>
-where
-    T: Arbitrary,
-{
-    fn any() -> Self {
-        if bool::any() { Some(T::any()) } else { None }
-    }
-}
-
-impl<T, E> Arbitrary for Result<T, E>
-where
-    T: Arbitrary,
-    E: Arbitrary,
-{
-    fn any() -> Self {
-        if bool::any() { Ok(T::any()) } else { Err(E::any()) }
-    }
-}
-
-impl<T: ?Sized> Arbitrary for std::marker::PhantomData<T> {
-    fn any() -> Self {
-        PhantomData
-    }
-}
-
-impl Arbitrary for std::marker::PhantomPinned {
-    fn any() -> Self {
-        PhantomPinned
-    }
-}
+use crate::Arbitrary;
 
 impl<T> Arbitrary for std::boxed::Box<T>
 where
diff --git a/library/kani/src/internal.rs b/library/kani/src/internal.rs
deleted file mode 100644
index 68b15316b4c1..000000000000
--- a/library/kani/src/internal.rs
+++ /dev/null
@@ -1,160 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-
-use crate::arbitrary::Arbitrary;
-use std::ptr;
-
-/// Helper trait for code generation for `modifies` contracts.
-///
-/// We allow the user to provide us with a pointer-like object that we convert as needed.
-#[doc(hidden)]
-pub trait Pointer {
-    /// Type of the pointed-to data
-    type Inner: ?Sized;
-
-    /// used for havocking on replecement of a `modifies` clause.
-    unsafe fn assignable(self) -> *mut Self::Inner;
-}
-
-impl<T: ?Sized> Pointer for &T {
-    type Inner = T;
-    unsafe fn assignable(self) -> *mut Self::Inner {
-        self as *const T as *mut T
-    }
-}
-
-impl<T: ?Sized> Pointer for &mut T {
-    type Inner = T;
-
-    unsafe fn assignable(self) -> *mut Self::Inner {
-        self as *mut T
-    }
-}
-
-impl<T: ?Sized> Pointer for *const T {
-    type Inner = T;
-
-    unsafe fn assignable(self) -> *mut Self::Inner {
-        self as *mut T
-    }
-}
-
-impl<T: ?Sized> Pointer for *mut T {
-    type Inner = T;
-    unsafe fn assignable(self) -> *mut Self::Inner {
-        self
-    }
-}
-
-/// A way to break the ownerhip rules. Only used by contracts where we can
-/// guarantee it is done safely.
-/// TODO: Remove this! This is not safe. Users should be able to use `ptr::read` and `old` if
-/// they really need to. See <https://github.com/model-checking/kani/issues/3293>.
-#[inline(never)]
-#[doc(hidden)]
-#[rustc_diagnostic_item = "KaniUntrackedDeref"]
-pub fn untracked_deref<T>(_: &T) -> T {
-    todo!()
-}
-
-/// CBMC contracts currently has a limitation where `free` has to be in scope.
-/// However, if there is no dynamic allocation in the harness, slicing removes `free` from the
-/// scope.
-///
-/// Thus, this function will basically translate into:
-/// ```c
-/// // This is a no-op.
-/// free(NULL);
-/// ```
-#[inline(never)]
-#[doc(hidden)]
-#[rustc_diagnostic_item = "KaniInitContracts"]
-pub fn init_contracts() {}
-
-/// This should only be used within contracts. The intent is to
-/// perform type inference on a closure's argument
-/// TODO: This should be generated inside the function that has contract. This is used for
-/// remembers.
-#[doc(hidden)]
-pub fn apply_closure<T, U: Fn(&T) -> bool>(f: U, x: &T) -> bool {
-    f(x)
-}
-
-/// Recieves a reference to a pointer-like object and assigns kani::any_modifies to that object.
-/// Only for use within function contracts and will not be replaced if the recursive or function stub
-/// replace contracts are not used.
-#[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")]
-#[rustc_diagnostic_item = "KaniWriteAny"]
-#[inline(never)]
-#[doc(hidden)]
-pub unsafe fn write_any<T: ?Sized>(_pointer: *mut T) {
-    // This function should not be reacheable.
-    // Users must include `#[kani::recursion]` in any function contracts for recursive functions;
-    // otherwise, this might not be properly instantiate. We mark this as unreachable to make
-    // sure Kani doesn't report any false positives.
-    unreachable!()
-}
-
-/// Fill in a slice with kani::any.
-/// Intended as a post compilation replacement for write_any
-#[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")]
-#[rustc_diagnostic_item = "KaniWriteAnySlice"]
-#[inline(always)]
-pub unsafe fn write_any_slice<T: Arbitrary>(slice: *mut [T]) {
-    (*slice).fill_with(T::any)
-}
-
-/// Fill in a pointer with kani::any.
-/// Intended as a post compilation replacement for write_any
-#[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")]
-#[rustc_diagnostic_item = "KaniWriteAnySlim"]
-#[inline(always)]
-pub unsafe fn write_any_slim<T: Arbitrary>(pointer: *mut T) {
-    ptr::write(pointer, T::any())
-}
-
-/// Fill in a str with kani::any.
-/// Intended as a post compilation replacement for write_any.
-/// Not yet implemented
-#[crate::unstable(feature = "function-contracts", issue = "none", reason = "function-contracts")]
-#[rustc_diagnostic_item = "KaniWriteAnyStr"]
-#[inline(always)]
-pub unsafe fn write_any_str(_s: *mut str) {
-    //TODO: strings introduce new UB
-    //(*s).as_bytes_mut().fill_with(u8::any)
-    //TODO: String validation
-    unimplemented!("Kani does not support creating arbitrary `str`")
-}
-
-/// Function that calls a closure used to implement contracts.
-///
-/// In contracts, we cannot invoke the generated closures directly, instead, we call register
-/// contract. This function is a no-op. However, in the reality, we do want to call the closure,
-/// so we swap the register body by this function body.
-#[doc(hidden)]
-#[allow(dead_code)]
-#[rustc_diagnostic_item = "KaniRunContract"]
-#[crate::unstable(
-    feature = "function-contracts",
-    issue = "none",
-    reason = "internal function required to run contract closure"
-)]
-fn run_contract_fn<T, F: FnOnce() -> T>(func: F) -> T {
-    func()
-}
-
-/// This is used by contracts to select which version of the contract to use during codegen.
-#[doc(hidden)]
-pub type Mode = u8;
-
-/// Keep the original body.
-pub const ORIGINAL: Mode = 0;
-
-/// Run the check with recursion support.
-pub const RECURSION_CHECK: Mode = 1;
-
-/// Run the simple check with no recursion support.
-pub const SIMPLE_CHECK: Mode = 2;
-
-/// Stub the body with its contract.
-pub const REPLACE: Mode = 3;
diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs
index 046c6e7a0667..59a89622a52d 100644
--- a/library/kani/src/lib.rs
+++ b/library/kani/src/lib.rs
@@ -28,19 +28,13 @@ pub mod arbitrary;
 mod concrete_playback;
 pub mod futures;
 pub mod invariant;
-pub mod mem;
 pub mod shadow;
 pub mod slice;
-pub mod tuple;
 pub mod vec;
 
-#[doc(hidden)]
-pub mod internal;
-
 mod mem_init;
 mod models;
 
-pub use arbitrary::Arbitrary;
 #[cfg(feature = "concrete_playback")]
 pub use concrete_playback::concrete_playback_run;
 pub use invariant::Invariant;
@@ -53,287 +47,19 @@ pub fn concrete_playback_run<F: Fn()>(_: Vec<Vec<u8>>, _: F) {
 
 pub use futures::{block_on, block_on_with_spawn, spawn, yield_now, RoundRobin};
 
-/// Creates an assumption that will be valid after this statement run. Note that the assumption
-/// will only be applied for paths that follow the assumption. If the assumption doesn't hold, the
-/// program will exit successfully.
-///
-/// # Example:
-///
-/// The code snippet below should never panic.
-///
-/// ```rust
-/// let i : i32 = kani::any();
-/// kani::assume(i > 10);
-/// if i < 0 {
-///   panic!("This will never panic");
-/// }
-/// ```
-///
-/// The following code may panic though:
-///
-/// ```rust
-/// let i : i32 = kani::any();
-/// assert!(i < 0, "This may panic and verification should fail.");
-/// kani::assume(i > 10);
-/// ```
-#[inline(never)]
-#[rustc_diagnostic_item = "KaniAssume"]
-#[cfg(not(feature = "concrete_playback"))]
-pub fn assume(cond: bool) {
-    let _ = cond;
-}
-
-#[inline(never)]
-#[rustc_diagnostic_item = "KaniAssume"]
-#[cfg(feature = "concrete_playback")]
-pub fn assume(cond: bool) {
-    assert!(cond, "`kani::assume` should always hold");
-}
-
-/// `implies!(premise => conclusion)` means that if the `premise` is true, so
-/// must be the `conclusion`.
-///
-/// This simply expands to `!premise || conclusion` and is intended to make checks more readable,
-/// as the concept of an implication is more natural to think about than its expansion.
-#[macro_export]
-macro_rules! implies {
-    ($premise:expr => $conclusion:expr) => {
-        !($premise) || ($conclusion)
-    };
-}
-
-/// Creates an assertion of the specified condition and message.
-///
-/// # Example:
-///
-/// ```rust
-/// let x: bool = kani::any();
-/// let y = !x;
-/// kani::assert(x || y, "ORing a boolean variable with its negation must be true")
-/// ```
-#[cfg(not(feature = "concrete_playback"))]
-#[inline(never)]
-#[rustc_diagnostic_item = "KaniAssert"]
-pub const fn assert(cond: bool, msg: &'static str) {
-    let _ = cond;
-    let _ = msg;
-}
-
-#[cfg(feature = "concrete_playback")]
-#[inline(never)]
-#[rustc_diagnostic_item = "KaniAssert"]
-pub const fn assert(cond: bool, msg: &'static str) {
-    assert!(cond, "{}", msg);
-}
-
-/// Creates an assertion of the specified condition, but does not assume it afterwards.
-///
-/// # Example:
-///
-/// ```rust
-/// let x: bool = kani::any();
-/// let y = !x;
-/// kani::check(x || y, "ORing a boolean variable with its negation must be true")
-/// ```
-#[cfg(not(feature = "concrete_playback"))]
-#[inline(never)]
-#[rustc_diagnostic_item = "KaniCheck"]
-pub const fn check(cond: bool, msg: &'static str) {
-    let _ = cond;
-    let _ = msg;
-}
-
-#[cfg(feature = "concrete_playback")]
-#[inline(never)]
-#[rustc_diagnostic_item = "KaniCheck"]
-pub const fn check(cond: bool, msg: &'static str) {
-    assert!(cond, "{}", msg);
-}
-
-/// Creates a cover property with the specified condition and message.
-///
-/// # Example:
-///
-/// ```rust
-/// kani::cover(slice.len() == 0, "The slice may have a length of 0");
-/// ```
-///
-/// A cover property checks if there is at least one execution that satisfies
-/// the specified condition at the location in which the function is called.
-///
-/// Cover properties are reported as:
-///  - SATISFIED: if Kani found an execution that satisfies the condition
-///  - UNSATISFIABLE: if Kani proved that the condition cannot be satisfied
-///  - UNREACHABLE: if Kani proved that the cover property itself is unreachable (i.e. it is vacuously UNSATISFIABLE)
-///
-/// This function is called by the [`cover!`] macro. The macro is more
-/// convenient to use.
-///
-#[inline(never)]
-#[rustc_diagnostic_item = "KaniCover"]
-pub const fn cover(_cond: bool, _msg: &'static str) {}
+// Kani proc macros must be in a separate crate
+pub use kani_macros::*;
 
-/// This creates an symbolic *valid* value of type `T`. You can assign the return value of this
-/// function to a variable that you want to make symbolic.
-///
-/// # Example:
-///
-/// In the snippet below, we are verifying the behavior of the function `fn_under_verification`
-/// under all possible `NonZeroU8` input values, i.e., all possible `u8` values except zero.
-///
-/// ```rust
-/// let inputA = kani::any::<std::num::NonZeroU8>();
-/// fn_under_verification(inputA);
-/// ```
-///
-/// Note: This is a safe construct and can only be used with types that implement the `Arbitrary`
-/// trait. The Arbitrary trait is used to build a symbolic value that represents all possible
-/// valid values for type `T`.
-#[rustc_diagnostic_item = "KaniAny"]
-#[inline(always)]
-pub fn any<T: Arbitrary>() -> T {
-    T::any()
-}
+// Declare common Kani API such as assume, assert
+kani_core::kani_lib!(kani);
 
-/// This function is only used for function contract instrumentation.
-/// It behaves exaclty like `kani::any<T>()`, except it will check for the trait bounds
-/// at compilation time. It allows us to avoid type checking errors while using function
-/// contracts only for verification.
-#[rustc_diagnostic_item = "KaniAnyModifies"]
-#[inline(never)]
+// Used to bind `core::assert` to a different name to avoid possible name conflicts if a
+// crate uses `extern crate std as core`. See
+// https://github.com/model-checking/kani/issues/1949 and https://github.com/model-checking/kani/issues/2187
 #[doc(hidden)]
-pub fn any_modifies<T>() -> T {
-    // This function should not be reacheable.
-    // Users must include `#[kani::recursion]` in any function contracts for recursive functions;
-    // otherwise, this might not be properly instantiate. We mark this as unreachable to make
-    // sure Kani doesn't report any false positives.
-    unreachable!()
-}
-
-/// This creates a symbolic *valid* value of type `T`.
-/// The value is constrained to be a value accepted by the predicate passed to the filter.
-/// You can assign the return value of this function to a variable that you want to make symbolic.
-///
-/// # Example:
-///
-/// In the snippet below, we are verifying the behavior of the function `fn_under_verification`
-/// under all possible `u8` input values between 0 and 12.
-///
-/// ```rust
-/// let inputA: u8 = kani::any_where(|x| *x < 12);
-/// fn_under_verification(inputA);
-/// ```
-///
-/// Note: This is a safe construct and can only be used with types that implement the `Arbitrary`
-/// trait. The Arbitrary trait is used to build a symbolic value that represents all possible
-/// valid values for type `T`.
-#[inline(always)]
-pub fn any_where<T: Arbitrary, F: FnOnce(&T) -> bool>(f: F) -> T {
-    let result = T::any();
-    assume(f(&result));
-    result
-}
-
-/// This function creates a symbolic value of type `T`. This may result in an invalid value.
-///
-/// # Safety
-///
-/// This function is unsafe and it may represent invalid `T` values which can lead to many
-/// undesirable undefined behaviors. Because of that, this function can only be used
-/// internally when we can guarantee that the type T has no restriction regarding its bit level
-/// representation.
-///
-/// This function is also used to find concrete values in the CBMC output trace
-/// and return those concrete values in concrete playback mode.
-///
-/// Note that SIZE_T must be equal the size of type T in bytes.
-#[inline(never)]
-#[cfg(not(feature = "concrete_playback"))]
-unsafe fn any_raw_internal<T: Copy>() -> T {
-    any_raw::<T>()
-}
-
-/// This is the same as [any_raw_internal] for verification flow, but not for concrete playback.
-#[inline(never)]
 #[cfg(not(feature = "concrete_playback"))]
-unsafe fn any_raw_array<T: Copy, const N: usize>() -> [T; N] {
-    any_raw::<[T; N]>()
-}
-
-#[cfg(feature = "concrete_playback")]
-use concrete_playback::{any_raw_array, any_raw_internal};
-
-/// This low-level function returns nondet bytes of size T.
-#[rustc_diagnostic_item = "KaniAnyRaw"]
-#[inline(never)]
-#[allow(dead_code)]
-fn any_raw<T: Copy>() -> T {
-    kani_intrinsic()
-}
-
-/// Function used to generate panic with a static message as this is the only one currently
-/// supported by Kani display.
-///
-/// During verification this will get replaced by `assert(false)`. For concrete executions, we just
-/// invoke the regular `std::panic!()` function. This function is used by our standard library
-/// overrides, but not the other way around.
-#[inline(never)]
-#[rustc_diagnostic_item = "KaniPanic"]
-#[doc(hidden)]
-pub const fn panic(message: &'static str) -> ! {
-    panic!("{}", message)
-}
+pub use core::assert as __kani__workaround_core_assert;
 
-/// An empty body that can be used to define Kani intrinsic functions.
-///
-/// A Kani intrinsic is a function that is interpreted by Kani compiler.
-/// While we could use `unreachable!()` or `panic!()` as the body of a kani intrinsic
-/// function, both cause Kani to produce a warning since we don't support caller location.
-/// (see https://github.com/model-checking/kani/issues/2010).
-///
-/// This function is dead, since its caller is always  handled via a hook anyway,
-/// so we just need to put a body that rustc does not complain about.
-/// An infinite loop works out nicely.
-fn kani_intrinsic<T>() -> T {
-    #[allow(clippy::empty_loop)]
-    loop {}
-}
-/// A macro to check if a condition is satisfiable at a specific location in the
-/// code.
-///
-/// # Example 1:
-///
-/// ```rust
-/// let mut set: BTreeSet<i32> = BTreeSet::new();
-/// set.insert(kani::any());
-/// set.insert(kani::any());
-/// // check if the set can end up with a single element (if both elements
-/// // inserted were the same)
-/// kani::cover!(set.len() == 1);
-/// ```
-/// The macro can also be called without any arguments to check if a location is
-/// reachable.
-///
-/// # Example 2:
-///
-/// ```rust
-/// match e {
-///     MyEnum::A => { /* .. */ }
-///     MyEnum::B => {
-///         // make sure the `MyEnum::B` variant is possible
-///         kani::cover!();
-///         // ..
-///     }
-/// }
-/// ```
-///
-/// A custom message can also be passed to the macro.
-///
-/// # Example 3:
-///
-/// ```rust
-/// kani::cover!(x > y, "x can be greater than y")
-/// ```
 #[macro_export]
 macro_rules! cover {
     () => {
@@ -347,15 +73,17 @@ macro_rules! cover {
     };
 }
 
-// Used to bind `core::assert` to a different name to avoid possible name conflicts if a
-// crate uses `extern crate std as core`. See
-// https://github.com/model-checking/kani/issues/1949 and https://github.com/model-checking/kani/issues/2187
-#[doc(hidden)]
-#[cfg(not(feature = "concrete_playback"))]
-pub use core::assert as __kani__workaround_core_assert;
-
-// Kani proc macros must be in a separate crate
-pub use kani_macros::*;
+/// `implies!(premise => conclusion)` means that if the `premise` is true, so
+/// must be the `conclusion`.
+///
+/// This simply expands to `!premise || conclusion` and is intended to make checks more readable,
+/// as the concept of an implication is more natural to think about than its expansion.
+#[macro_export]
+macro_rules! implies {
+    ($premise:expr => $conclusion:expr) => {
+        !($premise) || ($conclusion)
+    };
+}
 
 pub(crate) use kani_macros::unstable_feature as unstable;
 
diff --git a/library/kani/src/mem.rs b/library/kani/src/mem.rs
deleted file mode 100644
index f718c09ec38d..000000000000
--- a/library/kani/src/mem.rs
+++ /dev/null
@@ -1,433 +0,0 @@
-// Copyright Kani Contributors
-// SPDX-License-Identifier: Apache-2.0 OR MIT
-//! This module contains functions useful for checking unsafe memory access.
-//!
-//! Given the following validity rules provided in the Rust documentation:
-//! <https://doc.rust-lang.org/std/ptr/index.html> (accessed Feb 6th, 2024)
-//!
-//! 1. A null pointer is never valid, not even for accesses of size zero.
-//! 2. For a pointer to be valid, it is necessary, but not always sufficient, that the pointer
-//!    be dereferenceable: the memory range of the given size starting at the pointer must all be
-//!    within the bounds of a single allocated object. Note that in Rust, every (stack-allocated)
-//!    variable is considered a separate allocated object.
-//!    ~~Even for operations of size zero, the pointer must not be pointing to deallocated memory,
-//!    i.e., deallocation makes pointers invalid even for zero-sized operations.~~
-//!    ZST access is not OK for any pointer.
-//!    See: <https://github.com/rust-lang/unsafe-code-guidelines/issues/472>
-//! 3. However, casting any non-zero integer literal to a pointer is valid for zero-sized
-//!    accesses, even if some memory happens to exist at that address and gets deallocated.
-//!    This corresponds to writing your own allocator: allocating zero-sized objects is not very
-//!    hard. The canonical way to obtain a pointer that is valid for zero-sized accesses is
-//!    `NonNull::dangling`.
-//! 4. All accesses performed by functions in this module are non-atomic in the sense of atomic
-//!    operations used to synchronize between threads.
-//!    This means it is undefined behavior to perform two concurrent accesses to the same location
-//!    from different threads unless both accesses only read from memory.
-//!    Notice that this explicitly includes `read_volatile` and `write_volatile`:
-//!    Volatile accesses cannot be used for inter-thread synchronization.
-//! 5. The result of casting a reference to a pointer is valid for as long as the underlying
-//!    object is live and no reference (just raw pointers) is used to access the same memory.
-//!    That is, reference and pointer accesses cannot be interleaved.
-//!
-//! Kani is able to verify #1 and #2 today.
-//!
-//! For #3, we are overly cautious, and Kani will only consider zero-sized pointer access safe if
-//! the address matches `NonNull::<()>::dangling()`.
-//! The way Kani tracks provenance is not enough to check if the address was the result of a cast
-//! from a non-zero integer literal.
-
-use crate::kani_intrinsic;
-use crate::mem::private::Internal;
-use std::mem::{align_of, size_of};
-use std::ptr::{DynMetadata, NonNull, Pointee};
-
-/// Check if the pointer is valid for write access according to [crate::mem] conditions 1, 2
-/// and 3.
-///
-/// Note this function also checks for pointer alignment. Use [self::can_write_unaligned]
-/// if you don't want to fail for unaligned pointers.
-///
-/// This function does not check if the value stored is valid for the given type. Use
-/// [self::can_dereference] for that.
-///
-/// This function will panic today if the pointer is not null, and it points to an unallocated or
-/// deallocated memory location. This is an existing Kani limitation.
-/// See <https://github.com/model-checking/kani/issues/2690> for more details.
-#[crate::unstable(
-    feature = "mem-predicates",
-    issue = 2690,
-    reason = "experimental memory predicate API"
-)]
-pub fn can_write<T>(ptr: *mut T) -> bool
-where
-    T: ?Sized,
-    <T as Pointee>::Metadata: PtrProperties<T>,
-{
-    // The interface takes a mutable pointer to improve readability of the signature.
-    // However, using constant pointer avoid unnecessary instrumentation, and it is as powerful.
-    // Hence, cast to `*const T`.
-    let ptr: *const T = ptr;
-    let (thin_ptr, metadata) = ptr.to_raw_parts();
-    metadata.is_ptr_aligned(thin_ptr, Internal) && is_inbounds(&metadata, thin_ptr)
-}
-
-/// Check if the pointer is valid for unaligned write access according to [crate::mem] conditions
-/// 1, 2 and 3.
-///
-/// Note this function succeeds for unaligned pointers. See [self::can_write] if you also
-/// want to check pointer alignment.
-///
-/// This function will panic today if the pointer is not null, and it points to an unallocated or
-/// deallocated memory location. This is an existing Kani limitation.
-/// See <https://github.com/model-checking/kani/issues/2690> for more details.
-#[crate::unstable(
-    feature = "mem-predicates",
-    issue = 2690,
-    reason = "experimental memory predicate API"
-)]
-pub fn can_write_unaligned<T>(ptr: *const T) -> bool
-where
-    T: ?Sized,
-    <T as Pointee>::Metadata: PtrProperties<T>,
-{
-    let (thin_ptr, metadata) = ptr.to_raw_parts();
-    is_inbounds(&metadata, thin_ptr)
-}
-
-/// Checks that pointer `ptr` point to a valid value of type `T`.
-///
-/// For that, the pointer has to be a valid pointer according to [crate::mem] conditions 1, 2
-/// and 3,
-/// and the value stored must respect the validity invariants for type `T`.
-///
-/// TODO: Kani should automatically add those checks when a de-reference happens.
-/// <https://github.com/model-checking/kani/issues/2975>
-///
-/// This function will panic today if the pointer is not null, and it points to an unallocated or
-/// deallocated memory location. This is an existing Kani limitation.
-/// See <https://github.com/model-checking/kani/issues/2690> for more details.
-#[crate::unstable(
-    feature = "mem-predicates",
-    issue = 2690,
-    reason = "experimental memory predicate API"
-)]
-#[allow(clippy::not_unsafe_ptr_arg_deref)]
-pub fn can_dereference<T>(ptr: *const T) -> bool
-where
-    T: ?Sized,
-    <T as Pointee>::Metadata: PtrProperties<T>,
-{
-    let (thin_ptr, metadata) = ptr.to_raw_parts();
-    // Need to assert `is_initialized` because non-determinism is used under the hood, so it does
-    // not make sense to use it inside assumption context.
-    metadata.is_ptr_aligned(thin_ptr, Internal)
-        && is_inbounds(&metadata, thin_ptr)
-        && assert_is_initialized(ptr)
-        && unsafe { has_valid_value(ptr) }
-}
-
-/// Checks that pointer `ptr` point to a valid value of type `T`.
-///
-/// For that, the pointer has to be a valid pointer according to [crate::mem] conditions 1, 2
-/// and 3,
-/// and the value stored must respect the validity invariants for type `T`.
-///
-/// Note this function succeeds for unaligned pointers. See [self::can_dereference] if you also
-/// want to check pointer alignment.
-///
-/// This function will panic today if the pointer is not null, and it points to an unallocated or
-/// deallocated memory location. This is an existing Kani limitation.
-/// See <https://github.com/model-checking/kani/issues/2690> for more details.
-#[crate::unstable(
-    feature = "mem-predicates",
-    issue = 2690,
-    reason = "experimental memory predicate API"
-)]
-#[allow(clippy::not_unsafe_ptr_arg_deref)]
-pub fn can_read_unaligned<T>(ptr: *const T) -> bool
-where
-    T: ?Sized,
-    <T as Pointee>::Metadata: PtrProperties<T>,
-{
-    let (thin_ptr, metadata) = ptr.to_raw_parts();
-    // Need to assert `is_initialized` because non-determinism is used under the hood, so it does
-    // not make sense to use it inside assumption context.
-    is_inbounds(&metadata, thin_ptr)
-        && assert_is_initialized(ptr)
-        && unsafe { has_valid_value(ptr) }
-}
-
-/// Checks that `data_ptr` points to an allocation that can hold data of size calculated from `T`.
-///
-/// This will panic if `data_ptr` points to an invalid `non_null`
-fn is_inbounds<M, T>(metadata: &M, data_ptr: *const ()) -> bool
-where
-    M: PtrProperties<T>,
-    T: ?Sized,
-{
-    let sz = metadata.pointee_size(Internal);
-    if sz == 0 {
-        true // ZST pointers are always valid including nullptr.
-    } else if data_ptr.is_null() {
-        false
-    } else {
-        // Note that this branch can't be tested in concrete execution as `is_read_ok` needs to be
-        // stubbed.
-        // We first assert that the data_ptr
-        crate::assert(
-            unsafe { is_allocated(data_ptr, 0) },
-            "Kani does not support reasoning about pointer to unallocated memory",
-        );
-        unsafe { is_allocated(data_ptr, sz) }
-    }
-}
-
-mod private {
-    /// Define like this to restrict usage of PtrProperties functions outside Kani.
-    #[derive(Copy, Clone)]
-    pub struct Internal;
-}
-
-/// Trait that allow us to extract information from pointers without de-referencing them.
-#[doc(hidden)]
-pub trait PtrProperties<T: ?Sized> {
-    fn pointee_size(&self, _: Internal) -> usize;
-
-    /// A pointer is aligned if its address is a multiple of its minimum alignment.
-    fn is_ptr_aligned(&self, ptr: *const (), internal: Internal) -> bool {
-        let min = self.min_alignment(internal);
-        ptr as usize % min == 0
-    }
-
-    fn min_alignment(&self, _: Internal) -> usize;
-
-    fn dangling(&self, _: Internal) -> *const ();
-}
-
-/// Get the information for sized types (they don't have metadata).
-impl<T> PtrProperties<T> for () {
-    fn pointee_size(&self, _: Internal) -> usize {
-        size_of::<T>()
-    }
-
-    fn min_alignment(&self, _: Internal) -> usize {
-        align_of::<T>()
-    }
-
-    fn dangling(&self, _: Internal) -> *const () {
-        NonNull::<T>::dangling().as_ptr() as *const _
-    }
-}
-
-/// Get the information from the str metadata.
-impl PtrProperties<str> for usize {
-    #[inline(always)]
-    fn pointee_size(&self, _: Internal) -> usize {
-        *self
-    }
-
-    /// String slices are a UTF-8 representation of characters that have the same layout as slices
-    /// of type [u8].
-    /// <https://doc.rust-lang.org/reference/type-layout.html#str-layout>
-    fn min_alignment(&self, _: Internal) -> usize {
-        align_of::<u8>()
-    }
-
-    fn dangling(&self, _: Internal) -> *const () {
-        NonNull::<u8>::dangling().as_ptr() as _
-    }
-}
-
-/// Get the information from the slice metadata.
-impl<T> PtrProperties<[T]> for usize {
-    fn pointee_size(&self, _: Internal) -> usize {
-        *self * size_of::<T>()
-    }
-
-    fn min_alignment(&self, _: Internal) -> usize {
-        align_of::<T>()
-    }
-
-    fn dangling(&self, _: Internal) -> *const () {
-        NonNull::<T>::dangling().as_ptr() as _
-    }
-}
-
-/// Get the information from the vtable.
-impl<T> PtrProperties<T> for DynMetadata<T>
-where
-    T: ?Sized,
-{
-    fn pointee_size(&self, _: Internal) -> usize {
-        self.size_of()
-    }
-
-    fn min_alignment(&self, _: Internal) -> usize {
-        self.align_of()
-    }
-
-    fn dangling(&self, _: Internal) -> *const () {
-        NonNull::<&T>::dangling().as_ptr() as _
-    }
-}
-
-/// Check if the pointer `_ptr` contains an allocated address of size equal or greater than `_size`.
-///
-/// # Safety
-///
-/// This function should only be called to ensure a pointer is always valid, i.e., in an assertion
-/// context.
-///
-/// I.e.: This function always returns `true` if the pointer is valid.
-/// Otherwise, it returns non-det boolean.
-#[rustc_diagnostic_item = "KaniIsAllocated"]
-#[inline(never)]
-unsafe fn is_allocated(_ptr: *const (), _size: usize) -> bool {
-    kani_intrinsic()
-}
-
-/// Check if the value stored in the given location satisfies type `T` validity requirements.
-///
-/// # Safety
-///
-/// - Users have to ensure that the pointer is aligned the pointed memory is allocated.
-#[rustc_diagnostic_item = "KaniValidValue"]
-#[inline(never)]
-unsafe fn has_valid_value<T: ?Sized>(_ptr: *const T) -> bool {
-    kani_intrinsic()
-}
-
-/// Check whether `len * size_of::<T>()` bytes are initialized starting from `ptr`.
-#[rustc_diagnostic_item = "KaniIsInitialized"]
-#[inline(never)]
-pub(crate) fn is_initialized<T: ?Sized>(_ptr: *const T) -> bool {
-    kani_intrinsic()
-}
-
-/// A helper to assert `is_initialized` to use it as a part of other predicates.
-fn assert_is_initialized<T: ?Sized>(ptr: *const T) -> bool {
-    crate::check(is_initialized(ptr), "Undefined Behavior: Reading from an uninitialized pointer");
-    true
-}
-
-/// Get the object ID of the given pointer.
-#[doc(hidden)]
-#[crate::unstable(
-    feature = "ghost-state",
-    issue = 3184,
-    reason = "experimental ghost state/shadow memory API"
-)]
-#[rustc_diagnostic_item = "KaniPointerObject"]
-#[inline(never)]
-pub fn pointer_object<T: ?Sized>(_ptr: *const T) -> usize {
-    kani_intrinsic()
-}
-
-/// Get the object offset of the given pointer.
-#[doc(hidden)]
-#[crate::unstable(
-    feature = "ghost-state",
-    issue = 3184,
-    reason = "experimental ghost state/shadow memory API"
-)]
-#[rustc_diagnostic_item = "KaniPointerOffset"]
-#[inline(never)]
-pub fn pointer_offset<T: ?Sized>(_ptr: *const T) -> usize {
-    kani_intrinsic()
-}
-
-#[cfg(test)]
-mod tests {
-    use super::{can_dereference, can_write, PtrProperties};
-    use crate::mem::private::Internal;
-    use std::fmt::Debug;
-    use std::intrinsics::size_of;
-    use std::mem::{align_of, align_of_val, size_of_val};
-    use std::ptr;
-    use std::ptr::{NonNull, Pointee};
-
-    fn size_of_t<T>(ptr: *const T) -> usize
-    where
-        T: ?Sized,
-        <T as Pointee>::Metadata: PtrProperties<T>,
-    {
-        let (_, metadata) = ptr.to_raw_parts();
-        metadata.pointee_size(Internal)
-    }
-
-    fn align_of_t<T>(ptr: *const T) -> usize
-    where
-        T: ?Sized,
-        <T as Pointee>::Metadata: PtrProperties<T>,
-    {
-        let (_, metadata) = ptr.to_raw_parts();
-        metadata.min_alignment(Internal)
-    }
-
-    #[test]
-    fn test_size_of() {
-        assert_eq!(size_of_t("hi"), size_of_val("hi"));
-        assert_eq!(size_of_t(&0u8), size_of_val(&0u8));
-        assert_eq!(size_of_t(&0u8 as *const dyn std::fmt::Display), size_of_val(&0u8));
-        assert_eq!(size_of_t(&[0u8, 1u8] as &[u8]), size_of_val(&[0u8, 1u8]));
-        assert_eq!(size_of_t(&[] as &[u8]), size_of_val::<[u8; 0]>(&[]));
-        assert_eq!(
-            size_of_t(NonNull::<u32>::dangling().as_ptr() as *const dyn std::fmt::Display),
-            size_of::<u32>()
-        );
-    }
-
-    #[test]
-    fn test_alignment() {
-        assert_eq!(align_of_t("hi"), align_of_val("hi"));
-        assert_eq!(align_of_t(&0u8), align_of_val(&0u8));
-        assert_eq!(align_of_t(&0u32 as *const dyn std::fmt::Display), align_of_val(&0u32));
-        assert_eq!(align_of_t(&[0isize, 1isize] as &[isize]), align_of_val(&[0isize, 1isize]));
-        assert_eq!(align_of_t(&[] as &[u8]), align_of_val::<[u8; 0]>(&[]));
-        assert_eq!(
-            align_of_t(NonNull::<u32>::dangling().as_ptr() as *const dyn std::fmt::Display),
-            align_of::<u32>()
-        );
-    }
-
-    #[test]
-    pub fn test_empty_slice() {
-        let slice_ptr = Vec::<char>::new().as_mut_slice() as *mut [char];
-        assert!(can_write(slice_ptr));
-    }
-
-    #[test]
-    pub fn test_empty_str() {
-        let slice_ptr = String::new().as_mut_str() as *mut str;
-        assert!(can_write(slice_ptr));
-    }
-
-    #[test]
-    fn test_dangling_zst() {
-        test_dangling_of_zst::<()>();
-        test_dangling_of_zst::<[(); 10]>();
-    }
-
-    fn test_dangling_of_zst<T>() {
-        let dangling: *mut T = NonNull::<T>::dangling().as_ptr();
-        assert!(can_write(dangling));
-
-        let vec_ptr = Vec::<T>::new().as_mut_ptr();
-        assert!(can_write(vec_ptr));
-    }
-
-    #[test]
-    fn test_null_fat_ptr() {
-        assert!(!can_dereference(ptr::null::<char>() as *const dyn Debug));
-    }
-
-    #[test]
-    fn test_null_char() {
-        assert!(!can_dereference(ptr::null::<char>()));
-    }
-
-    #[test]
-    fn test_null_mut() {
-        assert!(!can_write(ptr::null_mut::<String>()));
-    }
-}
diff --git a/library/kani_core/Cargo.toml b/library/kani_core/Cargo.toml
index ec12209f0e08..8928992c3f16 100644
--- a/library/kani_core/Cargo.toml
+++ b/library/kani_core/Cargo.toml
@@ -3,14 +3,14 @@
 
 [package]
 name = "kani_core"
-version = "0.53.0"
+version = "0.54.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
 description = "Define core constructs to use with Kani"
 
 [dependencies]
-kani_macros = { path = "../kani_macros", features = ["no_core"] }
+kani_macros = { path = "../kani_macros"}
 
 [features]
 no_core=["kani_macros/no_core"]
diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs
index b7263816800a..6cbe98d30df2 100644
--- a/library/kani_core/src/lib.rs
+++ b/library/kani_core/src/lib.rs
@@ -52,6 +52,10 @@ macro_rules! kani_lib {
         pub use kani_core::*;
         kani_core::kani_intrinsics!(std);
         kani_core::generate_arbitrary!(std);
+
+        pub mod mem {
+            kani_core::kani_mem!(std);
+        }
     };
 }
 
@@ -298,6 +302,7 @@ macro_rules! kani_intrinsics {
             loop {}
         }
 
+        #[doc(hidden)]
         pub mod internal {
             use crate::kani::Arbitrary;
             use core::ptr;
diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs
index 0b029ad53089..34cff4b17ad7 100644
--- a/library/kani_core/src/mem.rs
+++ b/library/kani_core/src/mem.rs
@@ -36,6 +36,7 @@
 //! The way Kani tracks provenance is not enough to check if the address was the result of a cast
 //! from a non-zero integer literal.
 
+#[allow(clippy::crate_in_macro_def)]
 #[macro_export]
 macro_rules! kani_mem {
     ($core:tt) => {
@@ -56,12 +57,11 @@ macro_rules! kani_mem {
         /// This function will panic today if the pointer is not null, and it points to an unallocated or
         /// deallocated memory location. This is an existing Kani limitation.
         /// See <https://github.com/model-checking/kani/issues/2690> for more details.
-        // TODO: Add this back! We might need to rename the attribute.
-        //#[crate::unstable(
-        //    feature = "mem-predicates",
-        //    issue = 2690,
-        //    reason = "experimental memory predicate API"
-        //)]
+        #[crate::kani::unstable_feature(
+            feature = "mem-predicates",
+            issue = 2690,
+            reason = "experimental memory predicate API"
+        )]
         pub fn can_write<T>(ptr: *mut T) -> bool
         where
             T: ?Sized,
@@ -84,12 +84,11 @@ macro_rules! kani_mem {
         /// This function will panic today if the pointer is not null, and it points to an unallocated or
         /// deallocated memory location. This is an existing Kani limitation.
         /// See <https://github.com/model-checking/kani/issues/2690> for more details.
-        // TODO: Add this back! We might need to rename the attribute.
-        //#[crate::unstable(
-        //    feature = "mem-predicates",
-        //    issue = 2690,
-        //    reason = "experimental memory predicate API"
-        //)]
+        #[crate::kani::unstable_feature(
+            feature = "mem-predicates",
+            issue = 2690,
+            reason = "experimental memory predicate API"
+        )]
         pub fn can_write_unaligned<T>(ptr: *const T) -> bool
         where
             T: ?Sized,
@@ -111,11 +110,11 @@ macro_rules! kani_mem {
         /// This function will panic today if the pointer is not null, and it points to an unallocated or
         /// deallocated memory location. This is an existing Kani limitation.
         /// See <https://github.com/model-checking/kani/issues/2690> for more details.
-        //#[crate::unstable(
-        //    feature = "mem-predicates",
-        //    issue = 2690,
-        //    reason = "experimental memory predicate API"
-        //)]
+        #[crate::kani::unstable_feature(
+            feature = "mem-predicates",
+            issue = 2690,
+            reason = "experimental memory predicate API"
+        )]
         #[allow(clippy::not_unsafe_ptr_arg_deref)]
         pub fn can_dereference<T>(ptr: *const T) -> bool
         where
@@ -143,12 +142,11 @@ macro_rules! kani_mem {
         /// This function will panic today if the pointer is not null, and it points to an unallocated or
         /// deallocated memory location. This is an existing Kani limitation.
         /// See <https://github.com/model-checking/kani/issues/2690> for more details.
-        // TODO: Add this back! We might need to rename the attribute.
-        //#[crate::unstable(
-        //    feature = "mem-predicates",
-        //    issue = 2690,
-        //    reason = "experimental memory predicate API"
-        //)]
+        #[crate::kani::unstable_feature(
+            feature = "mem-predicates",
+            issue = 2690,
+            reason = "experimental memory predicate API"
+        )]
         #[allow(clippy::not_unsafe_ptr_arg_deref)]
         pub fn can_read_unaligned<T>(ptr: *const T) -> bool
         where
@@ -180,7 +178,7 @@ macro_rules! kani_mem {
                 // Note that this branch can't be tested in concrete execution as `is_read_ok` needs to be
                 // stubbed.
                 // We first assert that the data_ptr
-                assert!(
+                super::assert(
                     unsafe { is_allocated(data_ptr, 0) },
                     "Kani does not support reasoning about pointer to unallocated memory",
                 );
@@ -320,30 +318,28 @@ macro_rules! kani_mem {
         }
 
         /// Get the object ID of the given pointer.
-        // TODO: Add this back later, as there is no unstable attribute here.
-        // #[doc(hidden)]
-        // #[crate::unstable(
-        //     feature = "ghost-state",
-        //     issue = 3184,
-        //     reason = "experimental ghost state/shadow memory API"
-        // )]
+        #[doc(hidden)]
+        #[crate::kani::unstable_feature(
+            feature = "ghost-state",
+            issue = 3184,
+            reason = "experimental ghost state/shadow memory API"
+        )]
         #[rustc_diagnostic_item = "KaniPointerObject"]
         #[inline(never)]
-        pub(crate) fn pointer_object<T: ?Sized>(_ptr: *const T) -> usize {
+        pub fn pointer_object<T: ?Sized>(_ptr: *const T) -> usize {
             kani_intrinsic()
         }
 
         /// Get the object offset of the given pointer.
-        // TODO: Add this back later, as there is no unstable attribute here.
-        // #[doc(hidden)]
-        // #[crate::unstable(
-        //     feature = "ghost-state",
-        //     issue = 3184,
-        //     reason = "experimental ghost state/shadow memory API"
-        // )]
+        #[doc(hidden)]
+        #[crate::kani::unstable_feature(
+            feature = "ghost-state",
+            issue = 3184,
+            reason = "experimental ghost state/shadow memory API"
+        )]
         #[rustc_diagnostic_item = "KaniPointerOffset"]
         #[inline(never)]
-        pub(crate) fn pointer_offset<T: ?Sized>(_ptr: *const T) -> usize {
+        pub fn pointer_offset<T: ?Sized>(_ptr: *const T) -> usize {
             kani_intrinsic()
         }
     };
diff --git a/library/kani_macros/Cargo.toml b/library/kani_macros/Cargo.toml
index 5917c322729e..475e2978df91 100644
--- a/library/kani_macros/Cargo.toml
+++ b/library/kani_macros/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "kani_macros"
-version = "0.53.0"
+version = "0.54.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
@@ -22,4 +22,4 @@ syn = { version = "2.0.18", features = ["full", "visit-mut", "visit", "extra-tra
 rustc_private = true
 
 [features]
-no_core = []
\ No newline at end of file
+no_core = []
diff --git a/library/std/Cargo.toml b/library/std/Cargo.toml
index ae70767f6781..9f0d09b0d7bb 100644
--- a/library/std/Cargo.toml
+++ b/library/std/Cargo.toml
@@ -5,7 +5,7 @@
 # Note: this package is intentionally named std to make sure the names of
 # standard library symbols are preserved
 name = "std"
-version = "0.53.0"
+version = "0.54.0"
 edition = "2021"
 license = "MIT OR Apache-2.0"
 publish = false
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index ab901a10d7e4..e3b6229d73c6 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-08-03"
+channel = "nightly-2024-08-07"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]
diff --git a/scripts/setup/al2/install_cbmc.sh b/scripts/setup/al2/install_cbmc.sh
index 34abcc52db93..de4b5215e083 100755
--- a/scripts/setup/al2/install_cbmc.sh
+++ b/scripts/setup/al2/install_cbmc.sh
@@ -21,10 +21,83 @@ git clone \
 
 pushd "${WORK_DIR}"
 
-mkdir build
-git submodule update --init
+# apply workaround for https://github.com/diffblue/cbmc/issues/8357 until it is
+# properly fixed in CBMC
+cat > varargs.patch << "EOF"
+--- a/src/ansi-c/library/stdio.c
++++ b/src/ansi-c/library/stdio.c
+@@ -1135,7 +1135,7 @@ int vfscanf(FILE *restrict stream, const char *restrict format, va_list arg)
 
-cmake3 -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical"
+   (void)*format;
+   while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&arg) <
+-        __CPROVER_OBJECT_SIZE(arg))
++        __CPROVER_OBJECT_SIZE(*(void **)&arg))
+   {
+     void *a = va_arg(arg, void *);
+     __CPROVER_havoc_object(a);
+@@ -1233,7 +1233,7 @@ int __stdio_common_vfscanf(
+
+   (void)*format;
+   while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&args) <
+-        __CPROVER_OBJECT_SIZE(args))
++        __CPROVER_OBJECT_SIZE(*(void **)&args))
+   {
+     void *a = va_arg(args, void *);
+     __CPROVER_havoc_object(a);
+@@ -1312,7 +1312,7 @@ __CPROVER_HIDE:;
+   (void)*s;
+   (void)*format;
+   while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&arg) <
+-        __CPROVER_OBJECT_SIZE(arg))
++        __CPROVER_OBJECT_SIZE(*(void **)&arg))
+   {
+     void *a = va_arg(arg, void *);
+     __CPROVER_havoc_object(a);
+@@ -1388,7 +1388,7 @@ int __stdio_common_vsscanf(
+   (void)*s;
+   (void)*format;
+   while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&args) <
+-        __CPROVER_OBJECT_SIZE(args))
++        __CPROVER_OBJECT_SIZE(*(void **)&args))
+   {
+     void *a = va_arg(args, void *);
+     __CPROVER_havoc_object(a);
+@@ -1774,12 +1774,12 @@ int vsnprintf(char *str, size_t size, const char *fmt, va_list ap)
+   (void)*fmt;
+
+   while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&ap) <
+-        __CPROVER_OBJECT_SIZE(ap))
++        __CPROVER_OBJECT_SIZE(*(void **)&ap))
+
+   {
+     (void)va_arg(ap, int);
+     __CPROVER_precondition(
+-      __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap),
++      __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(*(void **)&ap),
+       "vsnprintf object overlap");
+   }
+
+@@ -1822,12 +1822,12 @@ int __builtin___vsnprintf_chk(
+   (void)*fmt;
+
+   while((__CPROVER_size_t)__CPROVER_POINTER_OFFSET(*(void **)&ap) <
+-        __CPROVER_OBJECT_SIZE(ap))
++        __CPROVER_OBJECT_SIZE(*(void **)&ap))
+
+   {
+     (void)va_arg(ap, int);
+     __CPROVER_precondition(
+-      __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(ap),
++      __CPROVER_POINTER_OBJECT(str) != __CPROVER_POINTER_OBJECT(*(void **)&ap),
+       "vsnprintf object overlap");
+   }
+
+EOF
+
+cmake3 -S . -Bbuild -DWITH_JBMC=OFF -Dsat_impl="minisat2;cadical" \
+  -DCMAKE_C_COMPILER=gcc10-cc -DCMAKE_CXX_COMPILER=gcc10-c++ \
+  -DCMAKE_CXX_STANDARD_LIBRARIES=-lstdc++fs \
+  -DCMAKE_CXX_FLAGS=-Wno-error=register
 cmake3 --build build -- -j$(nproc)
 sudo make -C build install
 
diff --git a/scripts/setup/al2/install_deps.sh b/scripts/setup/al2/install_deps.sh
index 0010aa58bab4..ce901ab8afa5 100755
--- a/scripts/setup/al2/install_deps.sh
+++ b/scripts/setup/al2/install_deps.sh
@@ -11,6 +11,7 @@ set -eu
 DEPS=(
   cmake
   cmake3
+  gcc10-c++
   git
   openssl-devel
   python3-pip
diff --git a/tests/expected/dangling-ptr-println/main.rs b/tests/expected/dangling-ptr-println/main.rs
index a83afa6f8313..04328c92cb52 100644
--- a/tests/expected/dangling-ptr-println/main.rs
+++ b/tests/expected/dangling-ptr-println/main.rs
@@ -1,6 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ptr-to-ref-cast-checks
 
 //! These tests check that Kani correctly detects dangling pointer dereference inside println macro.
 //! Related issue: <https://github.com/model-checking/kani/issues/3235>.
diff --git a/tests/expected/function-contract/modifies/check_invalid_modifies.expected b/tests/expected/function-contract/modifies/check_invalid_modifies.expected
index 660430705aa2..c0ce839c3aae 100644
--- a/tests/expected/function-contract/modifies/check_invalid_modifies.expected
+++ b/tests/expected/function-contract/modifies/check_invalid_modifies.expected
@@ -1,7 +1,2 @@
-error: `&str` doesn't implement `kani::Arbitrary`\
-   -->\
-|
-|     T::any()
-|     ^^^^^^^^
-|
+error: `&str` doesn't implement `kani::Arbitrary`.
 = help: All objects in the modifies clause must implement the Arbitrary. The return type must also implement the Arbitrary trait if you are checking recursion or using verified stub.
diff --git a/tests/expected/function-contract/valid_ptr.expected b/tests/expected/function-contract/valid_ptr.expected
index 1b62781adaaf..4014a0723029 100644
--- a/tests/expected/function-contract/valid_ptr.expected
+++ b/tests/expected/function-contract/valid_ptr.expected
@@ -1,5 +1,4 @@
 Checking harness pre_condition::harness_invalid_ptr...
-Failed Checks: Kani does not support reasoning about pointer to unallocated memory
 VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected)
 
 Checking harness pre_condition::harness_stack_ptr...
diff --git a/tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs b/tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs
index 3b713a34d967..e04ac9cd3169 100644
--- a/tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs
+++ b/tests/expected/ptr_to_ref_cast/ptr_to_ref_cast.rs
@@ -1,6 +1,5 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
-// kani-flags: -Z ptr-to-ref-cast-checks
 
 //! This test case checks that raw pointer validity is checked before converting it to a reference, e.g., &(*ptr).
 
diff --git a/tests/script-based-pre/verify_std_cmd/verify_std.sh b/tests/script-based-pre/verify_std_cmd/verify_std.sh
index 3a24bf15241e..6a95c667b71b 100755
--- a/tests/script-based-pre/verify_std_cmd/verify_std.sh
+++ b/tests/script-based-pre/verify_std_cmd/verify_std.sh
@@ -51,7 +51,7 @@ cat ${TMP_DIR}/std_lib.rs >> ${TMP_DIR}/library/std/src/lib.rs
 
 echo "[TEST] Run kani verify-std"
 export RUST_BACKTRACE=1
-kani verify-std -Z unstable-options "${TMP_DIR}/library" --target-dir "${TMP_DIR}/target" -Z function-contracts -Z stubbing
+kani verify-std -Z unstable-options "${TMP_DIR}/library" --target-dir "${TMP_DIR}/target" -Z function-contracts -Z stubbing -Z mem-predicates
 
 # Cleanup
 rm -r ${TMP_DIR}
diff --git a/tests/std-checks/core/Cargo.toml b/tests/std-checks/core/Cargo.toml
index f6e1645c3a39..9cacaa1368e3 100644
--- a/tests/std-checks/core/Cargo.toml
+++ b/tests/std-checks/core/Cargo.toml
@@ -7,7 +7,7 @@ edition = "2021"
 description = "This crate contains contracts and harnesses for core library"
 
 [package.metadata.kani]
-unstable = { function-contracts = true, mem-predicates = true, ptr-to-ref-cast-checks = true }
+unstable = { function-contracts = true, mem-predicates = true }
 
 [package.metadata.kani.flags]
 output-format = "terse"
diff --git a/tests/ui/derive-arbitrary/non_arbitrary_param/expected b/tests/ui/derive-arbitrary/non_arbitrary_param/expected
index 55f12678cf9a..68e3710d6dcb 100644
--- a/tests/ui/derive-arbitrary/non_arbitrary_param/expected
+++ b/tests/ui/derive-arbitrary/non_arbitrary_param/expected
@@ -1,4 +1,4 @@
 error[E0277]: the trait bound `Void: kani::Arbitrary` is not satisfied
-    |\
-14  |     let _wrapper: Wrapper<Void> = kani::any();\
-    |                                   ^^^^^^^^^^^ the trait `kani::Arbitrary` is not implemented for `Void`, which is required by `Wrapper<Void>: kani::Arbitrary`\
+|\
+|     let _wrapper: Wrapper<Void> = kani::any();\
+|                                   ^^^^^^^^^^^ the trait `kani::Arbitrary` is not implemented for `Void`, which is required by `Wrapper<Void>: kani::Arbitrary`\
diff --git a/tools/build-kani/Cargo.toml b/tools/build-kani/Cargo.toml
index 7c8e6eef122a..cd2985e4ad68 100644
--- a/tools/build-kani/Cargo.toml
+++ b/tools/build-kani/Cargo.toml
@@ -3,7 +3,7 @@
 
 [package]
 name = "build-kani"
-version = "0.53.0"
+version = "0.54.0"
 edition = "2021"
 description = "Builds Kani, Sysroot and release bundle."
 license = "MIT OR Apache-2.0"