diff --git a/tests/cargo-kani/no-std/Cargo.toml b/tests/cargo-kani/no-std/Cargo.toml
new file mode 100644
index 000000000000..856337b180be
--- /dev/null
+++ b/tests/cargo-kani/no-std/Cargo.toml
@@ -0,0 +1,9 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "no-std"
+version = "0.1.0"
+edition = "2024"
+
+[dependencies]
diff --git a/tests/cargo-kani/no-std/expected b/tests/cargo-kani/no-std/expected
new file mode 100644
index 000000000000..9eb718272967
--- /dev/null
+++ b/tests/cargo-kani/no-std/expected
@@ -0,0 +1 @@
+Complete - 2 successfully verified harnesses, 0 failures, 2 total.
\ No newline at end of file
diff --git a/tests/cargo-kani/no-std/src/lib.rs b/tests/cargo-kani/no-std/src/lib.rs
new file mode 100644
index 000000000000..67367335645b
--- /dev/null
+++ b/tests/cargo-kani/no-std/src/lib.rs
@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Ensure that "extern crate kani" is sufficient to run Kani when no_std is enabled.
+
+#![no_std]
+extern crate kani;
+
+fn add(x: u8, y: u8) -> u8 {
+    x + y
+}
+
+#[kani::proof]
+fn prove_add() {
+    let x = kani::any_where(|n| *n < u8::MAX / 2);
+    let y = kani::any_where(|n| *n < u8::MAX / 2);
+    add(x, y);
+}
+
+use kani::cover;
+
+#[kani::proof]
+fn verify_point() {
+    cover!(true)
+}