diff --git a/anneal/v2/Cargo.toml b/anneal/v2/Cargo.toml
index 7c056f854d..ead0da8c35 100644
--- a/anneal/v2/Cargo.toml
+++ b/anneal/v2/Cargo.toml
@@ -4,6 +4,8 @@ members = [".", "exocrate"]
 [features]
 # Enables tests that assume a prebuilt exocrate archive.
 exocrate_tests = []
+# Enables tests that make network requests or download cargo dependencies.
+online_tests = []
 
 [package]
 name = "cargo-anneal"
diff --git a/anneal/v2/src/charon.rs b/anneal/v2/src/charon.rs
index d274b3f571..3d39cd7092 100644
--- a/anneal/v2/src/charon.rs
+++ b/anneal/v2/src/charon.rs
@@ -90,6 +90,11 @@ pub fn run_charon(
         cmd.env("PATH", &new_path);
         cmd.env(lib_env_var, &new_lib_path);
 
+        // Redirect Cargo's build outputs to our safe local workspace target dir.
+        // This prevents permission errors when compiling read-only registry dependency directories.
+        let local_target_dir = roots.cargo_target_dir();
+        cmd.env("CARGO_TARGET_DIR", &local_target_dir);
+
         cmd.arg("cargo");
         cmd.arg("--preset=aeneas");
 
@@ -226,7 +231,7 @@ pub fn run_charon(
 mod tests {
     use super::*;
     use crate::resolve::{Args, resolve_roots};
-    use crate::scanner::scan_workspace;
+    use crate::scanner::{ScanMode, scan_workspace};
     use clap::Parser as _;
     use std::fs;
 
@@ -313,7 +318,7 @@ mod tests {
         let roots = resolve_roots(&args).unwrap();
 
         // 6. Scan workspace.
-        let packages = scan_workspace(&roots).unwrap();
+        let packages = scan_workspace(&roots, ScanMode::WorkspaceOnly).unwrap();
         assert_eq!(packages.len(), 1);
 
         // 7. Lock run root.
@@ -375,7 +380,7 @@ mod tests {
 
         // 3. Resolve roots and scan workspace.
         let roots = resolve_roots(&args).unwrap();
-        let packages = scan_workspace(&roots).unwrap();
+        let packages = scan_workspace(&roots, ScanMode::WorkspaceOnly).unwrap();
         assert_eq!(packages.len(), 1);
 
         // 4. Lock run root.
@@ -410,7 +415,7 @@ mod tests {
 
     #[cfg(feature = "exocrate_tests")]
     #[test]
-    fn test_charon_crates_io_dependency() {
+    fn test_charon_crates_io_dependency_not_chased_workspace_only() {
         let _ = env_logger::builder().is_test(true).try_init();
 
         let temp_dir = tempfile::tempdir().unwrap();
@@ -442,7 +447,7 @@ mod tests {
         .unwrap();
 
         let roots = resolve_roots(&args).unwrap();
-        let packages = scan_workspace(&roots).unwrap();
+        let packages = scan_workspace(&roots, ScanMode::WorkspaceOnly).unwrap();
         let locked_roots = roots.lock_run_root().unwrap();
 
         let toolchain = crate::setup::Toolchain::resolve().expect("Failed to resolve toolchain");
@@ -464,7 +469,7 @@ mod tests {
 
     #[cfg(feature = "exocrate_tests")]
     #[test]
-    fn test_charon_path_dependency_behavior() {
+    fn test_charon_path_dependency_not_chased_workspace_only() {
         let _ = env_logger::builder().is_test(true).try_init();
 
         let temp_dir = tempfile::tempdir().unwrap();
@@ -515,7 +520,7 @@ mod tests {
         .unwrap();
 
         let roots = resolve_roots(&args).unwrap();
-        let packages = scan_workspace(&roots).unwrap();
+        let packages = scan_workspace(&roots, ScanMode::WorkspaceOnly).unwrap();
         assert_eq!(packages.len(), 1);
         let locked_roots = roots.lock_run_root().unwrap();
 
@@ -585,7 +590,7 @@ mod tests {
 
         // 3. Resolve roots and scan workspace.
         let roots = resolve_roots(&args).unwrap();
-        let packages = scan_workspace(&roots).unwrap();
+        let packages = scan_workspace(&roots, ScanMode::WorkspaceOnly).unwrap();
         assert_eq!(packages.len(), 2, "Expected exactly two packages resolved in workspace");
 
         // 4. Lock run root.
@@ -630,4 +635,524 @@ mod tests {
             "Function 'func_a' was incorrectly translated in Package B!"
         );
     }
+
+    #[cfg(feature = "exocrate_tests")]
+    #[test]
+    fn test_charon_path_dependency_chasing() {
+        let _ = env_logger::builder().is_test(true).try_init();
+
+        let temp_dir = tempfile::tempdir().unwrap();
+        crate::workspace_fixture!(&temp_dir, {
+            "Cargo.toml" => r#"
+                [workspace]
+                resolver = "2"
+                members = [
+                    "test_proj",
+                ]
+                exclude = [
+                    "my_dep",
+                ]
+            "#,
+            "my_dep/Cargo.toml" => r#"
+                [package]
+                name = "my_dep"
+                version = "0.1.0"
+                edition = "2021"
+
+                [workspace]
+
+                [lib]
+                path = "src/lib.rs"
+            "#,
+            "my_dep/src/lib.rs" => r#"
+                pub fn dep_fn() {}
+            "#,
+            "test_proj/Cargo.toml" => r#"
+                [package]
+                name = "test_proj"
+                version = "0.1.0"
+                edition = "2021"
+
+                [dependencies]
+                my_dep = { path = "../my_dep" }
+
+                [lib]
+                path = "src/lib.rs"
+            "#,
+            "test_proj/src/lib.rs" => r#"
+                pub fn call_dep() {
+                    my_dep::dep_fn();
+                }
+            "#,
+        });
+
+        let args = Args::try_parse_from(&[
+            "cargo-anneal",
+            "--manifest-path",
+            temp_dir.path().join("test_proj").join("Cargo.toml").to_str().unwrap(),
+        ])
+        .unwrap();
+
+        // 1. Resolve roots.
+        let roots = resolve_roots(&args).unwrap();
+
+        // 2. Scan workspace WITH include_dependencies = true!
+        let packages = scan_workspace(&roots, ScanMode::FollowDependencies).unwrap();
+
+        // 3. Assert that BOTH local project and external path dependency were promoted to target packages!
+        assert_eq!(packages.len(), 2, "Expected exactly two target artifacts promoted!");
+
+        let local_target = &packages[0];
+        let dep_target = &packages[1];
+
+        assert_eq!(local_target.name.package_name, "test_proj");
+        assert_eq!(dep_target.name.package_name, "my_dep");
+
+        let locked_roots = roots.lock_run_root().unwrap();
+        let toolchain = crate::setup::Toolchain::resolve().expect("Failed to resolve toolchain");
+
+        // 4. Run Charon coordinator.
+        let res = run_charon(&args, &toolchain, &locked_roots, &packages, false);
+        assert!(res.is_ok(), "charon failed: {:?}", res.err());
+
+        // 5. Verify test_proj target translated.
+        let llbc_path_local = local_target.llbc_path(&locked_roots);
+        assert!(llbc_path_local.exists());
+        let llbc_content_local = std::fs::read_to_string(&llbc_path_local).unwrap();
+        assert!(llbc_content_local.contains("call_dep"));
+
+        // 6. Verify path dependency was CHASED and compiled as an independent root target!
+        let llbc_path_dep = dep_target.llbc_path(&locked_roots);
+        assert!(
+            llbc_path_dep.exists(),
+            "Dependency LLBC file did not exist at {:?}",
+            llbc_path_dep
+        );
+        let llbc_content_dep = std::fs::read_to_string(&llbc_path_dep).unwrap();
+
+        // Assert that the dependency's implementation body is fully translated inside its own file!
+        assert!(
+            llbc_content_dep
+                .contains("\"name\":[{\"Ident\":[\"my_dep\",0]},{\"Ident\":[\"dep_fn\",0]}]"),
+            "Chased dependency function 'dep_fn' was not declared!"
+        );
+        assert!(
+            llbc_content_dep.contains("\"body\":{\"Structured\":"),
+            "Chased dependency function should contain a translated structured body implementation!"
+        );
+    }
+
+    #[cfg(all(feature = "exocrate_tests", feature = "online_tests"))]
+    #[test]
+    fn test_charon_crates_io_dependency_chasing() {
+        let _ = env_logger::builder().is_test(true).try_init();
+
+        let temp_dir = tempfile::tempdir().unwrap();
+        crate::workspace_fixture!(&temp_dir, {
+            "Cargo.toml" => r#"
+                [workspace]
+                resolver = "2"
+
+                [package]
+                name = "test_proj"
+                version = "0.1.0"
+                edition = "2021"
+
+                [dependencies]
+                log = "0.4"
+
+                [lib]
+                path = "src/lib.rs"
+            "#,
+            "src/lib.rs" => r#"
+                pub fn log_info(msg: &str) {
+                    log::info!("{}", msg);
+                    let opt: Option<u32> = Some(42);
+                    let _x = opt.unwrap_or(0);
+                }
+            "#,
+        });
+
+        let args = Args::try_parse_from(&[
+            "cargo-anneal",
+            "--manifest-path",
+            temp_dir.path().join("Cargo.toml").to_str().unwrap(),
+        ])
+        .unwrap();
+
+        // 1. Resolve roots.
+        let roots = resolve_roots(&args).unwrap();
+
+        // 2. Scan workspace WITH FollowDependencies mode!
+        let packages = scan_workspace(&roots, ScanMode::FollowDependencies).unwrap();
+        log::debug!(
+            "Promoted packages: {:?}",
+            packages.iter().map(|p| &p.name.package_name).collect::<Vec<_>>()
+        );
+
+        // 3. Verify that the external crates.io dependency 'log' was successfully promoted to a compile target!
+        let local_target = packages
+            .iter()
+            .find(|p| p.name.package_name == "test_proj")
+            .cloned()
+            .expect("local target test_proj was not resolved!");
+        let log_target = packages
+            .iter()
+            .find(|p| p.name.package_name == "log")
+            .cloned()
+            .expect("crates.io dependency log was not promoted!");
+
+        let locked_roots = roots.lock_run_root().unwrap();
+        let toolchain = crate::setup::Toolchain::resolve().expect("Failed to resolve toolchain");
+
+        // 4. Run Charon coordinator on ONLY our test targets to keep build hermetic
+        let targets_to_run = vec![local_target.clone(), log_target.clone()];
+        let res = run_charon(&args, &toolchain, &locked_roots, &targets_to_run, false);
+        assert!(res.is_ok(), "charon failed: {:?}", res.err());
+
+        // 5. Verify that the chased crates.io dependency 'log' was fully compiled to LLBC!
+        let llbc_path_log = log_target.llbc_path(&locked_roots);
+        assert!(
+            llbc_path_log.exists(),
+            "Chased crates.io LLBC file did not exist at {:?}",
+            llbc_path_log
+        );
+        let llbc_content_log = std::fs::read_to_string(&llbc_path_log).unwrap();
+
+        // Deep check: Assert that 'log' functions are translated with their FULL implementation body
+        // inside their own dependency .llbc file (no longer "Opaque"!).
+        assert!(
+            llbc_content_log.contains("log_enabled"),
+            "Chased crates.io function 'log_enabled' was not declared!"
+        );
+
+        // 6. Deep Standard Library Check:
+        // Investigating stdlib function implementation: Since stdlib functions (like 'unwrap_or')
+        // are automatically lowered directly into the local MIR context of the calling crate,
+        // we verify that we have its fully structured compilation body available inside local LLBC.
+        let llbc_path_local = local_target.llbc_path(&locked_roots);
+        // 5. Verify test_proj target translated (definition included).
+        assert_fn_body(&llbc_path_local, &["test_proj", "call_dep"], true, true);
+
+        // 6. Verify path dependency was CHASED and compiled as an independent root target with its own local definition!
+        let llbc_path_dep = dep_target.llbc_path(&locked_roots);
+        assert!(llbc_path_dep.exists());
+        assert_fn_body(&llbc_path_dep, &["my_dep", "dep_fn"], true, true);
+    }
+
+    #[cfg(all(feature = "exocrate_tests", feature = "online_tests"))]
+    #[test]
+    fn test_charon_crates_io_dependency_chasing() {
+        let _ = env_logger::builder().is_test(true).try_init();
+
+        let temp_dir = tempfile::tempdir().unwrap();
+        crate::workspace_fixture!(&temp_dir, {
+            "Cargo.toml" => r#"
+                [workspace]
+                resolver = "2"
+
+                [package]
+                name = "test_proj"
+                version = "0.1.0"
+                edition = "2021"
+
+                [dependencies]
+                log = "0.4"
+
+                [lib]
+                path = "src/lib.rs"
+            "#,
+            "src/lib.rs" => r#"
+                pub fn log_info(msg: &str) {
+                    log::info!("{}", msg);
+                    let opt: Option<u32> = Some(42);
+                    let _x = opt.unwrap_or(0);
+                }
+            "#,
+        });
+
+        let args = Args::try_parse_from(&[
+            "cargo-anneal",
+            "--manifest-path",
+            temp_dir.path().join("Cargo.toml").to_str().unwrap(),
+        ])
+        .unwrap();
+
+        // 1. Resolve roots.
+        let roots = resolve_roots(&args).unwrap();
+
+        // 2. Scan workspace WITH FollowDependencies mode!
+        let packages = scan_workspace(&roots, ScanMode::FollowDependencies).unwrap();
+        log::debug!(
+            "Promoted packages: {:?}",
+            packages.iter().map(|p| &p.name.package_name).collect::<Vec<_>>()
+        );
+
+        // 3. Verify that the external crates.io dependency 'log' was successfully promoted to a compile target!
+        let local_target = packages
+            .iter()
+            .find(|p| p.name.package_name == "test_proj")
+            .cloned()
+            .expect("local target test_proj was not resolved!");
+        let log_target = packages
+            .iter()
+            .find(|p| p.name.package_name == "log")
+            .cloned()
+            .expect("crates.io dependency log was not promoted!");
+
+        let locked_roots = roots.lock_run_root().unwrap();
+        let toolchain = crate::setup::Toolchain::resolve().expect("Failed to resolve toolchain");
+
+        // 4. Run Charon coordinator on ONLY our test targets to keep build hermetic
+        let targets_to_run = vec![local_target.clone(), log_target.clone()];
+        let res = run_charon(&args, &toolchain, &locked_roots, &targets_to_run, false);
+        assert!(res.is_ok(), "charon failed: {:?}", res.err());
+
+        // 5. Verify that the chased crates.io dependency 'log' was compiled as an independent root target (so definition is local to itself)!
+        let llbc_path_log = log_target.llbc_path(&locked_roots);
+        assert!(llbc_path_log.exists());
+        assert_fn_body(&llbc_path_log, &["log", "log_enabled"], true, true);
+
+        // 6. Deep Standard Library Check:
+        // Investigating stdlib function implementation: Since stdlib functions (like 'unwrap_or')
+        // are automatically lowered directly into the local MIR context of the calling crate,
+        // we verify that we have its referred external declaration inside local LLBC (body opaque).
+        let llbc_path_local = local_target.llbc_path(&locked_roots);
+        assert_fn_body(&llbc_path_local, &["core", "option", "Option", "unwrap_or"], false, false);
+    }
+
+    #[cfg(feature = "exocrate_tests")]
+    #[test]
+    fn test_charon_crates_io_dependency_chasing_offline_hermetic() {
+        let _ = env_logger::builder().is_test(true).try_init();
+
+        let temp_dir = tempfile::tempdir().unwrap();
+        crate::workspace_fixture!(&temp_dir, {
+            "Cargo.toml" => r#"
+                [workspace]
+                resolver = "2"
+
+                [package]
+                name = "test_proj"
+                version = "0.1.0"
+                edition = "2021"
+
+                [dependencies]
+                log = "0.4"
+
+                [lib]
+                path = "src/lib.rs"
+
+                [patch.crates-io]
+                log = { path = "./vendor/log" }
+            "#,
+            "src/lib.rs" => r#"
+                pub fn log_info(msg: &str) {
+                    log::info!("{}", msg);
+                    let opt: Option<u32> = Some(42);
+                    let _x = opt.unwrap_or(0);
+                }
+            "#,
+        });
+
+        let args = Args::try_parse_from(&[
+            "cargo-anneal",
+            "--manifest-path",
+            temp_dir.path().join("Cargo.toml").to_str().unwrap(),
+        ])
+        .unwrap();
+
+        // Copy vendored dependency directory directly into virtual workspace sandbox
+        // so that path patch resolves cleanly under standard file permissions
+        let src_vendor_dir = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("vendor");
+        let dest_vendor_dir = temp_dir.path().join("vendor");
+        std::fs::create_dir_all(&dest_vendor_dir).unwrap();
+
+        // Recursively copy log package to local vendor path
+        let src_log = src_vendor_dir.join("log");
+        let dest_log = dest_vendor_dir.join("log");
+        std::fs::create_dir_all(&dest_log).unwrap();
+
+        let copy_dir = |src: &std::path::Path, dest: &std::path::Path| {
+            for entry in walkdir::WalkDir::new(src) {
+                let entry = entry.unwrap();
+                let rel_path = entry.path().strip_prefix(src).unwrap();
+                let dest_path = dest.join(rel_path);
+                if entry.file_type().is_dir() {
+                    std::fs::create_dir_all(&dest_path).unwrap();
+                } else {
+                    std::fs::copy(entry.path(), &dest_path).unwrap();
+                    if rel_path == std::path::Path::new("Cargo.toml") {
+                        // Force-inject an empty [workspace] to prevent matching parent workspace rules!
+                        let mut content = std::fs::read_to_string(&dest_path).unwrap();
+
+                        // Strip optional dependency targets to bypass registry checks under offline mode
+                        for target in &[
+                            "[dependencies.sval]",
+                            "[dependencies.sval_ref]",
+                            "[dependencies.value-bag]",
+                            "[dependencies.serde_core]",
+                        ] {
+                            if let Some(idx) = content.find(target) {
+                                content.truncate(idx);
+                            }
+                        }
+
+                        // Strip dev-dependencies block to avoid triggering registry resolution on unused test packages
+                        if let Some(idx) = content.find("[dev-dependencies") {
+                            content.truncate(idx);
+                        }
+
+                        // Strip features block, keeping [lib] targets completely intact
+                        if let Some(f_start) = content.find("[features]") {
+                            if let Some(lib_start) = content.find("[lib]") {
+                                if f_start < lib_start {
+                                    // Features is before lib. Remove between them.
+                                    content.replace_range(f_start..lib_start, "");
+                                } else {
+                                    // Features is after lib. Truncate at features.
+                                    content.truncate(f_start);
+                                }
+                            } else {
+                                content.truncate(f_start);
+                            }
+                        }
+
+                        content.push_str("\n[workspace]\n");
+                        std::fs::write(&dest_path, content).unwrap();
+                    }
+                }
+            }
+        };
+        copy_dir(&src_log, &dest_log);
+
+        // 1. Resolve roots.
+        let roots = resolve_roots(&args).unwrap();
+
+        // 2. Scan workspace WITH FollowDependencies mode!
+        let packages = scan_workspace(&roots, ScanMode::FollowDependencies).unwrap();
+        log::debug!(
+            "Promoted packages: {:?}",
+            packages.iter().map(|p| &p.name.package_name).collect::<Vec<_>>()
+        );
+
+        // 3. Verify that the external crates.io dependency 'log' was successfully promoted to a compile target!
+        let local_target = packages
+            .iter()
+            .find(|p| p.name.package_name == "test_proj")
+            .cloned()
+            .expect("local target test_proj was not resolved!");
+        let log_target = packages
+            .iter()
+            .find(|p| p.name.package_name == "log")
+            .cloned()
+            .expect("crates.io dependency log was not promoted!");
+
+        let locked_roots = roots.lock_run_root().unwrap();
+        let toolchain = crate::setup::Toolchain::resolve().expect("Failed to resolve toolchain");
+
+        // 4. Run Charon coordinator on ONLY our test targets to keep build hermetic
+        let targets_to_run = vec![local_target.clone(), log_target.clone()];
+        let res = run_charon(&args, &toolchain, &locked_roots, &targets_to_run, false);
+        assert!(res.is_ok(), "charon failed: {:?}", res.err());
+
+        // 5. Verify that the chased crates.io dependency 'log' was compiled as an independent root target with local definition!
+        let llbc_path_log = log_target.llbc_path(&locked_roots);
+        assert!(llbc_path_log.exists());
+        assert_fn_body(&llbc_path_log, &["log", "log_enabled"], true, true);
+    }
+
+    #[cfg(feature = "exocrate_tests")]
+    #[test]
+    fn test_charon_stdlib_unwrap_or_not_chased_workspace_only() {
+        let _ = env_logger::builder().is_test(true).try_init();
+
+        let temp_dir = tempfile::tempdir().unwrap();
+        crate::workspace_fixture!(&temp_dir, {
+            "Cargo.toml" => r#"
+                [package]
+                name = "test_proj"
+                version = "0.1.0"
+                edition = "2021"
+
+                [lib]
+                path = "src/lib.rs"
+            "#,
+            "src/lib.rs" => r#"
+                pub fn call_unwrap(opt: Option<u32>) -> u32 {
+                    opt.unwrap_or(0)
+                }
+            "#,
+        });
+
+        let args = Args::try_parse_from(&[
+            "cargo-anneal",
+            "--manifest-path",
+            temp_dir.path().join("Cargo.toml").to_str().unwrap(),
+        ])
+        .unwrap();
+
+        let roots = resolve_roots(&args).unwrap();
+        let packages = scan_workspace(&roots, ScanMode::WorkspaceOnly).unwrap();
+        let locked_roots = roots.lock_run_root().unwrap();
+
+        let toolchain = crate::setup::Toolchain::resolve().expect("Failed to resolve toolchain");
+        let res = run_charon(&args, &toolchain, &locked_roots, &packages, false);
+        assert!(res.is_ok(), "charon failed: {:?}", res.err());
+
+        let llbc_path = packages[0].llbc_path(&locked_roots);
+        assert!(llbc_path.exists());
+
+        // Rigorous standard library checks:
+        // Verify that in WorkspaceOnly mode:
+        // 1. The unwrap_or declaration matches and is referred to as external/opaque (definition body NOT included).
+        assert_fn_body(&llbc_path, &["core", "option", "Option", "unwrap_or"], false, false);
+    }
+
+    #[cfg(feature = "exocrate_tests")]
+    #[test]
+    fn test_charon_stdlib_unwrap_or_chased_dependency_following() {
+        let _ = env_logger::builder().is_test(true).try_init();
+
+        let temp_dir = tempfile::tempdir().unwrap();
+        crate::workspace_fixture!(&temp_dir, {
+            "Cargo.toml" => r#"
+                [package]
+                name = "test_proj"
+                version = "0.1.0"
+                edition = "2021"
+
+                [lib]
+                path = "src/lib.rs"
+            "#,
+            "src/lib.rs" => r#"
+                pub fn call_unwrap(opt: Option<u32>) -> u32 {
+                    opt.unwrap_or(0)
+                }
+            "#,
+        });
+
+        let args = Args::try_parse_from(&[
+            "cargo-anneal",
+            "--manifest-path",
+            temp_dir.path().join("Cargo.toml").to_str().unwrap(),
+        ])
+        .unwrap();
+
+        let roots = resolve_roots(&args).unwrap();
+        let packages = scan_workspace(&roots, ScanMode::FollowDependencies).unwrap();
+        let locked_roots = roots.lock_run_root().unwrap();
+
+        let toolchain = crate::setup::Toolchain::resolve().expect("Failed to resolve toolchain");
+        let res = run_charon(&args, &toolchain, &locked_roots, &packages, false);
+        assert!(res.is_ok(), "charon failed: {:?}", res.err());
+
+        let llbc_path = packages[0].llbc_path(&locked_roots);
+        assert!(llbc_path.exists());
+
+        // Rigorous standard library checks in FollowDependencies mode:
+        // Standard library functions are referred to as external, but generic items called directly are
+        // lowered into the calling package's compiled body structure context (meaning local definition is Structured).
+        assert_fn_body(&llbc_path, &["core", "option", "Option", "unwrap_or"], false, true);
+    }
 }
diff --git a/anneal/v2/src/main.rs b/anneal/v2/src/main.rs
index b57c109471..da1a43fbbb 100644
--- a/anneal/v2/src/main.rs
+++ b/anneal/v2/src/main.rs
@@ -69,6 +69,10 @@ pub struct ExpandArgs {
     /// Do not show compilation progress bars
     #[arg(long)]
     pub no_progress: bool,
+
+    /// Recursively compile and translate all third-party dependencies to LLBC
+    #[arg(long)]
+    pub include_dependencies: bool,
 }
 
 fn setup(args: SetupArgs) -> anyhow::Result<()> {
@@ -78,7 +82,12 @@ fn setup(args: SetupArgs) -> anyhow::Result<()> {
 
 fn expand(args: ExpandArgs) -> anyhow::Result<()> {
     let roots = crate::resolve::resolve_roots(&args.resolve_args)?;
-    let packages = crate::scanner::scan_workspace(&roots)?;
+    let mode = if args.include_dependencies {
+        crate::scanner::ScanMode::FollowDependencies
+    } else {
+        crate::scanner::ScanMode::WorkspaceOnly
+    };
+    let packages = crate::scanner::scan_workspace(&roots, mode)?;
     if packages.is_empty() {
         log::warn!("No targets found to expand.");
         return Ok(());
diff --git a/anneal/v2/src/resolve.rs b/anneal/v2/src/resolve.rs
index 0e602f83dc..91cf5d9e44 100644
--- a/anneal/v2/src/resolve.rs
+++ b/anneal/v2/src/resolve.rs
@@ -154,6 +154,7 @@ pub struct Roots {
     // E.g., `target/anneal/<hash>`.
     anneal_run_root: std::path::PathBuf,
     pub roots: Vec<AnnealTarget>,
+    pub metadata: cargo_metadata::Metadata,
 }
 
 impl Roots {
@@ -246,6 +247,7 @@ pub fn resolve_roots(args: &Args) -> anyhow::Result<Roots> {
         anneal_global_root,
         anneal_run_root,
         roots: Vec::new(),
+        metadata: metadata.clone(), // `metadata` must outlive `selected_packages`.
     };
 
     for package in selected_packages {
diff --git a/anneal/v2/src/scanner.rs b/anneal/v2/src/scanner.rs
index fb090583c1..a7d51f9da6 100644
--- a/anneal/v2/src/scanner.rs
+++ b/anneal/v2/src/scanner.rs
@@ -9,11 +9,21 @@
 
 use sha2::Digest as _;
 
+/// Controls target scanning scope.
+#[derive(Debug, Copy, Clone, PartialEq, Eq)]
+pub enum ScanMode {
+    /// Scan local workspace member crates only.
+    WorkspaceOnly,
+    /// Walk all source code crates in the dependency graph and emit LLBC.
+    FollowDependencies,
+}
+
 /// Represents a compilation target (artifact) that needs to be processed.
 ///
 /// In this rewrite, we no longer directly parse Rust files to extract annotations
 /// or entry points. Instead, Charon compiles the entire target to generate LLBC
 /// files, and annotations will be processed from LLBC directly at a later stage.
+#[derive(Clone, Debug)]
 pub struct AnnealArtifact {
     pub name: crate::resolve::AnnealTargetName,
     pub target_kind: crate::resolve::AnnealTargetKind,
@@ -107,7 +117,10 @@ impl AnnealArtifact {
 
 /// Scans the resolved workspace roots to identify the targets that need to be passed
 /// to Charon. No Rust source code parsing is performed during this step.
-pub fn scan_workspace(roots: &crate::resolve::Roots) -> anyhow::Result<Vec<AnnealArtifact>> {
+pub fn scan_workspace(
+    roots: &crate::resolve::Roots,
+    mode: ScanMode,
+) -> anyhow::Result<Vec<AnnealArtifact>> {
     let mut artifacts = Vec::new();
     for target in &roots.roots {
         artifacts.push(AnnealArtifact {
@@ -116,5 +129,24 @@ pub fn scan_workspace(roots: &crate::resolve::Roots) -> anyhow::Result<Vec<Annea
             manifest_path: target.manifest_path.clone(),
         });
     }
+
+    if mode == ScanMode::FollowDependencies {
+        for pkg in &roots.metadata.packages {
+            // Skip workspace members to prevent duplication.
+            if roots.metadata.workspace_members.contains(&pkg.id) {
+                continue;
+            }
+            artifacts.push(AnnealArtifact {
+                name: crate::resolve::AnnealTargetName {
+                    package_name: pkg.name.clone(),
+                    target_name: pkg.name.to_string(),
+                    kind: crate::resolve::AnnealTargetKind::Lib,
+                },
+                target_kind: crate::resolve::AnnealTargetKind::Lib,
+                manifest_path: pkg.manifest_path.as_std_path().to_owned(),
+            });
+        }
+    }
+
     Ok(artifacts)
 }