diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs
index 3f2b3d0c7722..312f59261f81 100644
--- a/kani-compiler/src/kani_compiler.rs
+++ b/kani-compiler/src/kani_compiler.rs
@@ -24,12 +24,18 @@ use crate::kani_middle::check_crate_items;
 use crate::kani_queries::QUERY_DB;
 use crate::session::init_session;
 use clap::Parser;
+use rustc_ast::{ast, attr};
 use rustc_codegen_ssa::traits::CodegenBackend;
 use rustc_driver::{Callbacks, Compilation, run_compiler};
 use rustc_interface::Config;
+use rustc_interface::interface::Compiler;
 use rustc_middle::ty::TyCtxt;
+use rustc_parse::lexer::StripTokens;
+use rustc_parse::new_parser_from_source_str;
+use rustc_parse::parser::ForceCollect;
 use rustc_public::rustc_internal;
 use rustc_session::config::ErrorOutputType;
+use rustc_span::{FileName, sym};
 use tracing::debug;
 
 /// Run the Kani flavour of the compiler.
@@ -84,12 +90,17 @@ fn backend(args: Arguments) -> Box<CodegenBackend> {
 ///
 /// It is responsible for initializing the query database, as well as controlling the compiler
 /// state machine.
-struct KaniCompiler {}
+struct KaniCompiler {
+    /// Whether we are currently building the standard library. When set, Kani's
+    /// macro overrides are not injected (the macros are defined in the standard
+    /// library being built, and `kani` is not available).
+    build_std: bool,
+}
 
 impl KaniCompiler {
     /// Create a new [KaniCompiler] instance.
     pub fn new() -> KaniCompiler {
-        KaniCompiler {}
+        KaniCompiler { build_std: false }
     }
 
     /// Compile the current crate with the given arguments.
@@ -112,6 +123,10 @@ impl Callbacks for KaniCompiler {
         let args = Arguments::parse_from(args);
         init_session(&args, matches!(config.opts.error_format, ErrorOutputType::Json { .. }));
 
+        // Remember whether we are building the standard library so that
+        // `after_crate_root_parsing` can decide whether to inject Kani's macro overrides.
+        self.build_std = args.build_std;
+
         // Capture args in the closure so they're available when the backend is created
         // (potentially on a different thread).
         config.make_codegen_backend = Some(Box::new({
@@ -120,6 +135,47 @@ impl Callbacks for KaniCompiler {
         }));
     }
 
+    /// Inject Kani's macro overrides into every (non-`#![no_std]`) crate we compile.
+    ///
+    /// Kani overrides several `core`/`std` macros (e.g. `assert_eq!` without a
+    /// `Debug` bound, `panic!` with Kani-specific message handling, reachability
+    /// instrumentation for `assert!`). These overrides are intentionally kept out of
+    /// the standard-library prelude: since they are `core`-prelude macros, placing
+    /// them there makes `#![no_std]` dependencies that import `std`'s prelude
+    /// explicitly (`extern crate std; use std::prelude::v1::*;`, e.g. `lazy_static`)
+    /// ambiguous against the auto-injected `core` prelude, which is a hard error
+    /// (rust-lang/rust E0659).
+    ///
+    /// Instead we bring the overrides into scope crate-wide by injecting a
+    /// `#[macro_use]`d re-import of the standard library. This is applied to every
+    /// crate Kani codegens — dependencies included, so that their assertions get the
+    /// same instrumentation and messages as the crate under verification — except:
+    ///  - when building the standard library itself (the macros live there and `kani`
+    ///    is not available), and
+    ///  - `#![no_std]`/`#![no_core]` crates, which must not gain an `extern crate std`
+    ///    (and which is exactly the case that would otherwise hit E0659).
+    ///
+    /// A `#![no_std]` dependency therefore keeps the regular `core` macros. This is
+    /// sound: Kani still intercepts the panics they lower to during codegen.
+    fn after_crate_root_parsing(
+        &mut self,
+        compiler: &Compiler,
+        krate: &mut ast::Crate,
+    ) -> Compilation {
+        if !self.build_std
+            && !attr::contains_name(&krate.attrs, sym::no_std)
+            && !attr::contains_name(&krate.attrs, sym::no_core)
+            // Only inject when an external `std` is available to import. The
+            // `verify-std` flow builds `std` itself (no `--extern std`), so
+            // injecting `extern crate std` there would pull in a *second* `std`
+            // (and `core`), causing duplicate-lang-item errors (E0152).
+            && compiler.sess.opts.externs.get("std").is_some()
+        {
+            inject_kani_macro_overrides(compiler, krate);
+        }
+        Compilation::Continue
+    }
+
     /// After analysis, we check the crate items for Kani API misuse or configuration issues.
     fn after_analysis(
         &mut self,
@@ -134,3 +190,41 @@ impl Callbacks for KaniCompiler {
         Compilation::Continue
     }
 }
+
+/// Inject `#[macro_use] extern crate std as _kani_std_macros;` at the crate root so
+/// that Kani's `#[macro_export]`ed overrides (`assert!`, `assert_eq!`, `panic!`, …)
+/// shadow the corresponding `std`/`core` prelude macros throughout the crate,
+/// including nested modules.
+///
+/// A `#[macro_use]` extern crate places the macros in the higher-priority
+/// "`macro_use` prelude" scope, so unlike a glob `use` (which would conflict with the
+/// standard prelude, rust-lang/rust E0659) this shadows the prelude macros without
+/// ambiguity. The crate is aliased (`as _kani_std_macros`) to avoid clashing with the
+/// compiler-injected `extern crate std`.
+fn inject_kani_macro_overrides(compiler: &Compiler, krate: &mut ast::Crate) {
+    let psess = &compiler.sess.psess;
+    let source = "#[allow(unused_extern_crates, unused_imports)]\n\
+                  #[macro_use]\n\
+                  extern crate std as _kani_std_macros;\n"
+        .to_string();
+    let filename = FileName::Custom("kani_macro_overrides".to_string());
+    let mut parser = match new_parser_from_source_str(psess, filename, source, StripTokens::Nothing)
+    {
+        Ok(parser) => parser,
+        Err(errors) => {
+            // This is an internal, statically-known source string, so a parse error
+            // indicates a Kani bug rather than a user error.
+            for error in errors {
+                error.emit();
+            }
+            return;
+        }
+    };
+    match parser.parse_item(ForceCollect::No) {
+        Ok(Some(item)) => krate.items.insert(0, item),
+        Ok(None) => unreachable!("failed to parse Kani's macro-override injection"),
+        Err(error) => {
+            error.emit();
+        }
+    }
+}
diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs
index bfe9647fff5c..cf00140c348c 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 dddca7978afa..915f7275ea15 100644
--- a/library/std/src/lib.rs
+++ b/library/std/src/lib.rs
@@ -16,6 +16,50 @@ pub use std::*;
 // Override process calls with stubs.
 pub mod process;
 
+// The standard prelude explicitly re-exports the built-in macros
+// (rust-lang/rust "Explicitly export core and std macros"), rather than
+// injecting them via `#[macro_use] extern crate std`. Because `pub use std::*`
+// above also re-exports `std::prelude`, user code would otherwise pick up the
+// *original* `println!`/`assert!`/... from the std prelude and ignore the
+// overrides defined below. Provide our own `prelude` (which shadows the glob
+// re-export) that re-exports Kani's versions of the overridden macros. Explicit
+// `use` imports take precedence over the `pub use std::prelude::...::*` globs,
+// so only the overridden macros are replaced; everything else comes from std.
+#[cfg(not(feature = "concrete_playback"))]
+pub mod prelude {
+    // The standard prelude is kept free of Kani's `assert`/`debug_assert`/
+    // `unreachable`/`panic` overrides: those are core-prelude macros, and putting
+    // Kani's versions here makes `#![no_std]` dependencies that import this prelude
+    // explicitly (`extern crate std; use std::prelude::v1::*;`, e.g. lazy_static)
+    // ambiguous against the injected core prelude (E0659). Instead, kani-compiler
+    // injects those overrides only into the crate under verification (see
+    // kani_compiler's macro-override injection). The print family is defined in this
+    // crate (std) with no core-prelude counterpart, so overriding it here is safe and
+    // applies everywhere (dependencies included), which is important so that a
+    // dependency's `println!` does not run real formatting/IO during verification.
+    pub mod v1 {
+        pub use crate::{eprint, eprintln, print, println};
+        pub use std::prelude::v1::*;
+    }
+    pub mod rust_2015 {
+        pub use super::v1::*;
+    }
+    pub mod rust_2018 {
+        pub use super::v1::*;
+    }
+    pub mod rust_2021 {
+        pub use super::v1::*;
+        pub use core::prelude::rust_2021::*;
+        // Both globs bring `panic` (std's vs core's); prefer std's, matching std's own prelude.
+        pub use super::v1::panic;
+    }
+    pub mod rust_2024 {
+        pub use super::v1::panic;
+        pub use super::v1::*;
+        pub use core::prelude::rust_2024::*;
+    }
+}
+
 /// 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.
 ///
diff --git a/rust-toolchain.toml b/rust-toolchain.toml
index c9177213cbc8..28210e92579a 100644
--- a/rust-toolchain.toml
+++ b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2026-01-13"
+channel = "nightly-2026-01-14"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]