diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs
index 8dd1c68a06e3..71faf63feaaf 100644
--- a/library/kani/src/lib.rs
+++ b/library/kani/src/lib.rs
@@ -21,6 +21,12 @@ pub mod vec;
 pub use arbitrary::Arbitrary;
 #[cfg(feature = "concrete_playback")]
 pub use concrete_playback::concrete_playback_run;
+#[cfg(not(feature = "concrete_playback"))]
+/// NOP `concrete_playback` for type checking during verification mode.
+pub fn concrete_playback_run<F: Fn()>(_: Vec<Vec<u8>>, _: F) {
+    unreachable!("Concrete playback does not work during verification")
+}
+
 pub use futures::block_on;
 
 /// Creates an assumption that will be valid after this statement run. Note that the assumption
diff --git a/tests/cargo-kani/concrete-playback-in-verification-mode/Cargo.toml b/tests/cargo-kani/concrete-playback-in-verification-mode/Cargo.toml
new file mode 100644
index 000000000000..f7e7015b1d76
--- /dev/null
+++ b/tests/cargo-kani/concrete-playback-in-verification-mode/Cargo.toml
@@ -0,0 +1,10 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "playback-test"
+version = "0.1.0"
+edition = "2018"
+
+[dependencies]
+
+[workspace]
diff --git a/tests/cargo-kani/concrete-playback-in-verification-mode/src/main.rs b/tests/cargo-kani/concrete-playback-in-verification-mode/src/main.rs
new file mode 100644
index 000000000000..773dacfa9514
--- /dev/null
+++ b/tests/cargo-kani/concrete-playback-in-verification-mode/src/main.rs
@@ -0,0 +1,14 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+#[kani::proof]
+fn main() {
+    assert!(1 == 1);
+}
+
+#[test]
+/// Purpose of this is to check if Kani can comple this code in
+/// verification mode when `kani::concrete_playback_run` is in the
+/// code,
+fn _playback_type_checks() {
+    kani::concrete_playback_run(vec![], test_sum);
+}