diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
index 37fa11cb59c4..cf428c44dbb4 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
@@ -306,9 +306,23 @@ impl CodegenBackend for GotocCodegenBackend {
             if queries.args().reachability_analysis != ReachabilityType::None
                 && queries.kani_functions().is_empty()
             {
-                tcx.sess.dcx().err(
-                    "Failed to detect Kani functions. Please check your installation is correct.",
-                );
+                if stable_mir::find_crates("std").is_empty()
+                    && stable_mir::find_crates("kani").is_empty()
+                {
+                    // Special error for when not importing kani and using #[no_std].
+                    // See here for more info: https://github.com/model-checking/kani/issues/3906#issuecomment-2932687768.
+                    tcx.sess.dcx().struct_err(
+                        "Failed to detect Kani functions."
+                    ).with_help(
+                        "This project seems to be using #[no_std] but does not import Kani. \
+                        Try adding `crate extern kani` to the crate root to explicitly import Kani."
+                    )
+                    .emit();
+                } else {
+                    tcx.sess.dcx().struct_err(
+                        "Failed to detect Kani functions. Please check your installation is correct."
+                    ).emit();
+                }
             }
 
             // Codegen all items that need to be processed according to the selected reachability mode:
diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs
index f1d064ed08eb..c489654c0249 100644
--- a/kani-compiler/src/kani_middle/kani_functions.rs
+++ b/kani-compiler/src/kani_middle/kani_functions.rs
@@ -269,5 +269,9 @@ pub fn validate_kani_functions(kani_funcs: &HashMap<KaniFunction, FnDef>) {
             missing += 1;
         }
     }
-    assert_eq!(missing, 0, "Failed to find `{missing}` Kani functions");
+    // If this is failing for #[no_std] crates, try explicitly adding `extern crate kani` to the crate root.
+    // See https://github.com/model-checking/kani/issues/3906 for why this is required.
+    if missing != 0 {
+        tracing::error!("Failed to find `{missing}` Kani functions")
+    }
 }
diff --git a/tests/cargo-ui/no-std-no-kani/Cargo.toml b/tests/cargo-ui/no-std-no-kani/Cargo.toml
new file mode 100644
index 000000000000..2d50643feeaa
--- /dev/null
+++ b/tests/cargo-ui/no-std-no-kani/Cargo.toml
@@ -0,0 +1,9 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "no-std-help"
+version = "0.1.0"
+edition = "2024"
+
+[dependencies]
diff --git a/tests/cargo-ui/no-std-no-kani/expected b/tests/cargo-ui/no-std-no-kani/expected
new file mode 100644
index 000000000000..4dbe890092f8
--- /dev/null
+++ b/tests/cargo-ui/no-std-no-kani/expected
@@ -0,0 +1,3 @@
+error: Failed to detect Kani functions.\
+  |\
+  = help: This project seems to be using #[no_std] but does not import Kani. Try adding `crate extern kani` to the crate root to explicitly import Kani.
\ No newline at end of file
diff --git a/tests/cargo-ui/no-std-no-kani/src/lib.rs b/tests/cargo-ui/no-std-no-kani/src/lib.rs
new file mode 100644
index 000000000000..92356330addc
--- /dev/null
+++ b/tests/cargo-ui/no-std-no-kani/src/lib.rs
@@ -0,0 +1,10 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Ensure that a no_std crate with no harnesses & no "extern crate kani" gets a useful error message.
+
+#![no_std]
+
+fn add(x: u8, y: u8) -> u8 {
+    x + y
+}