diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs
index 09aefa90de3..81027b987f6 100644
--- a/kani-compiler/src/kani_compiler.rs
+++ b/kani-compiler/src/kani_compiler.rs
@@ -24,12 +24,19 @@ use crate::kani_middle::check_crate_items;
 use crate::kani_queries::QueryDb;
 use crate::session::init_session;
 use clap::Parser;
+use rustc_ast::{ItemKind, UseTreeKind};
 use rustc_codegen_ssa::traits::CodegenBackend;
 use rustc_driver::{Callbacks, Compilation, run_compiler};
 use rustc_interface::Config;
 use rustc_middle::ty::TyCtxt;
 use rustc_public::rustc_internal;
 use rustc_session::config::ErrorOutputType;
+use rustc_session::parse::ParseSess;
+use rustc_span::edition::Edition;
+use rustc_span::source_map::{FileLoader, RealFileLoader};
+use rustc_span::{FileName, RealFileName};
+use std::io;
+use std::path::Path;
 use std::sync::{Arc, Mutex};
 use tracing::debug;
 
@@ -75,6 +82,70 @@ fn backend(queries: Arc<Mutex<QueryDb>>) -> Box<CodegenBackend> {
     compile_error!("No backend is available. Use `cprover` or `llbc`.");
 }
 
+struct KaniFileLoader;
+
+impl FileLoader for KaniFileLoader {
+    fn file_exists(&self, path: &Path) -> bool {
+        RealFileLoader.file_exists(path)
+    }
+
+    fn read_file(&self, path: &Path) -> io::Result<String> {
+        struct AstNoAnn;
+        impl rustc_ast_pretty::pprust::PpAnn for AstNoAnn {}
+
+        if path.ends_with("library/std/src/macros.rs") {
+            let psess = ParseSess::new(vec![]);
+            let filename = FileName::Real(RealFileName::LocalPath(path.to_owned()));
+
+            let mut module = rustc_parse::new_parser_from_source_str(
+                &psess,
+                filename.clone(),
+                RealFileLoader.read_file(path)?,
+            )
+            .unwrap()
+            .parse_crate_mod()
+            .unwrap();
+
+            // Remove definitions of macros we will overwrite.
+            module.items.retain(|item| match item.kind {
+                ItemKind::MacroDef(name, _) => {
+                    !matches!(name.as_str(), "print" | "eprint" | "println" | "eprintln" | "panic")
+                }
+                _ => true,
+            });
+
+            // Parse the macro definition overwrites and append them to the current std::macros module.
+            let macros_mod = rustc_parse::new_parser_from_source_str(
+                &psess,
+                FileName::Custom("kani-macros".to_owned()),
+                include_str!("../../library/std/src/macros.rs").to_owned(),
+            )
+            .unwrap()
+            .parse_crate_mod()
+            .unwrap()
+            .items;
+            module.items.extend(macros_mod);
+
+            Ok(rustc_ast_pretty::pprust::print_crate(
+                psess.source_map(),
+                &module,
+                filename,
+                "".to_owned(),
+                &AstNoAnn,
+                false,
+                Edition::Edition2024,
+                &psess.attr_id_generator,
+            ))
+        } else {
+            RealFileLoader.read_file(path)
+        }
+    }
+
+    fn read_binary_file(&self, path: &Path) -> io::Result<Arc<[u8]>> {
+        RealFileLoader.read_binary_file(path)
+    }
+}
+
 /// This object controls the compiler behavior.
 ///
 /// It is responsible for initializing the query database, as well as controlling the compiler
