diff --git a/kani-compiler/src/kani_compiler.rs b/kani-compiler/src/kani_compiler.rs
index 8382c5421222..25de67e45db2 100644
--- a/kani-compiler/src/kani_compiler.rs
+++ b/kani-compiler/src/kani_compiler.rs
@@ -111,6 +111,7 @@ impl Callbacks for KaniCompiler {
             let queries = self.queries.clone();
             move |_cfg| backend(queries)
         }));
+        // `kani-driver` passes the `kani-compiler` specific arguments through llvm-args, so extract them here.
         args.extend(config.opts.cg.llvm_args.iter().cloned());
         let args = Arguments::parse_from(args);
         init_session(&args, matches!(config.opts.error_format, ErrorOutputType::Json { .. }));
diff --git a/kani-compiler/src/main.rs b/kani-compiler/src/main.rs
index 6bf8e549af76..3452484c5054 100644
--- a/kani-compiler/src/main.rs
+++ b/kani-compiler/src/main.rs
@@ -72,10 +72,15 @@ fn main() {
 
 /// Return whether we should run our flavour of the compiler, and which arguments to pass to rustc.
 ///
-/// We add a `--kani-compiler` argument to run the Kani version of the compiler, which needs to be
+/// `kani-driver` adds a `--kani-compiler` argument to run the Kani version of the compiler, which needs to be
 /// filtered out before passing the arguments to rustc.
-///
 /// All other Kani arguments are today located inside `--llvm-args`.
+///
+/// This function returns `true` for rustc invocations that originate from our rustc / cargo rustc invocations in `kani-driver`.
+/// It returns `false` for rustc invocations that cargo adds in the process of executing the `kani-driver` rustc command.
+/// For example, if we are compiling a crate that has a build.rs file, cargo will compile and run that build script
+/// (c.f. https://doc.rust-lang.org/cargo/reference/build-scripts.html#life-cycle-of-a-build-script).
+/// The build script should be compiled with normal rustc, not the Kani compiler.
 pub fn is_kani_compiler(args: Vec<String>) -> (bool, Vec<String>) {
     assert!(!args.is_empty(), "Arguments should always include executable name");
     const KANI_COMPILER: &str = "--kani-compiler";
diff --git a/kani-driver/src/autoharness/mod.rs b/kani-driver/src/autoharness/mod.rs
index 83162621dd1b..00f2e809e6ad 100644
--- a/kani-driver/src/autoharness/mod.rs
+++ b/kani-driver/src/autoharness/mod.rs
@@ -154,6 +154,8 @@ impl KaniSession {
     }
 
     /// Add the compiler arguments specific to the `autoharness` subcommand.
+    /// TODO: this should really be appending onto the `kani_compiler_flags()` output instead of `pkg_args`.
+    /// It doesn't affect functionality since autoharness doesn't examine dependencies, but would still be better practice.
     pub fn add_auto_harness_args(&mut self, included: &[String], excluded: &[String]) {
         for func in included {
             self.pkg_args
diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs
index 9097713a0016..5f9f18d03563 100644
--- a/kani-driver/src/call_cargo.rs
+++ b/kani-driver/src/call_cargo.rs
@@ -182,14 +182,19 @@ crate-type = ["lib"]
             cargo_args.push("-v".into());
         }
 
-        // Arguments that will only be passed to the target package.
+        // Arguments that will only be passed to the target package (the package under verification)
+        // and not its dependencies, c.f. https://doc.rust-lang.org/cargo/commands/cargo-rustc.html.
+        // The difference between pkg_args and rustc_args is that rustc_args are also provided when
+        // we invoke rustc on the target package's dependencies.
+        // We do not provide the `--reachability` argument to dependencies so that it has the default value `None`
+        // (c.f. kani-compiler::args::ReachabilityType) and we skip codegen for the dependency.
+        // This is the desired behavior because we only want to construct `CodegenUnits` for the target package;
+        // i.e., if some dependency has harnesses, we don't want to run them.
+
+        // If you are adding a new `kani-compiler` argument, you likely want to put it `kani_compiler_flags()` instead,
+        // unless there a reason it shouldn't be passed to dependencies.
+        // (Note that at the time of writing, passing the other compiler args to dependencies is a no-op, since `--reachability=None` skips codegen anyway.)
         self.pkg_args.push(self.reachability_arg());
-        if let Some(backend_arg) = self.backend_arg() {
-            self.pkg_args.push(backend_arg);
-        }
-        if self.args.no_assert_contracts {
-            self.pkg_args.push("--no-assert-contracts".into());
-        }
 
         let mut found_target = false;
         let packages = self.packages_to_verify(&self.args, &metadata)?;
diff --git a/kani-driver/src/call_single_file.rs b/kani-driver/src/call_single_file.rs
index f21f83345783..a24028dd84ba 100644
--- a/kani-driver/src/call_single_file.rs
+++ b/kani-driver/src/call_single_file.rs
@@ -53,9 +53,6 @@ impl KaniSession {
     ) -> Result<()> {
         let mut kani_args = self.kani_compiler_flags();
         kani_args.push(format!("--reachability={}", self.reachability_mode()));
-        if self.args.common_args.unstable_features.contains(UnstableFeature::Lean) {
-            kani_args.push("--backend=llbc".into());
-        }
 
         let lib_path = lib_folder().unwrap();
         let mut rustc_args = self.kani_rustc_flags(LibConfig::new(lib_path));
@@ -100,14 +97,6 @@ impl KaniSession {
         to_rustc_arg(vec![format!("--reachability={}", self.reachability_mode())])
     }
 
-    pub fn backend_arg(&self) -> Option<String> {
-        if self.args.common_args.unstable_features.contains(UnstableFeature::Lean) {
-            Some(to_rustc_arg(vec!["--backend=llbc".into()]))
-        } else {
-            None
-        }
-    }
-
     /// 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![check_version()];
@@ -150,6 +139,10 @@ impl KaniSession {
             flags.push("--ub-check=uninit".into());
         }
 
+        if self.args.common_args.unstable_features.contains(UnstableFeature::Lean) {
+            flags.push("--backend=llbc".into());
+        }
+
         if self.args.print_llbc {
             flags.push("--print-llbc".into());
         }
diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs
index 6645db06e45e..20ebef0e2aaa 100644
--- a/kani-driver/src/session.rs
+++ b/kani-driver/src/session.rs
@@ -34,7 +34,7 @@ pub struct KaniSession {
     /// Automatically verify functions in the crate, in addition to running manual harnesses.
     pub auto_harness: bool,
 
-    /// The arguments that will be passed to the target package, i.e. kani_compiler.
+    /// The arguments that will be passed only to the target package, not its dependencies.
     pub pkg_args: Vec<String>,
 
     /// Include all publicly-visible symbols in the generated goto binary, not just those reachable from