diff --git a/Cargo.toml b/Cargo.toml
index 1f6896e1a1a4..7a97b0bb791e 100644
--- a/Cargo.toml
+++ b/Cargo.toml
@@ -66,4 +66,5 @@ exclude = [
   "tests/cargo-ui",
   "tests/slow",
   "tests/assess-scan-test-scaffold",
+  "tests/script-based-pre",
 ]
diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
index 11ba4916025d..1fac5cc56674 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
@@ -81,6 +81,10 @@ impl CodegenBackend for GotocCodegenBackend {
         provide::provide_extern(providers);
     }
 
+    fn print_version(&self) {
+        println!("Kani-goto version: {}", env!("CARGO_PKG_VERSION"));
+    }
+
     fn codegen_crate(
         &self,
         tcx: TyCtxt,
diff --git a/kani-compiler/src/parser.rs b/kani-compiler/src/parser.rs
index c34f27baf0f4..0704a45d5b1d 100644
--- a/kani-compiler/src/parser.rs
+++ b/kani-compiler/src/parser.rs
@@ -46,12 +46,6 @@ pub const ENABLE_STUBBING: &str = "enable-stubbing";
 /// Configure command options for the Kani compiler.
 pub fn parser() -> Command {
     let app = command!()
-        .arg(
-            Arg::new("kani-compiler-version")
-                .short('?')
-                .action(ArgAction::Version)
-                .help("Gets `kani-compiler` version."),
-        )
         .arg(
             Arg::new(KANI_LIB)
                 .long(KANI_LIB)
@@ -137,6 +131,12 @@ pub fn parser() -> Command {
                 .help("Instruct the compiler to perform stubbing.")
                 .requires(HARNESS)
                 .action(ArgAction::SetTrue),
+        )
+        .arg(
+            Arg::new("check-version")
+                .long("check-version")
+                .action(ArgAction::Set)
+                .help("Pass the kani version to the compiler to ensure cache coherence."),
         );
     #[cfg(feature = "unsound_experiments")]
     let app = crate::unsound_experiments::arg_parser::add_unsound_experiments_to_parser(app);
diff --git a/kani-driver/src/args.rs b/kani-driver/src/args.rs
index 6def7979317c..43870e05c275 100644
--- a/kani-driver/src/args.rs
+++ b/kani-driver/src/args.rs
@@ -113,6 +113,10 @@ pub struct KaniArgs {
     #[arg(long)]
     pub target_dir: Option<PathBuf>,
 
+    /// Force Kani to rebuild all packages before the verification.
+    #[arg(long)]
+    pub force_build: bool,
+
     /// Toggle between different styles of output
     #[arg(long, default_value = "regular", ignore_case = true, value_enum)]
     pub output_format: OutputFormat,
diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs
index c73d2a1bbdd2..27694ffa4f3a 100644
--- a/kani-driver/src/call_cargo.rs
+++ b/kani-driver/src/call_cargo.rs
@@ -51,9 +51,7 @@ impl KaniSession {
             .join("kani");
         let outdir = target_dir.join(build_target).join("debug/deps");
 
-        // Clean directory before building since we are unable to handle cache today.
-        // TODO: https://github.com/model-checking/kani/issues/1736
-        if target_dir.exists() {
+        if self.args.force_build && target_dir.exists() {
             fs::remove_dir_all(&target_dir)?;
         }
 
diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs
index d1691ee5a6e7..704f909c1d66 100644
--- a/kani-driver/src/call_single_file.rs
+++ b/kani-driver/src/call_single_file.rs
@@ -66,7 +66,7 @@ impl KaniSession {
 
     /// These arguments are arguments passed to kani-compiler that are `kani` compiler specific.
     pub fn kani_compiler_flags(&self) -> Vec<String> {
-        let mut flags = vec![];
+        let mut flags = vec![check_version()];
 
         if self.args.debug {
             flags.push("--log-level=debug".into());
@@ -187,3 +187,11 @@ impl KaniSession {
 pub fn to_rustc_arg(kani_args: Vec<String>) -> String {
     format!(r#"-Cllvm-args={}"#, kani_args.join(" "))
 }
+
+/// Function that returns a `--check-version` argument to be added to the compiler flags.
+/// This is really just used to force the compiler to recompile everything from scratch when a user
+/// upgrades Kani. Cargo currently ignores the codegen backend version.
+/// See <https://github.com/model-checking/kani/issues/2140> for more context.
+fn check_version() -> String {
+    format!("--check-version={}", env!("CARGO_PKG_VERSION"))
+}
diff --git a/tests/cargo-ui/supported-lib-types/lib-rlib/Cargo.toml b/tests/cargo-ui/supported-lib-types/lib-rlib/Cargo.toml
index 7434f1c27f5f..1b4066c265ef 100644
--- a/tests/cargo-ui/supported-lib-types/lib-rlib/Cargo.toml
+++ b/tests/cargo-ui/supported-lib-types/lib-rlib/Cargo.toml
@@ -10,3 +10,16 @@ description = "Test that Kani correctly handle supported crate types"
 name = "lib"
 crate-type = ["lib", "rlib"]
 path = "../src/lib.rs"
+
+[package.metadata.kani.flags]
+# This test doesn't work with the cache due to naming conflict caused by
+# declaring ["lib", "rlib"] which is in fact redundant.
+# See https://github.com/rust-lang/cargo/issues/6313 for more details.
+#
+# This still works for a fresh build and it only prints a warning. Thus, we
+# force rebuild for now.
+#
+# Note that support for this case is deprecated. AFAIK, there is no plan to fix
+# cargo build cache for cases like this. Until then, we might as well check that
+# our support level matches cargo's.
+force-build = true
diff --git a/tests/script-based-pre/build-cache-bin/bin/Cargo.toml b/tests/script-based-pre/build-cache-bin/bin/Cargo.toml
new file mode 100644
index 000000000000..53ef8b4ced03
--- /dev/null
+++ b/tests/script-based-pre/build-cache-bin/bin/Cargo.toml
@@ -0,0 +1,6 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "bin"
+version = "0.1.0"
+edition = "2021"
diff --git a/tests/script-based-pre/build-cache-bin/bin/src/lib.rs b/tests/script-based-pre/build-cache-bin/bin/src/lib.rs
new file mode 100644
index 000000000000..8f4468728cac
--- /dev/null
+++ b/tests/script-based-pre/build-cache-bin/bin/src/lib.rs
@@ -0,0 +1,18 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+#[kani::proof]
+fn cover_bool() {
+    match kani::any() {
+        true => kani::cover!(true, "true"),
+        false => kani::cover!(true, "false"),
+    }
+}
+
+#[kani::proof]
+fn cover_option() {
+    match kani::any() {
+        Some(true) => kani::cover!(true, "true"),
+        Some(false) => kani::cover!(true, "false"),
+        None => kani::cover!(true, "none"),
+    }
+}
diff --git a/tests/script-based-pre/build-cache-bin/cache_works.expected b/tests/script-based-pre/build-cache-bin/cache_works.expected
new file mode 100644
index 000000000000..e67a9b7f7fc6
--- /dev/null
+++ b/tests/script-based-pre/build-cache-bin/cache_works.expected
@@ -0,0 +1,21 @@
+Initial compilation
+target/initial.log:Compiled 1 crates
+target/initial.log:No harness verified
+Re-execute the same command
+target/same.log:Compiled 0 crates
+target/same.log:No harness verified
+Run with new arg that affects kani-driver workflow only
+target/driver_opt.log:Compiled 0 crates
+target/driver_opt.log:Checking harness cover_option...
+target/driver_opt.log:Checking harness cover_bool...
+target/driver_opt.log:Complete - 2 successfully verified harnesses, 0 failures, 2 total.
+Run with a new argument that affects compilation
+target/disable_checks.log:Compiled 1 crates
+target/disable_checks.log:Checking harness cover_option...
+target/disable_checks.log:Checking harness cover_bool...
+target/disable_checks.log:Complete - 2 successfully verified harnesses, 0 failures, 2 total.
+Run with new dependency
+target/new_dep.log:Compiled 2 crates
+target/new_dep.log:Checking harness cover_option...
+target/new_dep.log:Checking harness cover_bool...
+target/new_dep.log:Complete - 2 successfully verified harnesses, 0 failures, 2 total.
diff --git a/tests/script-based-pre/build-cache-bin/cache_works.sh b/tests/script-based-pre/build-cache-bin/cache_works.sh
new file mode 100755
index 000000000000..22f102392a6a
--- /dev/null
+++ b/tests/script-based-pre/build-cache-bin/cache_works.sh
@@ -0,0 +1,71 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# Checks situations where running kani multiple times will work as expected when
+# the target crate is binary.
+#
+# The following checks should not trigger recompilation.
+# - Exact same input being invoked a second time.
+# - Different options that do not affect the compilation, only the Kani workt flow.
+# While the following should recompile the target.
+# - Pass a new argument that affects compilation
+# - Add a dependency
+set -e
+set -u
+
+ORIG=bin
+OUT_DIR=target
+MANIFEST=${OUT_DIR}/${ORIG}/Cargo.toml
+
+# Expects two arguments: "kani arguments" "output_file"
+function check_kani {
+    local args=$1
+    local log_file="${OUT_DIR}/$2"
+    # Run kani with the given arguments
+    if [ -z "${args}" ]
+    then
+        cargo kani --manifest-path "${MANIFEST}" --target-dir "${OUT_DIR}" \
+            2>&1 | tee "${log_file}"
+    else
+        cargo kani --manifest-path "${MANIFEST}" --target-dir "${OUT_DIR}" \
+            "${args}" 2>&1 | tee "${log_file}"
+    fi
+
+    # Print information about the generated log file.
+    # Check for occurrences of "Compiling" messages in the log files
+    local compiled=$(grep -c "Compiling" ${log_file})
+    echo "${log_file}:Compiled ${compiled} crates"
+
+    # Check which harnesses were verified
+    grep "Checking harness" -H ${log_file} || echo "${log_file}:No harness verified"
+
+    # Check the verification summary
+    grep "successfully verified harnesses" -H ${log_file} || true
+}
+
+# Ensure output folder is clean
+rm -rf ${OUT_DIR}
+mkdir -p ${OUT_DIR}
+# Move the original source to the output folder since it will be modified
+cp -r ${ORIG} ${OUT_DIR}
+
+echo "Initial compilation"
+check_kani --only-codegen initial.log
+
+echo "Re-execute the same command"
+check_kani --only-codegen same.log
+
+echo "Run with new arg that affects kani-driver workflow only"
+check_kani "" driver_opt.log
+
+echo "Run with a new argument that affects compilation"
+check_kani --no-assertion-reach-checks disable_checks.log
+
+echo "Run with new dependency"
+cargo new --lib ${OUT_DIR}/new_dep
+cargo add new_dep --manifest-path ${MANIFEST} --path ${OUT_DIR}/new_dep
+check_kani  --no-assertion-reach-checks new_dep.log
+
+# Try to leave a clean output folder at the end
+rm -rf ${OUT_DIR}
diff --git a/tests/script-based-pre/build-cache-bin/config.yml b/tests/script-based-pre/build-cache-bin/config.yml
new file mode 100644
index 000000000000..a5e5035b11f4
--- /dev/null
+++ b/tests/script-based-pre/build-cache-bin/config.yml
@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: cache_works.sh
+expected: cache_works.expected
diff --git a/tests/script-based-pre/build-cache-dirty/config.yml b/tests/script-based-pre/build-cache-dirty/config.yml
new file mode 100644
index 000000000000..dc1f964977b4
--- /dev/null
+++ b/tests/script-based-pre/build-cache-dirty/config.yml
@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: rebuild.sh
+expected: rebuild.expected
diff --git a/tests/script-based-pre/build-cache-dirty/rebuild.expected b/tests/script-based-pre/build-cache-dirty/rebuild.expected
new file mode 100644
index 000000000000..31b45fd8b3ee
--- /dev/null
+++ b/tests/script-based-pre/build-cache-dirty/rebuild.expected
@@ -0,0 +1,23 @@
+Initial compilation
+omplete - 2 successfully verified harnesses, 0 failures, 2 total.
+target/initial.log:Compiled 2 crates
+target/initial.log:Checking harness check_u8_i16...
+target/initial.log:Checking harness check_u8_u32...
+target/initial.log:Complete - 2 successfully verified harnesses, 0 failures, 2 total.
+Run with a new argument that affects compilation
+target/enable_checks.log:Compiled 2 crates
+target/enable_checks.log:Checking harness check_u8_i16...
+target/enable_checks.log:Checking harness check_u8_u32...
+target/enable_checks.log:Complete - 2 successfully verified harnesses, 0 failures, 2 total.
+Run after change to the source code
+target/changed_src.log:Compiled 1 crates
+target/changed_src.log:Checking harness noop_check...
+target/changed_src.log:Checking harness check_u8_i16...
+target/changed_src.log:Checking harness check_u8_u32...
+target/changed_src.log:Complete - 3 successfully verified harnesses, 0 failures, 3 total.
+Run with new dependency
+target/new_dep.log:Compiled 2 crates
+target/new_dep.log:Checking harness noop_check...
+target/new_dep.log:Checking harness check_u8_i16...
+target/new_dep.log:Checking harness check_u8_u32...
+target/new_dep.log:Complete - 3 successfully verified harnesses, 0 failures, 3 total.
diff --git a/tests/script-based-pre/build-cache-dirty/rebuild.sh b/tests/script-based-pre/build-cache-dirty/rebuild.sh
new file mode 100755
index 000000000000..e9e800b96287
--- /dev/null
+++ b/tests/script-based-pre/build-cache-dirty/rebuild.sh
@@ -0,0 +1,68 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# Checks situations where running kani multiple times should trigger a new build
+# The cases we cover here are:
+# - Pass a new argument that affects compilation
+# - Change the source code
+# - Add a dependency
+# Note: This should run in the folder where the script is.
+
+OUT_DIR=target
+MANIFEST=${OUT_DIR}/target_lib/Cargo.toml
+LIB_SRC=${OUT_DIR}/target_lib/src/lib.rs
+
+# Expects two arguments: "kani arguments" "output_file"
+function check_kani {
+    local args=$1
+    local log_file="${OUT_DIR}/$2"
+    # Run kani with the given arguments
+    if [ -z "${args}" ]
+    then
+        cargo kani --manifest-path "${MANIFEST}" --target-dir "${OUT_DIR}" \
+            2>&1 | tee "${log_file}"
+    else
+        cargo kani --manifest-path "${MANIFEST}" --target-dir "${OUT_DIR}" \
+            "${args}" 2>&1 | tee "${log_file}"
+    fi
+
+    # Print information about the generated log file.
+    # Check for occurrences of "Compiling" messages in the log files
+    local compiled=$(grep -c "Compiling" ${log_file})
+    echo "${log_file}:Compiled ${compiled} crates"
+
+    # Check which harnesses were verified
+    grep "Checking harness" -H ${log_file} || echo "${log_file}:No harness verified"
+
+    # Check the verification summary
+    grep "successfully verified harnesses" -H ${log_file} || true
+}
+
+# Ensure output folder is clean
+rm -rf ${OUT_DIR}
+mkdir -p ${OUT_DIR}
+
+# Copy the project so we don't make changes to the source code
+cp -r target_lib ${OUT_DIR}
+
+echo "Initial compilation"
+check_kani --no-assertion-reach-checks initial.log
+
+echo "Run with a new argument that affects compilation"
+check_kani "" enable_checks.log
+
+echo "Run after change to the source code"
+echo '
+#[kani::proof]
+fn noop_check() {}
+' >> ${LIB_SRC}
+check_kani "" changed_src.log
+
+echo "Run with new dependency"
+cargo new --lib ${OUT_DIR}/new_dep
+cargo add new_dep --manifest-path ${MANIFEST} --path ${OUT_DIR}/new_dep
+check_kani "" new_dep.log
+
+# Try to leave a clean output folder at the end
+rm -rf ${OUT_DIR}
diff --git a/tests/script-based-pre/build-cache-dirty/target_lib/Cargo.toml b/tests/script-based-pre/build-cache-dirty/target_lib/Cargo.toml
new file mode 100644
index 000000000000..e2a176e022ef
--- /dev/null
+++ b/tests/script-based-pre/build-cache-dirty/target_lib/Cargo.toml
@@ -0,0 +1,11 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "target_lib"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
+either = "1.8"
diff --git a/tests/script-based-pre/build-cache-dirty/target_lib/src/lib.rs b/tests/script-based-pre/build-cache-dirty/target_lib/src/lib.rs
new file mode 100644
index 000000000000..fa495defdaaa
--- /dev/null
+++ b/tests/script-based-pre/build-cache-dirty/target_lib/src/lib.rs
@@ -0,0 +1,19 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! We don't use any of our dependencies to keep the test fast
+
+#[kani::proof]
+fn check_u8_u32() {
+    let before: u8 = kani::any();
+    let temp = before as u32;
+    let after: u8 = temp.try_into().unwrap();
+    assert_eq!(after, before);
+}
+
+#[kani::proof]
+fn check_u8_i16() {
+    let before: u8 = kani::any();
+    let temp = before as i16;
+    let after: u8 = temp.try_into().unwrap();
+    assert_eq!(after, before);
+}
diff --git a/tests/script-based-pre/build-cache-fresh/cache_works.expected b/tests/script-based-pre/build-cache-fresh/cache_works.expected
new file mode 100644
index 000000000000..f283bf6fdff0
--- /dev/null
+++ b/tests/script-based-pre/build-cache-fresh/cache_works.expected
@@ -0,0 +1,16 @@
+Initial compilation
+target/initial.log:Compiled 1 crates
+target/initial.log:No harness verified
+Re-execute the same command
+target/same.log:Compiled 0 crates
+target/same.log:No harness verified
+Run with new arg that affects kani-driver workflow only
+target/driver_opt.log:Compiled 0 crates
+target/driver_opt.log:Checking harness cover_option...
+target/driver_opt.log:Checking harness cover_bool...
+target/driver_opt.log:Complete - 2 successfully verified harnesses, 0 failures, 2 total.
+Run with a new cbmc option
+target/cbmc_opt.log:Compiled 0 crates
+target/cbmc_opt.log:Checking harness cover_option...
+target/cbmc_opt.log:Checking harness cover_bool...
+target/cbmc_opt.log:Complete - 2 successfully verified harnesses, 0 failures, 2 total.
diff --git a/tests/script-based-pre/build-cache-fresh/cache_works.sh b/tests/script-based-pre/build-cache-fresh/cache_works.sh
new file mode 100755
index 000000000000..558437f0973e
--- /dev/null
+++ b/tests/script-based-pre/build-cache-fresh/cache_works.sh
@@ -0,0 +1,57 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# Checks situations where running kani multiple times will not trigger a recompilation
+# The cases we cover here are:
+# - Exact same input being invoked 2x.
+# - Different options that do not affect the compilation, only the Kani workflow.
+# - Different options that do not affect the compilation, only the CBMC execution.
+
+MANIFEST=lib/Cargo.toml
+OUT_DIR=target
+
+# Expects two arguments: "kani arguments" "output_file"
+function check_kani {
+    local args=$1
+    local log_file="${OUT_DIR}/$2"
+    # Run kani with the given arguments
+    if [ -z "${args}" ]
+    then
+        cargo kani --manifest-path "${MANIFEST}" --target-dir "${OUT_DIR}" \
+            2>&1 | tee "${log_file}"
+    else
+        cargo kani --manifest-path "${MANIFEST}" --target-dir "${OUT_DIR}" \
+            "${args}" 2>&1 | tee "${log_file}"
+    fi
+
+    # Print information about the generated log file.
+    # Check for occurrences of "Compiling" messages in the log files
+    local compiled=$(grep -c "Compiling" ${log_file})
+    echo "${log_file}:Compiled ${compiled} crates"
+
+    # Check which harnesses were verified
+    grep "Checking harness" -H ${log_file} || echo "${log_file}:No harness verified"
+
+    # Check the verification summary
+    grep "successfully verified harnesses" -H ${log_file} || true
+}
+
+# Ensure output folder is clean
+rm -rf ${OUT_DIR}
+mkdir -p ${OUT_DIR}
+
+echo "Initial compilation"
+check_kani --only-codegen initial.log
+
+echo "Re-execute the same command"
+check_kani --only-codegen same.log
+
+echo "Run with new arg that affects kani-driver workflow only"
+check_kani "" driver_opt.log
+
+echo "Run with a new cbmc option"
+check_kani --no-default-checks cbmc_opt.log
+
+# Try to leave a clean output folder at the end
+rm -rf ${OUT_DIR}
diff --git a/tests/script-based-pre/build-cache-fresh/config.yml b/tests/script-based-pre/build-cache-fresh/config.yml
new file mode 100644
index 000000000000..a5e5035b11f4
--- /dev/null
+++ b/tests/script-based-pre/build-cache-fresh/config.yml
@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: cache_works.sh
+expected: cache_works.expected
diff --git a/tests/script-based-pre/build-cache-fresh/lib/Cargo.toml b/tests/script-based-pre/build-cache-fresh/lib/Cargo.toml
new file mode 100644
index 000000000000..b75742d280b6
--- /dev/null
+++ b/tests/script-based-pre/build-cache-fresh/lib/Cargo.toml
@@ -0,0 +1,10 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+[package]
+name = "lib"
+version = "0.1.0"
+edition = "2021"
+
+# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
+
+[dependencies]
diff --git a/tests/script-based-pre/build-cache-fresh/lib/src/lib.rs b/tests/script-based-pre/build-cache-fresh/lib/src/lib.rs
new file mode 100644
index 000000000000..8f4468728cac
--- /dev/null
+++ b/tests/script-based-pre/build-cache-fresh/lib/src/lib.rs
@@ -0,0 +1,18 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+#[kani::proof]
+fn cover_bool() {
+    match kani::any() {
+        true => kani::cover!(true, "true"),
+        false => kani::cover!(true, "false"),
+    }
+}
+
+#[kani::proof]
+fn cover_option() {
+    match kani::any() {
+        Some(true) => kani::cover!(true, "true"),
+        Some(false) => kani::cover!(true, "false"),
+        None => kani::cover!(true, "none"),
+    }
+}