@@ -120,6 +191,40 @@ impl Callbacks for KaniCompiler {
         let queries = &mut (*self.queries.lock().unwrap());
         queries.set_args(args);
         debug!(?queries, "config end");
+
+        config.file_loader = Some(Box::new(KaniFileLoader));
+    }
+
+    fn after_crate_root_parsing(
+        &mut self,
+        compiler: &rustc_interface::interface::Compiler,
+        krate: &mut rustc_ast::Crate,
+    ) -> Compilation {
+        if compiler.sess.opts.crate_name.as_deref() == Some("std") {
+            for item in &mut krate.items {
+                if let ItemKind::Use(use_) = &mut item.kind
+                    && let [root] = &*use_.prefix.segments
+                    && root.ident.as_str() == "core"
+                    && let UseTreeKind::Nested { items, .. } = &mut use_.kind
+                {
+                    // Remove all re-exports of core macros that we overwrite to prevent conflicts.
+                    items.retain(|item| {
+                        !matches!(
+                            item.0.ident().as_str(),
+                            "assert"
+                                | "assert_eq"
+                                | "assert_ne"
+                                | "debug_assert"
+                                | "debug_assert_eq"
+                                | "debug_assert_ne"
+                                | "unreachable"
+                        )
+                    });
+                }
+            }
+        }
+
+        Compilation::Continue
     }
 
     /// After analysis, we check the crate items for Kani API misuse or configuration issues.
diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs
index a96cb297973..1c2b4ed11f6 100644
--- a/kani-compiler/src/main.rs
+++ b/kani-compiler/src/main.rs
@@ -34,6 +34,7 @@ extern crate rustc_interface;
 extern crate rustc_metadata;
 extern crate rustc_middle;
 extern crate rustc_mir_dataflow;
+extern crate rustc_parse;
 extern crate rustc_public;
 extern crate rustc_public_bridge;
 extern crate rustc_session;
diff --git a/library/std/src/lib.rs b/library/std/src/lib.rs
index dddca7978af..e1179106ac4 100644
--- a/library/std/src/lib.rs
+++ b/library/std/src/lib.rs
@@ -16,220 +16,5 @@ pub use std::*;
 // Override process calls with stubs.
 pub mod process;
 
-/// This assert macro calls kani's assert function passing it down the condition
-/// as well as a message that will be used when reporting the assertion result.
-///
-/// For the first form that does not involve a message, the macro will generate the following message:
-/// assertion failed: cond
-/// where `cond` is the stringified condition. For example, for
-/// ```rust
-/// assert!(1 + 1 == 2);
-/// ```
-/// the message will be:
-/// assertion failed: 1 + 1 == 2
-///
-/// For the second form that involves a custom message possibly with arguments,
-/// the macro will generate a message that is a concat of the custom message
-/// along with all the arguments. For example, for
-/// ```rust
-/// assert!(a + b == c, "The sum of {} and {} is {}", a, b, c);
-/// ```
-/// the assert message will be:
-/// "The sum of {} and {} is {}", a, b, c
-#[cfg(not(feature = "concrete_playback"))]
-#[macro_export]
-macro_rules! assert {
-    ($cond:expr $(,)?) => {
-        // The double negation is to resolve https://github.com/model-checking/kani/issues/2108
-        kani::assert(!!$cond, concat!("assertion failed: ", stringify!($cond)));
-    };
-    // Before edition 2021, the `assert!` macro could take a single argument
-    // that wasn't a string literal. This is not supported in edition 2021 and above.
-    // Because we reexport the 2021 edition macro, we need to support this
-    // case. For this, if there is a single argument we do the following:
-    // If it is a literal: Just pass it through and stringify it.
-    // If it isn't a literal: We add a default format
-    // specifier to the macro (see https://github.com/model-checking/kani/issues/1375).
-    ($cond:expr, $first:literal $(,)?) => {{
-        kani::assert(!!$cond, stringify!($first));
-        // Process the arguments of the assert inside an unreachable block. This
-        // is to make sure errors in the arguments (e.g. an unknown variable or
-        // an argument that does not implement the Display or Debug traits) are
-        // reported, without creating any overhead on verification performance
-        // that may arise from processing strings involved in the arguments.
-        // Note that this approach is only correct with the "abort" panic
-        // strategy, but is unsound with the "unwind" panic strategy which
-        // requires evaluating the arguments (because they might have side
-        // effects). This is fine until we add support for the "unwind" panic
-        // strategy, which is tracked in
-        // https://github.com/model-checking/kani/issues/692
-        if false {
-            kani::__kani__workaround_core_assert!(true, "{}", $first);
-        }
-    }};
-    ($cond:expr, $first:expr $(,)?) => {{
-        kani::assert(!!$cond, stringify!($first));
-        // See comment above
-        if false {
-            kani::__kani__workaround_core_assert!(true, "{}", $first);
-        }
-    }};
-    ($cond:expr, $($arg:tt)+) => {{
-        kani::assert(!!$cond, concat!(stringify!($($arg)+)));
-        // See comment above
-        if false {
-            kani::__kani__workaround_core_assert!(true, $($arg)+);
-        }
-    }};
-}
-
-// Override the assert_eq and assert_ne macros to
-// 1. Bypass the formatting-related code in the standard library implementation,
-//    which is not relevant for verification (see
-//    https://github.com/model-checking/kani/issues/14)
-// 2. Generate a suitable message for the assert of the form:
-//        assertion failed: $left == $right
-//    instead of the uninformative:
-//        a panicking function core::panicking::assert_failed is invoked
-//    (see https://github.com/model-checking/kani/issues/13)
-// 3. Call kani::assert so that any instrumentation that it does (e.g. injecting
-//    reachability checks) is done for assert_eq and assert_ne
-#[cfg(not(feature = "concrete_playback"))]
-#[macro_export]
-macro_rules! assert_eq {
-    ($left:expr, $right:expr $(,)?) => ({
-        // Add parentheses around the operands to avoid a "comparison operators
-        // cannot be chained" error, but exclude the parentheses in the message
-        kani::assert(($left) == ($right), concat!("assertion failed: ", stringify!($left == $right)));
-    });
-    ($left:expr, $right:expr, $($arg:tt)+) => ({
-        assert!(($left) == ($right), $($arg)+);
-    });
-}
-
-#[cfg(not(feature = "concrete_playback"))]
-#[macro_export]
-macro_rules! assert_ne {
-    ($left:expr, $right:expr $(,)?) => ({
-        // Add parentheses around the operands to avoid a "comparison operators
-        // cannot be chained" error, but exclude the parentheses in the message
-        kani::assert(($left) != ($right), concat!("assertion failed: ", stringify!($left != $right)));
-    });
-    ($left:expr, $right:expr, $($arg:tt)+) => ({
-        assert!(($left) != ($right), $($arg)+);
-    });
-}
-
-// Treat the debug assert macros same as non-debug ones
-#[cfg(not(feature = "concrete_playback"))]
-#[macro_export]
-macro_rules! debug_assert {
-    ($($x:tt)*) => ({ if cfg!(debug_assertions) { $crate::assert!($($x)*); } })
-}
-
-#[cfg(not(feature = "concrete_playback"))]
-#[macro_export]
-macro_rules! debug_assert_eq {
-    ($($x:tt)*) => ({ if cfg!(debug_assertions) { $crate::assert_eq!($($x)*); } })
-}
-
-#[cfg(not(feature = "concrete_playback"))]
-#[macro_export]
-macro_rules! debug_assert_ne {
-    ($($x:tt)*) => ({ if cfg!(debug_assertions) { $crate::assert_ne!($($x)*); } })
-}
-
-// Override the print macros to skip all the printing functionality (which
-// is not relevant for verification)
-#[cfg(not(feature = "concrete_playback"))]
-#[macro_export]
-macro_rules! print {
-    ($($x:tt)*) => {{ let _ = format_args!($($x)*); }};
-}
-
-#[cfg(not(feature = "concrete_playback"))]
-#[macro_export]
-macro_rules! eprint {
-    ($($x:tt)*) => {{ let _ = format_args!($($x)*); }};
-}
-
-#[cfg(not(feature = "concrete_playback"))]
-#[macro_export]
-macro_rules! println {
-    () => { $crate::print!("\n") };
-    ($($x:tt)*) => {{ let _ = format_args!($($x)*); }};
-}
-
-#[cfg(not(feature = "concrete_playback"))]
-#[macro_export]
-macro_rules! eprintln {
-    () => { $crate::eprint!("\n") };
-    ($($x:tt)*) => {{ let _ = format_args!($($x)*); }};
-}
-
-#[cfg(not(feature = "concrete_playback"))]
-#[macro_export]
-macro_rules! unreachable {
-    // The argument, if present, is a literal that represents the error message, i.e.:
-    // `unreachable!("Error message")` or `unreachable!()`
-    ($($msg:literal)? $(,)?) => (
-        kani::panic(concat!("internal error: entered unreachable code: ", $($msg)?))
-    );
-    // The argument is an expression, such as a variable.
-    // ```
-    // let msg = format!("Error: {}", code);
-    // unreachable!(msg);
-    // ```
-    // This was supported for 2018 and older rust editions.
-    // TODO: Is it possible to trigger an error if 2021 and above?
-    // https://github.com/model-checking/kani/issues/1375
-    ($($msg:expr)? $(,)?) => (
-        kani::panic(concat!("internal error: entered unreachable code: ", stringify!($($msg)?)))
-    );
-    // The first argument is the format and the rest contains tokens to be included in the msg.
-    // `unreachable!("Error: {}", code);`
-    // We have the same issue as with panic!() described bellow where we over-approx what we can
-    // handle.
-    ($fmt:expr, $($arg:tt)*) => {{
-        if false {
-            kani::__kani__workaround_core_assert!(true, $fmt, $($arg)+);
-        }
-        kani::panic(concat!("internal error: entered unreachable code: ",
-        stringify!($fmt, $($arg)*)))}};
-}
-
-#[cfg(not(feature = "concrete_playback"))]
-#[macro_export]
-macro_rules! panic {
-    // No argument is given.
-    () => (
-        kani::panic("explicit panic")
-    );
-    // The argument is a literal that represents the error message, i.e.:
-    // `panic!("Error message")`
-    ($msg:literal $(,)?) => ({
-        if false {
-            kani::__kani__workaround_core_assert!(true, $msg);
-        }
-        kani::panic(concat!($msg))
-    });
-    // The argument is an expression, such as a variable.
-    // ```
-    // let msg = format!("Error: {}", code);
-    // panic!(msg);
-    // ```
-    // This was supported for 2018 and older rust editions.
-    // TODO: Is it possible to trigger an error if 2021 and above?
-    // https://github.com/model-checking/kani/issues/1375
-    ($msg:expr $(,)?) => ({
-        kani::panic(stringify!($msg));
-    });
-    // All other cases, e.g.:
-    // `panic!("Error: {}", code);`
-    ($($arg:tt)+) => {{
-        if false {
-            kani::__kani__workaround_core_assert!(true, $($arg)+);
-        }
-        kani::panic(stringify!($($arg)+));
-    }};
-}
+#[macro_use]
+mod macros;
diff --git a/library/std/src/macros.rs b/library/std/src/macros.rs
new file mode 100644
index 00000000000..e5d793d17eb
--- /dev/null
+++ b/library/std/src/macros.rs
@@ -0,0 +1,232 @@
+pub extern crate core;
+pub extern crate kani;
+
+/// This assert macro calls kani's assert function passing it down the condition
+/// as well as a message that will be used when reporting the assertion result.
+///
+/// For the first form that does not involve a message, the macro will generate the following message:
+/// assertion failed: cond
+/// where `cond` is the stringified condition. For example, for
+/// ```rust
+/// assert!(1 + 1 == 2);
+/// ```
+/// the message will be:
+/// assertion failed: 1 + 1 == 2
+///
+/// For the second form that involves a custom message possibly with arguments,
+/// the macro will generate a message that is a concat of the custom message
+/// along with all the arguments. For example, for
+/// ```rust
+/// assert!(a + b == c, "The sum of {} and {} is {}", a, b, c);
+/// ```
+/// the assert message will be:
+/// "The sum of {} and {} is {}", a, b, c
+#[cfg(not(feature = "concrete_playback"))]
+#[stable(feature = "rust1", since = "1.0.0")]
+#[macro_export]
+macro_rules! assert {
+    ($cond:expr $(,)?) => {
+        // The double negation is to resolve https://github.com/model-checking/kani/issues/2108
+        $crate::macros::kani::assert(!!$cond, concat!("assertion failed: ", stringify!($cond)));
+    };
+    // Before edition 2021, the `assert!` macro could take a single argument
+    // that wasn't a string literal. This is not supported in edition 2021 and above.
+    // Because we reexport the 2021 edition macro, we need to support this
+    // case. For this, if there is a single argument we do the following:
+    // If it is a literal: Just pass it through and stringify it.
+    // If it isn't a literal: We add a default format
+    // specifier to the macro (see https://github.com/model-checking/kani/issues/1375).
+    ($cond:expr, $first:literal $(,)?) => {{
+        $crate::macros::kani::assert(!!$cond, stringify!($first));
+        // Process the arguments of the assert inside an unreachable block. This
+        // is to make sure errors in the arguments (e.g. an unknown variable or
+        // an argument that does not implement the Display or Debug traits) are
+        // reported, without creating any overhead on verification performance
+        // that may arise from processing strings involved in the arguments.
+        // Note that this approach is only correct with the "abort" panic
+        // strategy, but is unsound with the "unwind" panic strategy which
+        // requires evaluating the arguments (because they might have side
+        // effects). This is fine until we add support for the "unwind" panic
+        // strategy, which is tracked in
+        // https://github.com/model-checking/kani/issues/692
+        if false {
+            $crate::macros::core::assert!(true, "{}", $first);
+        }
+    }};
+    ($cond:expr, $first:expr $(,)?) => {{
+        $crate::macros::kani::assert(!!$cond, stringify!($first));
+        // See comment above
+        if false {
+            $crate::macros::core::assert!(true, "{}", $first);
+        }
+    }};
+    ($cond:expr, $($arg:tt)+) => {{
+        $crate::macros::kani::assert(!!$cond, concat!(stringify!($($arg)+)));
+        // See comment above
+        if false {
+            $crate::macros::core::assert!(true, $($arg)+);
+        }
+    }};
+}
+
+// Override the assert_eq and assert_ne macros to
+// 1. Bypass the formatting-related code in the standard library implementation,
+//    which is not relevant for verification (see
+//    https://github.com/model-checking/kani/issues/14)
+// 2. Generate a suitable message for the assert of the form:
+//        assertion failed: $left == $right
+//    instead of the uninformative:
+//        a panicking function core::panicking::assert_failed is invoked
+//    (see https://github.com/model-checking/kani/issues/13)
+// 3. Call kani::assert so that any instrumentation that it does (e.g. injecting
+//    reachability checks) is done for assert_eq and assert_ne
+#[cfg(not(feature = "concrete_playback"))]
+#[stable(feature = "rust1", since = "1.0.0")]
+#[macro_export]
+macro_rules! assert_eq {
+    ($left:expr, $right:expr $(,)?) => ({
+        // Add parentheses around the operands to avoid a "comparison operators
+        // cannot be chained" error, but exclude the parentheses in the message
+        $crate::macros::kani::assert(($left) == ($right), concat!("assertion failed: ", stringify!($left == $right)));
+    });
+    ($left:expr, $right:expr, $($arg:tt)+) => ({
+        assert!(($left) == ($right), $($arg)+);
+    });
+}
+
+#[cfg(not(feature = "concrete_playback"))]
+#[stable(feature = "rust1", since = "1.0.0")]
+#[macro_export]
+macro_rules! assert_ne {
+    ($left:expr, $right:expr $(,)?) => ({
+        // Add parentheses around the operands to avoid a "comparison operators
+        // cannot be chained" error, but exclude the parentheses in the message
+        $crate::macros::kani::assert(($left) != ($right), concat!("assertion failed: ", stringify!($left != $right)));
+    });
+    ($left:expr, $right:expr, $($arg:tt)+) => ({
+        assert!(($left) != ($right), $($arg)+);
+    });
+}
+
+// Treat the debug assert macros same as non-debug ones
+#[cfg(not(feature = "concrete_playback"))]
+#[stable(feature = "rust1", since = "1.0.0")]
+#[macro_export]
+macro_rules! debug_assert {
+    ($($x:tt)*) => ({ if cfg!(debug_assertions) { $crate::assert!($($x)*); } })
+}
+
+#[cfg(not(feature = "concrete_playback"))]
+#[stable(feature = "rust1", since = "1.0.0")]
+#[macro_export]
+macro_rules! debug_assert_eq {
+    ($($x:tt)*) => ({ if cfg!(debug_assertions) { $crate::assert_eq!($($x)*); } })
+}
+
+#[cfg(not(feature = "concrete_playback"))]
+#[stable(feature = "rust1", since = "1.0.0")]
+#[macro_export]
+macro_rules! debug_assert_ne {
+    ($($x:tt)*) => ({ if cfg!(debug_assertions) { $crate::assert_ne!($($x)*); } })
+}
+
+// Override the print macros to skip all the printing functionality (which
+// is not relevant for verification)
+#[cfg(not(feature = "concrete_playback"))]
+#[stable(feature = "rust1", since = "1.0.0")]
+#[macro_export]
+macro_rules! print {
+    ($($x:tt)*) => {{ let _ = format_args!($($x)*); }};
+}
+
+#[cfg(not(feature = "concrete_playback"))]
+#[stable(feature = "rust1", since = "1.0.0")]
+#[macro_export]
+macro_rules! eprint {
+    ($($x:tt)*) => {{ let _ = format_args!($($x)*); }};
+}
+
+#[cfg(not(feature = "concrete_playback"))]
+#[stable(feature = "rust1", since = "1.0.0")]
+#[macro_export]
+macro_rules! println {
+    () => { $crate::print!("\n") };
+    ($($x:tt)*) => {{ let _ = format_args!($($x)*); }};
+}
+
+#[cfg(not(feature = "concrete_playback"))]
+#[stable(feature = "rust1", since = "1.0.0")]
+#[macro_export]
+macro_rules! eprintln {
+    () => { $crate::eprint!("\n") };
+    ($($x:tt)*) => {{ let _ = format_args!($($x)*); }};
+}
+
+#[cfg(not(feature = "concrete_playback"))]
+#[stable(feature = "rust1", since = "1.0.0")]
+#[macro_export]
+macro_rules! unreachable {
+    // The argument, if present, is a literal that represents the error message, i.e.:
+    // `unreachable!("Error message")` or `unreachable!()`
+    ($($msg:literal)? $(,)?) => (
+        $crate::macros::kani::panic(concat!("internal error: entered unreachable code: ", $($msg)?))
+    );
+    // The argument is an expression, such as a variable.
+    // ```
+    // let msg = format!("Error: {}", code);
+    // unreachable!(msg);
+    // ```
+    // This was supported for 2018 and older rust editions.
+    // TODO: Is it possible to trigger an error if 2021 and above?
+    // https://github.com/model-checking/kani/issues/1375
+    ($($msg:expr)? $(,)?) => (
+        $crate::macros::kani::panic(concat!("internal error: entered unreachable code: ", stringify!($($msg)?)))
+    );
+    // The first argument is the format and the rest contains tokens to be included in the msg.
+    // `unreachable!("Error: {}", code);`
+    // We have the same issue as with panic!() described bellow where we over-approx what we can
+    // handle.
+    ($fmt:expr, $($arg:tt)*) => {{
+        if false {
+            $crate::macros::core::assert!(true, $fmt, $($arg)+);
+        }
+        $crate::macros::kani::panic(concat!("internal error: entered unreachable code: ",
+        stringify!($fmt, $($arg)*)))}};
+}
+
+#[cfg(not(feature = "concrete_playback"))]
+#[stable(feature = "rust1", since = "1.0.0")]
+#[macro_export]
+macro_rules! panic {
+    // No argument is given.
+    () => (
+        $crate::macros::kani::panic("explicit panic")
+    );
+    // The argument is a literal that represents the error message, i.e.:
+    // `panic!("Error message")`
+    ($msg:literal $(,)?) => ({
+        if false {
+            $crate::macros::core::assert!(true, $msg);
+        }
+        $crate::macros::kani::panic(concat!($msg))
+    });
+    // The argument is an expression, such as a variable.
+    // ```
+    // let msg = format!("Error: {}", code);
+    // panic!(msg);
+    // ```
+    // This was supported for 2018 and older rust editions.
+    // TODO: Is it possible to trigger an error if 2021 and above?
+    // https://github.com/model-checking/kani/issues/1375
+    ($msg:expr $(,)?) => ({
+        $crate::macros::kani::panic(stringify!($msg));
+    });
+    // All other cases, e.g.:
+    // `panic!("Error: {}", code);`
+    ($($arg:tt)+) => {{
+        if false {
+            $crate::macros::core::assert!(true, $($arg)+);
+        }
+        $crate::macros::kani::panic(stringify!($($arg)+));
+    }};
+}