diff --git a/anneal/v2/src/charon.rs b/anneal/v2/src/charon.rs
index 618ad55694..bc0b44583a 100644
--- a/anneal/v2/src/charon.rs
+++ b/anneal/v2/src/charon.rs
@@ -1,25 +1,15 @@
-// Orchestration of Charon extraction.
-//
-// This module handles the invocation of the `charon` tool to extract
-// Low-Level Borrow Calculus (LLBC) from Rust crates. It manages:
-// - Setting up the Charon command and arguments (including features,
-//   targets, and output paths).
-// - Handling `unsafe(axiom)` functions by marking them as opaque to Charon.
-// - Streaming and filtering compiler output to provide user-friendly
-//   feedback via `indicatif` and `miette`.
-// - Validating the extraction result.
-
-use std::io::{BufRead, BufReader};
-
-use anyhow::{Context as _, Result, bail};
-use cargo_metadata::{Message, diagnostic::DiagnosticLevel};
-
-use crate::{
-    parse::{ParsedItem, attr::FunctionBlockInner},
-    resolve::{AnnealTargetKind, Args, LockedRoots},
-    scanner::AnnealArtifact,
-    setup::Tool,
-};
+//! Orchestration of Charon extraction.
+//!
+//! This module handles the invocation of the `charon` tool to extract
+//! Low-Level Borrow Calculus (LLBC) from Rust crates. It manages:
+//! - Setting up the Charon command and arguments (including features,
+//!   targets, and output paths).
+//! - Handling `unsafe(axiom)` functions by marking them as opaque to Charon.
+//! - Streaming and filtering compiler output to provide user-friendly
+//!   feedback via `indicatif` and `miette`.
+//! - Validating the extraction result.
+
+use anyhow::Context as _;
 
 /// Runs Charon on the specified packages to generate LLBC artifacts.
 ///
@@ -34,34 +24,33 @@ use crate::{
 ///   minimize extraction scope.
 /// - **Output Handling**: capturing stdout/stderr, parsing JSON compiler
 ///   messages, and rendering them using `DiagnosticMapper`.
-pub fn run_charon(args: &Args, roots: &LockedRoots, packages: &[AnnealArtifact]) -> Result<()> {
+pub fn run_charon(
+    args: &crate::resolve::Args,
+    roots: &crate::resolve::LockedRoots,
+    packages: &[crate::scanner::AnnealArtifact],
+    toolchain: &crate::setup::Toolchain,
+) -> anyhow::Result<()> {
     let llbc_root = roots.llbc_root();
     std::fs::create_dir_all(&llbc_root).context("Failed to create LLBC output directory")?;
 
-    let toolchain = crate::setup::Toolchain::resolve()?;
-
-    let rust_sysroot = toolchain.root.join("rust");
-    let rust_bin = rust_sysroot.join("bin");
-    let rust_lib = rust_sysroot.join("lib");
-
-    // Helper closure to prepend a path to an existing environment variable,
-    // separating them with a colon if the variable is not empty. This is used
-    // to inject our managed Rust toolchain paths before the system paths.
-    let prepend_to_env_var = |var_name: &str, new_path: std::path::PathBuf| {
-        let current_val = std::env::var_os(var_name).unwrap_or_default();
-        let mut combined = new_path.into_os_string();
-        if !current_val.is_empty() {
-            combined.push(":");
-            combined.push(current_val);
-        }
-        combined
-    };
+    let rust_bin = toolchain.rust_bin();
+    let rust_lib = toolchain.rust_lib();
 
-    let new_path = prepend_to_env_var("PATH", rust_bin);
+    // We prepend the managed Rust toolchain's `bin` directory to `PATH`. This is
+    // necessary because Charon is a compiler frontend that invokes `cargo` and
+    // `rustc` under the hood. To ensure hermeticity and correctness, we must force
+    // Charon to use our pinned nightly compiler version rather than falling back
+    // to whatever version happens to be installed in the system `PATH`.
+    let new_path = crate::util::prepend_to_env_var("PATH", rust_bin);
 
     let lib_env_var =
         if cfg!(target_os = "macos") { "DYLD_LIBRARY_PATH" } else { "LD_LIBRARY_PATH" };
-    let new_lib_path = prepend_to_env_var(lib_env_var, rust_lib);
+    // We set `LD_LIBRARY_PATH` (or `DYLD_LIBRARY_PATH` on macOS) to point to the
+    // managed Rust toolchain's `lib` directory. This is strictly required because
+    // `charon-driver` is a dynamic executable that links against `rustc` compiler
+    // dynamic libraries (like `librustc_driver-*.so`). Without this, the dynamic
+    // linker will fail to load the libraries when `charon-driver` is executed.
+    let new_lib_path = crate::util::prepend_to_env_var(lib_env_var, rust_lib);
 
     for artifact in packages {
         if artifact.start_from.is_empty() {
@@ -70,8 +59,12 @@ pub fn run_charon(args: &Args, roots: &LockedRoots, packages: &[AnnealArtifact])
 
         log::info!("Invoking Charon on package '{}'...", artifact.name.package_name);
 
-        let mut cmd = toolchain.command(Tool::Charon);
+        let mut cmd = toolchain.command(crate::setup::Tool::Charon);
 
+        // We set `CHARON_TOOLCHAIN_IS_IN_PATH=1` to instruct Charon to bypass its
+        // standard toolchain resolution logic (which expects the compiler to be
+        // managed via `rustup`). Instead, it will directly use the `rustc` and
+        // `cargo` binaries we prepended to the `PATH` environment variable.
         cmd.env("CHARON_TOOLCHAIN_IS_IN_PATH", "1");
         cmd.env("PATH", &new_path);
         cmd.env(lib_env_var, &new_lib_path);
@@ -79,18 +72,21 @@ pub fn run_charon(args: &Args, roots: &LockedRoots, packages: &[AnnealArtifact])
         cmd.arg("cargo");
         cmd.arg("--preset=aeneas");
 
-        // Output artifacts to target/anneal/<hash>/llbc
+        // Output artifacts to target/anneal/<hash>/llbc.
         let llbc_path = artifact.llbc_path(roots);
-        log::debug!("Writing .llbc file to {}", llbc_path.display());
+        log::debug!("Writing .llbc file to {:?}", llbc_path);
         cmd.arg("--dest-file").arg(llbc_path);
 
-        // Fail fast on errors
+        // We use `--abort-on-error` to fail fast. If Charon (or `rustc`)
+        // encounters a compilation error or translation failure (e.g., an
+        // unsupported Rust feature), it will terminate the process immediately
+        // rather than attempting to proceed and translate other parts of the crate.
         cmd.arg("--abort-on-error");
 
         for item in &artifact.items {
-            if let ParsedItem::Function(func) = &item.item {
-                // Check if the function body is an Axiom (unsafe)
-                if let FunctionBlockInner::Axiom { .. } = func.anneal.inner {
+            if let crate::parse::ParsedItem::Function(func) = &item.item {
+                // Check if the function body is an Axiom (unsafe).
+                if let crate::parse::attr::FunctionBlockInner::Axiom { .. } = func.anneal.inner {
                     // Mark `unsafe(axiom)` functions as opaque in Charon. This
                     // instructs Aeneas to treat the function as external and
                     // generate a template file (`FunsExternal_Template.lean`)
@@ -103,6 +99,7 @@ pub fn run_charon(args: &Args, roots: &LockedRoots, packages: &[AnnealArtifact])
                     opaque_name.push_str("::");
                     opaque_name.push_str(func.item.name());
 
+                    log::trace!("Marking item as opaque in Charon: {}", opaque_name);
                     cmd.args(["--opaque", &opaque_name]);
                 }
             }
@@ -116,14 +113,17 @@ pub fn run_charon(args: &Args, roots: &LockedRoots, packages: &[AnnealArtifact])
         let mut start_from = artifact.start_from.iter().map(String::as_ref).collect::<Vec<_>>();
         start_from.sort_unstable(); // Slightly faster than `sort`, and equivalent for strings.
 
+        if log::log_enabled!(log::Level::Trace) {
+            for entry in &start_from {
+                log::trace!("Translation entry point: {}", entry);
+            }
+        }
+
         let start_from_str = start_from.join(",");
-        // OS command-line length limits (Windows is ~32k; Linux `ARG_MAX` is
-        // usually larger, but variable)
-        const ARG_CHAR_LIMIT: usize = 32_768;
-        if start_from_str.len() > ARG_CHAR_LIMIT {
+        if start_from_str.len() > crate::util::ARG_CHAR_LIMIT {
             // FIXME: Pass the list of entry points to Charon via a file instead
             // of the command line.
-            bail!(
+            anyhow::bail!(
                 "The list of Anneal entry points for package '{}' is too large ({} bytes). \n\
                  This exceeds safe OS command-line limits.",
                 artifact.name.package_name,
@@ -133,20 +133,19 @@ pub fn run_charon(args: &Args, roots: &LockedRoots, packages: &[AnnealArtifact])
 
         cmd.arg("--start-from").arg(start_from_str);
 
-        // Separator for the underlying cargo command
+        // Separator for the underlying cargo command.
         cmd.arg("--");
 
-        // Ensure cargo emits json msgs which charon-driver natively generates
+        // Ensure cargo emits json msgs which charon-driver natively generates.
         cmd.arg("--message-format=json");
 
         cmd.arg("--manifest-path").arg(&artifact.manifest_path);
 
-        use AnnealTargetKind::*;
         match artifact.target_kind {
-            Lib | RLib | ProcMacro | CDyLib | DyLib | StaticLib => cmd.arg("--lib"),
-            Bin => cmd.args(["--bin", &artifact.name.target_name]),
-            Example => cmd.args(["--example", &artifact.name.target_name]),
-            Test => cmd.args(["--test", &artifact.name.target_name]),
+            crate::resolve::AnnealTargetKind::Lib | crate::resolve::AnnealTargetKind::RLib | crate::resolve::AnnealTargetKind::ProcMacro | crate::resolve::AnnealTargetKind::CDyLib | crate::resolve::AnnealTargetKind::DyLib | crate::resolve::AnnealTargetKind::StaticLib => cmd.arg("--lib"),
+            crate::resolve::AnnealTargetKind::Bin => cmd.args(["--bin", &artifact.name.target_name]),
+            crate::resolve::AnnealTargetKind::Example => cmd.args(["--example", &artifact.name.target_name]),
+            crate::resolve::AnnealTargetKind::Test => cmd.args(["--test", &artifact.name.target_name]),
         };
 
         // Forward all feature-related flags.
@@ -160,91 +159,55 @@ pub fn run_charon(args: &Args, roots: &LockedRoots, packages: &[AnnealArtifact])
             cmd.arg("--features").arg(feature);
         }
 
-        // Reuse the main target directory for dependencies to save time.
+        // We share `CARGO_TARGET_DIR` (`target/anneal/cargo_target`) across all
+        // Charon invocations to enable Cargo's incremental build cache. This
+        // prevents Cargo from recompiling identical workspace dependencies from
+        // scratch for each individual target, saving significant compilation time.
         cmd.env("CARGO_TARGET_DIR", roots.cargo_target_dir());
 
-        log::debug!("Command: {:?}", cmd);
+        log::debug!("Executing charon command: {:?}", cmd);
 
-        cmd.stdout(std::process::Stdio::piped());
-        cmd.stderr(std::process::Stdio::piped());
         let start = std::time::Instant::now();
-        let mut child = cmd.spawn().context("Failed to spawn charon")?;
-
-        let mut output_error = false;
-
-        let safety_buffer = std::sync::Arc::new(std::sync::Mutex::new(Vec::new()));
-        let safety_buffer_clone = std::sync::Arc::clone(&safety_buffer);
+        let output_error = std::sync::Arc::new(std::sync::atomic::AtomicBool::new(false));
+        let output_error_clone = std::sync::Arc::clone(&output_error);
 
         // Charon's standard error stream contains unstructured diagnostic
         // output (such as panic messages from build scripts or ICEs). We
-        // dedicate a background thread to drain this stream into a
-        // thread-safe safety buffer. This ensures that even if Charon aborts
+        // collect this in a safety buffer to ensure that even if Charon aborts
         // unexpectedly, the user receives the complete unstructured output
         // instead of a generic "silent death".
-        let mut stderr_thread = None;
-        if let Some(stderr) = child.stderr.take() {
-            stderr_thread = Some(std::thread::spawn(move || {
-                use std::io::{BufRead, BufReader};
-                let reader = BufReader::new(stderr);
-                for line in reader.lines().map_while(Result::ok) {
-                    safety_buffer_clone.lock().unwrap().push(line);
-                }
-            }));
-        }
+        let safety_buffer = std::sync::Arc::new(std::sync::Mutex::new(Vec::new()));
+        let safety_buffer_clone = std::sync::Arc::clone(&safety_buffer);
 
-        let pb = indicatif::ProgressBar::new_spinner();
-        pb.set_style(
-            indicatif::ProgressStyle::default_spinner().template("{spinner:.green} {msg}").unwrap(),
-        );
-        pb.enable_steady_tick(std::time::Duration::from_millis(100));
-        pb.set_message("Compiling...");
-
-        if let Some(stdout) = child.stdout.take() {
-            let reader = BufReader::new(stdout);
-
-            let mut mapper = crate::diagnostics::DiagnosticMapper::new(roots.workspace().clone());
-            for line in reader.lines().map_while(Result::ok) {
-                if let Ok(msg) = serde_json::from_str::<cargo_metadata::Message>(&line) {
-                    match msg {
-                        Message::CompilerArtifact(a) => {
-                            pb.set_message(format!("Compiling {}", a.target.name));
-                        }
-                        Message::CompilerMessage(msg) => {
-                            pb.suspend(|| {
-                                mapper.render_miette(&msg.message, |s| eprintln!("{}", s));
-                            });
-                            if matches!(
-                                msg.message.level,
-                                DiagnosticLevel::Error | DiagnosticLevel::Ice
-                            ) {
-                                output_error = true;
-                            }
-                        }
-                        Message::TextLine(t) => {
-                            safety_buffer.lock().unwrap().push(t);
+        let mut mapper = crate::diagnostics::DiagnosticMapper::new(roots.workspace().clone());
+
+        let res = crate::util::run_command_with_progress(cmd, "Compiling...", move |line, pb| {
+            if let Ok(msg) = serde_json::from_str::<cargo_metadata::Message>(line) {
+                match msg {
+                    cargo_metadata::Message::CompilerArtifact(a) => {
+                        pb.set_message(format!("Compiling {}", a.target.name));
+                    }
+                    cargo_metadata::Message::CompilerMessage(msg) => {
+                        pb.suspend(|| {
+                            mapper.render_miette(&msg.message, |s| eprintln!("{}", s));
+                        });
+                        if matches!(
+                            msg.message.level,
+                            cargo_metadata::diagnostic::DiagnosticLevel::Error | cargo_metadata::diagnostic::DiagnosticLevel::Ice
+                        ) {
+                            output_error_clone.store(true, std::sync::atomic::Ordering::Relaxed);
                         }
-                        _ => {}
                     }
-                } else {
-                    safety_buffer.lock().unwrap().push(line);
+                    cargo_metadata::Message::TextLine(t) => {
+                        safety_buffer_clone.lock().unwrap().push(t);
+                    }
+                    _ => {}
                 }
+            } else {
+                safety_buffer_clone.lock().unwrap().push(line.to_string());
             }
-        }
-
-        pb.finish_and_clear();
-
-        let status = child.wait().context("Failed to wait for charon")?;
-
-        // The main thread has finished reading the structured JSON output from
-        // Charon's standard output stream, and the Charon process itself has
-        // exited. However, we must explicitly wait for the background thread
-        // to finish draining the standard error stream. Failing to join this
-        // thread introduces a race condition where the main thread might
-        // inspect the `safety_buffer` before the background thread has
-        // finished appending the final error messages from the dying process.
-        if let Some(thread) = stderr_thread {
-            let _ = thread.join();
-        }
+            Ok(())
+        })?;
 
         log::trace!("Charon for '{}' took {:.2?}", artifact.name.package_name, start.elapsed());
 
@@ -253,14 +216,18 @@ pub fn run_charon(args: &Args, roots: &LockedRoots, packages: &[AnnealArtifact])
         // print won't include all relevant information – some will be printed
         // via stderr. In this case, `output_error = true` and so we bail and
         // discard stderr, which will swallow information from the user.
-        if output_error {
-            bail!("Diagnostic error in charon");
-        } else if !status.success() {
-            // "Silent Death" dump
+        if output_error.load(std::sync::atomic::Ordering::Relaxed) {
+            anyhow::bail!("Diagnostic error in charon");
+        } else if !res.status.success() {
+            // "Silent Death" dump.
             for line in safety_buffer.lock().unwrap().iter() {
                 eprintln!("{}", line);
             }
-            bail!("Charon failed with status: {}", status);
+            // Also dump the dynamic linker errors or panic messages captured in stderr.
+            for line in &res.stderr_lines {
+                eprintln!("{}", line);
+            }
+            anyhow::bail!("Charon failed with status: {}", res.status);
         }
     }
 
@@ -277,9 +244,6 @@ mod tests {
 
     #[test]
     fn test_run_charon_simple() {
-        // We must set __ANNEAL_LOCAL_DEV=1 so that it finds the toolchain in the local target directory.
-        unsafe { std::env::set_var("__ANNEAL_LOCAL_DEV", "1"); }
-
         // 1. Create a temporary directory
         let temp_dir = tempfile::tempdir().unwrap();
         let proj_dir = temp_dir.path().join("test_proj");
@@ -324,8 +288,14 @@ mod tests {
         // 7. Lock run root
         let locked_roots = roots.lock_run_root().unwrap();
 
-        // 8. Run charon
-        let res = run_charon(&args, &locked_roots, &packages);
+        // 8. Resolve test-only stripped toolchain and run charon
+        let toolchain_root = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR"))
+            .join("tests")
+            .join("toolchains")
+            .join("charon-only");
+        let toolchain = crate::setup::Toolchain::new_test(toolchain_root);
+
+        let res = run_charon(&args, &locked_roots, &packages, &toolchain);
         assert!(res.is_ok(), "charon failed: {:?}", res.err());
 
         // 9. Verify .llbc file exists
diff --git a/anneal/v2/src/diagnostics.rs b/anneal/v2/src/diagnostics.rs
index cd27b771e2..31b71eb118 100644
--- a/anneal/v2/src/diagnostics.rs
+++ b/anneal/v2/src/diagnostics.rs
@@ -1,19 +1,11 @@
 // Handling of Lean diagnostics and error mapping.
 //
-// This module provides the `DiagnosticMapper` struct, which is responsible
+// This module provides the [`crate::diagnostics::DiagnosticMapper`] struct, which is responsible
 // for translating diagnostics from external tools (like Lean or Charon) back
 // to the original Rust source code. It maps errors in generated files back to
 // their origin spans in the user's codebase.
 
-use std::{
-    collections::HashMap,
-    fs,
-    path::{Component, Path, PathBuf},
-};
-
 pub use cargo_metadata::diagnostic::{Diagnostic, DiagnosticLevel, DiagnosticSpan};
-use miette::{NamedSource, Report, SourceOffset};
-use thiserror::Error;
 
 /// Maps diagnostics from generated intermediate code back to pristine,
 /// original source code files.
@@ -24,19 +16,19 @@ use thiserror::Error;
 /// To create a first-class user experience, this mapper actively
 /// cross-references Lean's emitted byte spans against the sidecar
 /// `SourceMapping`s built by `src/generate.rs`, dynamically synthesizing a
-/// `miette::NamedSource` that points directly into the user's actual `.rs`
+/// [`miette::NamedSource`] that points directly into the user's actual `.rs`
 /// workspace files.
 pub struct DiagnosticMapper {
-    user_root: PathBuf,
-    user_root_canonical: PathBuf,
-    source_cache: HashMap<PathBuf, String>,
+    user_root: std::path::PathBuf,
+    user_root_canonical: std::path::PathBuf,
+    source_cache: std::collections::HashMap<std::path::PathBuf, String>,
 }
 
-#[derive(Error, Debug)]
+#[derive(thiserror::Error, Debug)]
 #[error("{message}")]
 struct MappedError {
     message: String,
-    src: NamedSource<String>,
+    src: miette::NamedSource<String>,
     labels: Vec<miette::LabeledSpan>,
     help: Option<String>,
     related: Vec<MappedError>,
@@ -48,7 +40,7 @@ impl miette::Diagnostic for MappedError {
         Some(&self.src)
     }
 
-    fn labels(&self) -> Option<Box<dyn Iterator<Item = miette::LabeledSpan> + '_>> {
+    fn labels(&self) -> Option<Box<dyn std::iter::Iterator<Item = miette::LabeledSpan> + '_>> {
         if self.labels.is_empty() { None } else { Some(Box::new(self.labels.iter().cloned())) }
     }
 
@@ -56,7 +48,7 @@ impl miette::Diagnostic for MappedError {
         self.help.as_ref().map(|h| Box::new(h.clone()) as Box<dyn std::fmt::Display>)
     }
 
-    fn related<'a>(&'a self) -> Option<Box<dyn Iterator<Item = &'a dyn miette::Diagnostic> + 'a>> {
+    fn related<'a>(&'a self) -> Option<Box<dyn std::iter::Iterator<Item = &'a dyn miette::Diagnostic> + 'a>> {
         if self.related.is_empty() {
             None
         } else {
@@ -72,46 +64,46 @@ impl miette::Diagnostic for MappedError {
 
 impl DiagnosticMapper {
     /// Creates a new mapper rooted at `user_root`.
-    pub fn new(user_root: PathBuf) -> Self {
+    pub fn new(user_root: std::path::PathBuf) -> Self {
         let user_root_canonical =
-            fs::canonicalize(&user_root).unwrap_or_else(|_| user_root.clone());
-        Self { user_root, user_root_canonical, source_cache: HashMap::new() }
+            std::fs::canonicalize(&user_root).unwrap_or_else(|_| user_root.clone());
+        Self { user_root, user_root_canonical, source_cache: std::collections::HashMap::new() }
     }
 
     /// Resolves a path relative to the user root, if applicable.
     ///
     /// This ensures we only report diagnostics for files within the user's
     /// workspace, avoiding noise from dependencies or system files.
-    pub fn map_path(&self, path: &Path) -> Option<PathBuf> {
+    pub fn map_path(&self, path: &std::path::Path) -> Option<std::path::PathBuf> {
         let mut p = path.to_path_buf();
         if p.is_relative() {
             p = self.user_root.join(p);
         }
 
         p = {
-            let mut normalized = PathBuf::new();
+            let mut normalized = std::path::PathBuf::new();
             for component in p.components() {
                 let most_recent = normalized.components().next_back();
                 match (component, most_recent) {
-                    (Component::ParentDir, Some(Component::Normal(_))) => {
+                    (std::path::Component::ParentDir, Some(std::path::Component::Normal(_))) => {
                         normalized.pop();
                     }
-                    (Component::CurDir, _) => {}
+                    (std::path::Component::CurDir, _) => {}
                     _ => normalized.push(component),
                 }
             }
             normalized
         };
 
-        // Strategy B: Starts with user_root or user_root_canonical
+        // Strategy B: Starts with user_root or user_root_canonical.
         (p.starts_with(&self.user_root) || p.starts_with(&self.user_root_canonical)).then_some(p)
     }
 
-    fn get_source(&mut self, path: &Path) -> Option<String> {
+    fn get_source(&mut self, path: &std::path::Path) -> Option<String> {
         if let Some(src) = self.source_cache.get(path) {
             return Some(src.clone());
         }
-        if let Ok(src) = fs::read_to_string(path) {
+        if let Ok(src) = std::fs::read_to_string(path) {
             self.source_cache.insert(path.to_path_buf(), src.clone());
             Some(src)
         } else {
@@ -128,11 +120,11 @@ impl DiagnosticMapper {
     where
         F: FnMut(String),
     {
-        let mut mapped_paths_and_spans: HashMap<PathBuf, Vec<&DiagnosticSpan>> = HashMap::new();
+        let mut mapped_paths_and_spans: std::collections::HashMap<std::path::PathBuf, Vec<&DiagnosticSpan>> = std::collections::HashMap::new();
 
-        // 1) Group spans by mapped path
+        // 1) Group spans by mapped path.
         for s in &diag.spans {
-            let p = PathBuf::from(&s.file_name);
+            let p = std::path::PathBuf::from(&s.file_name);
             if let Some(mapped_path) = self.map_path(&p) {
                 mapped_paths_and_spans.entry(mapped_path).or_default().push(s);
             }
@@ -152,14 +144,14 @@ impl DiagnosticMapper {
                 .spans
                 .iter()
                 .find(|s| s.is_primary)
-                .and_then(|s| self.map_path(&PathBuf::from(&s.file_name)))
+                .and_then(|s| self.map_path(&std::path::PathBuf::from(&s.file_name)))
                 .or_else(|| mapped_paths_and_spans.keys().next().cloned());
 
             if let Some(main_path) = primary_path {
                 let mut all_errors = Vec::new();
 
-                // Sort the paths to have the primary path first
-                let mut paths: Vec<PathBuf> = mapped_paths_and_spans.keys().cloned().collect();
+                // Sort the paths to have the primary path first.
+                let mut paths: Vec<std::path::PathBuf> = mapped_paths_and_spans.keys().cloned().collect();
                 paths.sort_by_key(|p| p != &main_path);
 
                 for p in paths {
@@ -173,7 +165,7 @@ impl DiagnosticMapper {
                                 let start: usize = s.byte_start.try_into().unwrap();
                                 let len = (s.byte_end - s.byte_start).try_into().unwrap();
                                 (start <= src.len() && start + len <= src.len()).then(|| {
-                                    let offset = SourceOffset::from(start);
+                                    let offset = miette::SourceOffset::from(start);
                                     miette::LabeledSpan::new(Some(label_text), offset.offset(), len)
                                 })
                             })
@@ -185,7 +177,7 @@ impl DiagnosticMapper {
                             } else {
                                 format!("related to: {}", p.display())
                             },
-                            src: NamedSource::new(p.to_string_lossy(), src),
+                            src: miette::NamedSource::new(p.to_string_lossy(), src),
                             labels,
                             help: if p == main_path { help_msg.clone() } else { None },
                             related: Vec::new(),
@@ -204,13 +196,13 @@ impl DiagnosticMapper {
                 if !all_errors.is_empty() {
                     let mut main_err = all_errors.remove(0);
                     main_err.related = all_errors;
-                    printer(format!("{:?}", Report::new(main_err)));
+                    printer(format!("{:?}", miette::Report::new(main_err)));
                     return;
                 }
             }
         }
 
-        // If we get here, no span was successfully mapped
+        // If we get here, no span was successfully mapped.
         let prefix = match diag.level {
             DiagnosticLevel::Error | DiagnosticLevel::Ice => "[External Error]",
             DiagnosticLevel::Warning => "[External Warning]",
@@ -224,7 +216,7 @@ impl DiagnosticMapper {
         }
     }
 
-    /// Renders a raw diagnostic (e.g., from Lean) directly at a mapped byte
+    /// Renders a diagnostic (e.g., from Lean) directly at a mapped byte
     /// range.
     ///
     /// The fundamental workflow for an external error is:
@@ -246,7 +238,7 @@ impl DiagnosticMapper {
     ) where
         F: FnMut(String),
     {
-        let p = PathBuf::from(file_name);
+        let p = std::path::PathBuf::from(file_name);
         if let Some(mapped_path) = self.map_path(&p)
             && let Some(src) = self.get_source(&mapped_path)
         {
@@ -254,12 +246,12 @@ impl DiagnosticMapper {
             if byte_end >= start {
                 let len = byte_end - start;
                 if start <= src.len() && start + len <= src.len() {
-                    let offset = SourceOffset::from(start);
+                    let offset = miette::SourceOffset::from(start);
                     let label =
                         miette::LabeledSpan::new(Some("here".to_string()), offset.offset(), len);
                     let err = MappedError {
                         message,
-                        src: NamedSource::new(mapped_path.to_string_lossy(), src),
+                        src: miette::NamedSource::new(mapped_path.to_string_lossy(), src),
                         labels: vec![label],
                         help: None,
                         related: Vec::new(),
@@ -271,13 +263,13 @@ impl DiagnosticMapper {
                             _ => Some(miette::Severity::Advice),
                         },
                     };
-                    printer(format!("{:?}", Report::new(err)));
+                    printer(format!("{:?}", miette::Report::new(err)));
                     return;
                 }
             }
         }
 
-        // Fallback
+        // Fallback.
         let prefix = match level {
             DiagnosticLevel::Error | DiagnosticLevel::Ice => "[External Error]",
             DiagnosticLevel::Warning => "[External Warning]",
@@ -297,7 +289,7 @@ mod tests {
         let user_root = temp.path().join("workspace");
         std::fs::create_dir(&user_root).unwrap();
 
-        // Create a symlink in the workspace pointing outside
+        // Create a symlink in the workspace pointing outside.
         let outside = temp.path().join("outside");
         std::fs::create_dir(&outside).unwrap();
         std::os::unix::fs::symlink(&outside, user_root.join("symlink")).unwrap();
diff --git a/anneal/v2/src/main.rs b/anneal/v2/src/main.rs
index bf73c625f1..c36af66a0a 100644
--- a/anneal/v2/src/main.rs
+++ b/anneal/v2/src/main.rs
@@ -17,7 +17,7 @@ mod scanner;
 mod charon;
 mod setup;
 
-/// Anneal: A Literate Verification Toolchain
+/// Anneal: A Literate Verification Toolchain.
 #[derive(clap::Parser, Debug)]
 #[command(name = "cargo-anneal", version, about, long_about = None)]
 struct Cli {
@@ -27,10 +27,13 @@ struct Cli {
 
 #[derive(clap::Subcommand, Debug)]
 enum Commands {
-    /// Setup Anneal dependencies
+    /// Setup Anneal dependencies.
     Setup(SetupArgs),
-    /// Expand a crate (runs Charon)
+    /// Expand a crate (runs Charon).
     Expand(ExpandArgs),
+    /// Setup test-only stripped toolchain (dev only).
+    #[cfg(feature = "exocrate_tests")]
+    TestSetup,
 }
 
 #[derive(clap::Parser, Debug)]
@@ -43,7 +46,7 @@ pub struct SetupArgs {
 #[derive(clap::Parser, Debug)]
 pub struct ExpandArgs {
     #[command(flatten)]
-    pub resolve_args: resolve::Args,
+    pub resolve_args: crate::resolve::Args,
 
     /// Controls where LLBC output is placed on the filesystem.
     #[arg(long, value_name = "output-dir")]
@@ -51,15 +54,15 @@ pub struct ExpandArgs {
 }
 
 fn setup(args: SetupArgs) {
-    setup::run_setup(setup::SetupArgs {
+    crate::setup::run_setup(crate::setup::SetupArgs {
         local_archive: args.local_archive,
     })
     .expect("failed to setup toolchain");
 }
 
 fn expand(args: ExpandArgs) -> anyhow::Result<()> {
-    let roots = resolve::resolve_roots(&args.resolve_args)?;
-    let packages = scanner::scan_workspace(&roots)?;
+    let roots = crate::resolve::resolve_roots(&args.resolve_args)?;
+    let packages = crate::scanner::scan_workspace(&roots)?;
     if packages.is_empty() {
         log::warn!("No targets found to expand.");
         return Ok(());
@@ -68,7 +71,8 @@ fn expand(args: ExpandArgs) -> anyhow::Result<()> {
     if let Some(output_dir) = args.output_dir {
         locked_roots.llbc_override = Some(output_dir);
     }
-    charon::run_charon(&args.resolve_args, &locked_roots, &packages)?;
+    let toolchain = crate::setup::Toolchain::resolve()?;
+    crate::charon::run_charon(&args.resolve_args, &locked_roots, &packages, &toolchain)?;
     Ok(())
 }
 
@@ -93,12 +97,18 @@ fn main() {
                 std::process::exit(1);
             }
         }
+        #[cfg(feature = "exocrate_tests")]
+        Commands::TestSetup => {
+            if let Err(e) = crate::setup::run_test_setup() {
+                eprintln!("TestSetup failed: {:?}", e);
+                std::process::exit(1);
+            }
+        }
     }
 }
 
-#[cfg(test)]
+#[cfg(all(test, feature = "exocrate_tests"))]
 mod tests {
-    #[cfg(feature = "exocrate_tests")]
     #[test]
     fn test_setup() {
         super::setup(super::SetupArgs {
diff --git a/anneal/v2/src/parse.rs b/anneal/v2/src/parse.rs
index d89f3b652d..0750d9d65b 100644
--- a/anneal/v2/src/parse.rs
+++ b/anneal/v2/src/parse.rs
@@ -1,6 +1,3 @@
-use std::marker::PhantomData;
-use std::path::PathBuf;
-
 pub mod hkd {
     pub struct Safe;
     pub trait ThreadSafety {}
@@ -17,7 +14,7 @@ pub struct AnnealDecorated<T, B> {
 
 #[derive(Clone, Debug)]
 pub enum FunctionItem<M> {
-    Free(PhantomData<M>),
+    Free(std::marker::PhantomData<M>),
 }
 
 impl<M> FunctionItem<M> {
@@ -35,7 +32,7 @@ pub enum FunctionBlockInner {
 #[derive(Clone, Debug)]
 pub struct FunctionAnnealBlock<M> {
     pub inner: FunctionBlockInner,
-    _phantom: PhantomData<M>,
+    _phantom: std::marker::PhantomData<M>,
 }
 
 #[derive(Clone, Debug)]
@@ -48,7 +45,7 @@ pub enum ParsedItem<M> {
 pub struct ParsedLeanItem<M> {
     pub item: ParsedItem<M>,
     pub module_path: Vec<String>,
-    pub source_file: PathBuf,
+    pub source_file: std::path::PathBuf,
 }
 
 pub mod attr {
diff --git a/anneal/v2/src/resolve.rs b/anneal/v2/src/resolve.rs
index 9034df14c4..1f302b58b3 100644
--- a/anneal/v2/src/resolve.rs
+++ b/anneal/v2/src/resolve.rs
@@ -1,13 +1,7 @@
-use std::{env, fs, path::PathBuf};
+use anyhow::Context as _;
+use sha2::Digest as _;
 
-use anyhow::{Context, Result, anyhow};
-use cargo_metadata::{Metadata, MetadataCommand, Package, PackageName, Target, TargetKind};
-use clap::Parser;
-use sha2::{Digest, Sha256};
-
-use crate::util::DirLock;
-
-#[derive(Parser, Debug)]
+#[derive(clap::Parser, Debug)]
 pub struct Args {
     #[command(flatten)]
     pub manifest: clap_cargo::Manifest,
@@ -18,44 +12,44 @@ pub struct Args {
     #[command(flatten)]
     pub features: clap_cargo::Features,
 
-    /// Verify the library target
+    /// Verify the library target.
     #[arg(long)]
     pub lib: bool,
 
-    /// Verify specific binary targets
+    /// Verify specific binary targets.
     #[arg(long)]
     pub bin: Vec<String>,
 
-    /// Verify all binary targets
+    /// Verify all binary targets.
     #[arg(long)]
     pub bins: bool,
 
-    /// Verify specific example targets
+    /// Verify specific example targets.
     #[arg(long)]
     pub example: Vec<String>,
 
-    /// Verify all example targets
+    /// Verify all example targets.
     #[arg(long)]
     pub examples: bool,
 
-    /// Verify specific test targets
+    /// Verify specific test targets.
     #[arg(long)]
     pub test: Vec<String>,
 
-    /// Verify all test targets
+    /// Verify all test targets.
     #[arg(long)]
     pub tests: bool,
 
-    /// Allow `sorry` in proofs and inject `sorry` for missing proofs
+    /// Allow `sorry` in proofs and inject `sorry` for missing proofs.
     #[arg(long)]
     pub allow_sorry: bool,
 
-    /// Allow use of `isValid` annotations
+    /// Allow use of `isValid` annotations.
     ///
     /// `isValid` annotations are currently unsound. In particular, Rust does
     /// not yet support annotating a field with `unsafe`, denoting that it
     /// carries an invariant. Thus, `isValid` annotations are effectively
-    /// advisory – any code which does not have a Anneal annotation can modify
+    /// advisory – any code which does not have a Anneal annotation can modify
     /// invariant-carrying fields without needing to use an `unsafe` block.
     /// Without an `unsafe` block, Anneal has no way of knowing that an
     /// operation needs to be analyzed for soundness.
@@ -67,7 +61,7 @@ pub struct Args {
     pub unsound_allow_is_valid: bool,
 }
 
-#[derive(Parser, Debug)]
+#[derive(clap::Parser, Debug)]
 pub struct SetupArgs {}
 
 #[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
@@ -100,11 +94,11 @@ impl AnnealTargetKind {
     }
 }
 
-impl TryFrom<&TargetKind> for AnnealTargetKind {
+impl std::convert::TryFrom<&cargo_metadata::TargetKind> for AnnealTargetKind {
     type Error = ();
 
-    fn try_from(kind: &TargetKind) -> Result<Self, Self::Error> {
-        use TargetKind::*;
+    fn try_from(kind: &cargo_metadata::TargetKind) -> anyhow::Result<Self, Self::Error> {
+        use cargo_metadata::TargetKind::*;
         match kind {
             Lib => Ok(Self::Lib),
             RLib => Ok(Self::RLib),
@@ -123,7 +117,7 @@ impl TryFrom<&TargetKind> for AnnealTargetKind {
 
 #[derive(Clone, Debug, Hash, PartialEq, Eq)]
 pub struct AnnealTargetName {
-    pub package_name: PackageName,
+    pub package_name: cargo_metadata::PackageName,
     pub target_name: String,
     pub kind: AnnealTargetKind,
 }
@@ -139,33 +133,33 @@ pub struct AnnealTarget {
     pub name: AnnealTargetName,
     pub kind: AnnealTargetKind,
     /// Path to the main source file for this target.
-    pub src_path: PathBuf,
+    pub src_path: std::path::PathBuf,
     /// Path to the `Cargo.toml` for this target.
-    pub manifest_path: PathBuf,
+    pub manifest_path: std::path::PathBuf,
 }
 
 #[derive(Debug)]
 pub struct Roots {
-    pub workspace: PathBuf,
+    pub workspace: std::path::PathBuf,
     // E.g., `target/anneal`.
-    anneal_global_root: PathBuf,
+    anneal_global_root: std::path::PathBuf,
     // E.g., `target/anneal/<hash>`.
-    anneal_run_root: PathBuf,
+    anneal_run_root: std::path::PathBuf,
     pub roots: Vec<AnnealTarget>,
 }
 
 impl Roots {
-    pub fn lock_run_root(&self) -> Result<LockedRoots<'_>> {
-        let lock = DirLock::lock_exclusive(self.anneal_run_root.clone())?;
+    pub fn lock_run_root(&self) -> anyhow::Result<LockedRoots<'_>> {
+        let lock = crate::util::DirLock::lock_exclusive(self.anneal_run_root.clone())?;
         Ok(LockedRoots { roots: self, anneal_run_root: lock, llbc_override: None })
     }
 
-    pub fn cargo_target_dir(&self) -> PathBuf {
+    pub fn cargo_target_dir(&self) -> std::path::PathBuf {
         self.anneal_global_root.join("cargo_target")
     }
 }
 
-/// A wrapper around `Roots` that proves the build lock is held.
+/// A wrapper around [`crate::resolve::Roots`] that proves the build lock is held.
 ///
 /// This struct is the *only* way to access paths within the Anneal build
 /// directory (e.g., LLBC output, Lean generation). This enforces that all
@@ -173,11 +167,11 @@ impl Roots {
 pub struct LockedRoots<'a> {
     roots: &'a Roots,
     anneal_run_root: crate::util::DirLock,
-    pub llbc_override: Option<PathBuf>,
+    pub llbc_override: Option<std::path::PathBuf>,
 }
 
 impl<'a> LockedRoots<'a> {
-    pub fn llbc_root(&self) -> PathBuf {
+    pub fn llbc_root(&self) -> std::path::PathBuf {
         if let Some(ref over) = self.llbc_override {
             over.clone()
         } else {
@@ -185,21 +179,21 @@ impl<'a> LockedRoots<'a> {
         }
     }
 
-    pub fn lean_root(&self) -> PathBuf {
+    pub fn lean_root(&self) -> std::path::PathBuf {
         self.anneal_run_root.path.join("lean")
     }
 
-    pub fn lean_generated_root(&self) -> PathBuf {
+    pub fn lean_generated_root(&self) -> std::path::PathBuf {
         self.lean_root().join("generated")
     }
 
     // We expose the Cargo target directory for convenience, as it is used
     // by downstream tools like Charon to coordinate dependency artifacts.
-    pub fn cargo_target_dir(&self) -> PathBuf {
+    pub fn cargo_target_dir(&self) -> std::path::PathBuf {
         self.roots.cargo_target_dir()
     }
 
-    pub fn workspace(&self) -> &PathBuf {
+    pub fn workspace(&self) -> &std::path::PathBuf {
         &self.roots.workspace
     }
 }
@@ -207,9 +201,9 @@ impl<'a> LockedRoots<'a> {
 /// Resolves all verification roots.
 ///
 /// Each entry represents a distinct compilation artifact to be verified.
-pub fn resolve_roots(args: &Args) -> Result<Roots> {
+pub fn resolve_roots(args: &Args) -> anyhow::Result<Roots> {
     log::trace!("resolve_roots({:?})", args);
-    let mut cmd = MetadataCommand::new();
+    let mut cmd = cargo_metadata::MetadataCommand::new();
 
     if let Some(path) = &args.manifest.manifest_path {
         cmd.manifest_path(path);
@@ -273,7 +267,7 @@ pub fn resolve_roots(args: &Args) -> Result<Roots> {
     Ok(roots)
 }
 
-fn resolve_run_roots(metadata: &Metadata) -> (PathBuf, PathBuf) {
+fn resolve_run_roots(metadata: &cargo_metadata::Metadata) -> (std::path::PathBuf, std::path::PathBuf) {
     log::trace!("resolve_run_root");
     log::debug!("workspace_root: {:?}", metadata.workspace_root.as_std_path());
     // NOTE: Automatically handles `CARGO_TARGET_DIR` env var.
@@ -292,7 +286,7 @@ fn resolve_run_roots(metadata: &Metadata) -> (PathBuf, PathBuf) {
     // build directory name remains consistent for the same workspace root,
     // avoiding unnecessary cache invalidation.
     let workspace_root_hash = {
-        let mut hasher = Sha256::new();
+        let mut hasher = sha2::Sha256::new();
         hasher.update(b"anneal_build_salt");
         hasher.update(metadata.workspace_root.as_str().as_bytes());
         let result = hasher.finalize();
@@ -307,13 +301,13 @@ fn resolve_run_roots(metadata: &Metadata) -> (PathBuf, PathBuf) {
 
 /// Resolves which packages to process based on workspace flags and CWD.
 fn resolve_packages<'a>(
-    metadata: &'a Metadata,
+    metadata: &'a cargo_metadata::Metadata,
     args: &clap_cargo::Workspace,
     manifest_path: Option<&std::path::Path>,
-) -> Result<Vec<&'a Package>> {
+) -> anyhow::Result<Vec<&'a cargo_metadata::Package>> {
     log::trace!("resolve_packages(workspace: {}, all: {})", args.workspace, args.all);
     let mut packages = if !args.package.is_empty() {
-        // Resolve explicitly selected packages (-p / --package)
+        // Resolve explicitly selected packages (-p / --package).
         args.package
             .iter()
             .map(|name| {
@@ -321,9 +315,9 @@ fn resolve_packages<'a>(
                     .packages
                     .iter()
                     .find(|p| p.name == *name)
-                    .ok_or_else(|| anyhow!("Package '{}' not found in workspace", name))
+                    .ok_or_else(|| anyhow::anyhow!("Package '{}' not found in workspace", name))
             })
-            .collect::<Result<Vec<_>>>()?
+            .collect::<anyhow::Result<Vec<_>>>()?
     } else if args.workspace || args.all {
         // Resolve entire workspace (--workspace / --all). This explicitly
         // selects all workspace members, ignoring any packages that might be
@@ -340,7 +334,7 @@ fn resolve_packages<'a>(
         let cwd = {
             let cwd_candidate = manifest_path
                 .map(|p| p.to_path_buf())
-                .unwrap_or_else(|| env::current_dir().unwrap_or_default())
+                .unwrap_or_else(|| std::env::current_dir().unwrap_or_default())
                 .canonicalize()
                 .context("Failed to canonicalize CWD")?;
 
@@ -353,7 +347,7 @@ fn resolve_packages<'a>(
             }
         };
 
-        // Find the package whose manifest directory is an ancestor of CWD
+        // Find the package whose manifest directory is an ancestor of CWD.
         let current_pkg = metadata.packages.iter().find(|p| {
             let manifest_dir = p.manifest_path.parent().unwrap();
             cwd.starts_with(manifest_dir)
@@ -371,14 +365,14 @@ fn resolve_packages<'a>(
                     .filter_map(|id| metadata.packages.iter().find(|p| &p.id == id))
                     .collect()
             } else {
-                return Err(anyhow!(
+                return Err(anyhow::anyhow!(
                     "Could not determine package from current directory. Please use -p <NAME> or --workspace."
                 ));
             }
         }
     };
 
-    // Filter out excluded packages (--exclude)
+    // Filter out excluded packages (--exclude).
     if !args.exclude.is_empty() {
         packages.retain(|p| !args.exclude.contains(&p.name));
     }
@@ -398,9 +392,9 @@ fn resolve_packages<'a>(
 /// Verifying them independently ensures we cover all intended compilation
 /// modes.
 fn resolve_targets<'a>(
-    package: &'a Package,
+    package: &'a cargo_metadata::Package,
     args: &Args,
-) -> Result<Vec<(&'a Target, AnnealTargetKind)>> {
+) -> anyhow::Result<Vec<(&'a cargo_metadata::Target, AnnealTargetKind)>> {
     log::trace!("resolve_targets({})", package.name);
     let default_mode = !args.lib
         && args.bin.is_empty()
@@ -445,10 +439,10 @@ fn resolve_targets<'a>(
 /// Scans the package graph to ensure all local dependencies are contained
 /// within the workspace root. Returns an error if an external path dependency
 /// is found.
-pub fn check_for_external_deps(metadata: &Metadata) -> Result<()> {
+pub fn check_for_external_deps(metadata: &cargo_metadata::Metadata) -> anyhow::Result<()> {
     log::trace!("check_for_external_deps");
-    // Canonicalize workspace root to handle symlinks correctly
-    let workspace_root = fs::canonicalize(&metadata.workspace_root)
+    // Canonicalize workspace root to handle symlinks correctly.
+    let workspace_root = std::fs::canonicalize(&metadata.workspace_root)
         .context("Failed to canonicalize workspace root")?;
 
     for pkg in &metadata.packages {
@@ -458,11 +452,11 @@ pub fn check_for_external_deps(metadata: &Metadata) -> Result<()> {
         if pkg.source.is_none() {
             let pkg_path = pkg.manifest_path.as_std_path();
 
-            // Canonicalize the package path for comparison
-            let canonical_pkg_path = fs::canonicalize(pkg_path)
+            // Canonicalize the package path for comparison.
+            let canonical_pkg_path = std::fs::canonicalize(pkg_path)
                 .with_context(|| format!("Failed to canonicalize path for package {}", pkg.name))?;
 
-            // Check if the package lives outside the workspace tree
+            // Check if the package lives outside the workspace tree.
             if !canonical_pkg_path.starts_with(&workspace_root) {
                 anyhow::bail!(
                     "Unsupported external dependency: '{}' at {:?}.\n\
diff --git a/anneal/v2/src/scanner.rs b/anneal/v2/src/scanner.rs
index be5b3e6724..bda966e159 100644
--- a/anneal/v2/src/scanner.rs
+++ b/anneal/v2/src/scanner.rs
@@ -1,25 +1,18 @@
-use std::collections::HashSet;
-use std::path::PathBuf;
-use sha2::{Digest as _, Sha256};
-
-use crate::{
-    parse::ParsedLeanItem,
-    resolve::{AnnealTargetKind, AnnealTargetName, LockedRoots},
-};
+use sha2::Digest as _;
 
 pub struct AnnealArtifact {
-    pub name: AnnealTargetName,
-    pub target_kind: AnnealTargetKind,
+    pub name: crate::resolve::AnnealTargetName,
+    pub target_kind: crate::resolve::AnnealTargetKind,
     /// The path to the crate's `Cargo.toml`.
-    pub manifest_path: PathBuf,
-    pub items: Vec<ParsedLeanItem<crate::parse::hkd::Safe>>,
+    pub manifest_path: std::path::PathBuf,
+    pub items: Vec<crate::parse::ParsedLeanItem<crate::parse::hkd::Safe>>,
     // NOTE: We store `start_from` as a `HashSet` rather than a `Vec` as an
     // optimization: when we encounter items which we can't name (which carry
     // Anneal annotations), we add their parent module to the list of
     // entrypoints. If there are multiple items in the same module, this can
     // lead to duplication in the list of entrypoints. Storing them in a
     // `HashSet` avoids us having to de-dup later.
-    pub start_from: HashSet<String>,
+    pub start_from: std::collections::HashSet<String>,
 }
 
 impl AnnealArtifact {
@@ -31,7 +24,7 @@ impl AnnealArtifact {
     /// identifier (no hyphens).
     pub fn artifact_slug(&self) -> String {
         fn hash(data: &[u8]) -> u64 {
-            let mut hasher = Sha256::new();
+            let mut hasher = sha2::Sha256::new();
             hasher.update(data);
             let result = hasher.finalize();
             let mut bytes = [0u8; 8];
@@ -43,7 +36,7 @@ impl AnnealArtifact {
         // (manifest_path, target_name) = ("abc", "def") and ("ab", "cdef"),
         // which would hash identically if we just hashed their concatenation.
         //
-        // Use SHA-256 not for security but rather stability – Rust's
+        // Use SHA-256 not for security but rather stability – Rust's
         // `DefaultHasher` doesn't guarantee stability even across runs of the
         // same binary.
         //
@@ -98,9 +91,9 @@ impl AnnealArtifact {
 
     /// Returns the absolute path to the .llbc file.
     ///
-    /// This method requires `LockedRoots` to ensure that the caller holds the
+    /// This method requires [`crate::resolve::LockedRoots`] to ensure that the caller holds the
     /// build lock before accessing the build artifact path.
-    pub fn llbc_path(&self, roots: &LockedRoots) -> PathBuf {
+    pub fn llbc_path(&self, roots: &crate::resolve::LockedRoots) -> std::path::PathBuf {
         roots.llbc_root().join(self.llbc_file_name())
     }
 }
@@ -127,7 +120,7 @@ pub fn scan_workspace(roots: &crate::resolve::Roots) -> anyhow::Result<Vec<Annea
             }
         }
 
-        // If we found nothing, but it's a bin, assume `main`
+        // If we found nothing, but it's a bin, assume `main`.
         if start_from.is_empty() && target.kind == crate::resolve::AnnealTargetKind::Bin {
             start_from.insert("crate::main".to_string());
         }
@@ -136,7 +129,7 @@ pub fn scan_workspace(roots: &crate::resolve::Roots) -> anyhow::Result<Vec<Annea
             name: target.name.clone(),
             target_kind: target.kind,
             manifest_path: target.manifest_path.clone(),
-            items: vec![], // empty for now
+            items: vec![], // Empty for now.
             start_from,
         });
     }
diff --git a/anneal/v2/src/setup.rs b/anneal/v2/src/setup.rs
index 1048814149..dca295d4f1 100644
--- a/anneal/v2/src/setup.rs
+++ b/anneal/v2/src/setup.rs
@@ -1,9 +1,7 @@
-use std::path::PathBuf;
-use std::process::Command;
-use anyhow::{Result, Context};
+use anyhow::Context as _;
 
 pub struct SetupArgs {
-    pub local_archive: Option<PathBuf>,
+    pub local_archive: Option<std::path::PathBuf>,
 }
 
 exocrate::config! {
@@ -32,14 +30,24 @@ impl Tool {
             Self::Charon => "charon",
         }
     }
+
+    pub fn path(&self, toolchain: &Toolchain) -> std::path::PathBuf {
+        match self {
+            Self::Charon => toolchain.aeneas_bin_dir().join(self.name()),
+        }
+    }
 }
 
 pub struct Toolchain {
-    pub root: PathBuf,
+    pub root: std::path::PathBuf,
+    aeneas_bin_dir: std::path::PathBuf,
+    rust_sysroot: std::path::PathBuf,
+    rust_bin: std::path::PathBuf,
+    rust_lib: std::path::PathBuf,
 }
 
 impl Toolchain {
-    pub fn resolve() -> Result<Self> {
+    pub fn resolve() -> anyhow::Result<Self> {
         let location = if std::env::var("__ANNEAL_LOCAL_DEV").is_ok() {
             exocrate::Location::Local
         } else {
@@ -48,17 +56,58 @@ impl Toolchain {
         let root = CONFIG
             .resolve_installation_dir(location)
             .context("Toolchain not installed. Please run 'cargo anneal setup' first.")?;
-        Ok(Self { root })
+
+        let aeneas_bin_dir = root.join("aeneas").join("bin");
+        let rust_sysroot = root.join("rust");
+        let rust_bin = rust_sysroot.join("bin");
+        let rust_lib = rust_sysroot.join("lib");
+
+        Ok(Self {
+            root,
+            aeneas_bin_dir,
+            rust_sysroot,
+            rust_bin,
+            rust_lib,
+        })
+    }
+
+    pub fn aeneas_bin_dir(&self) -> &std::path::Path {
+        &self.aeneas_bin_dir
+    }
+
+    pub fn rust_sysroot(&self) -> &std::path::Path {
+        &self.rust_sysroot
     }
 
-    pub fn command(&self, tool: Tool) -> Command {
-        let bin_name = tool.name();
-        let managed_path = self.root.join("aeneas").join("bin").join(bin_name);
-        Command::new(managed_path)
+    pub fn rust_bin(&self) -> &std::path::Path {
+        &self.rust_bin
+    }
+
+    pub fn rust_lib(&self) -> &std::path::Path {
+        &self.rust_lib
+    }
+
+    pub fn command(&self, tool: Tool) -> std::process::Command {
+        std::process::Command::new(tool.path(self))
+    }
+
+    #[cfg(test)]
+    pub fn new_test(root: std::path::PathBuf) -> Self {
+        let aeneas_bin_dir = root.join("aeneas").join("bin");
+        let rust_sysroot = root.join("rust");
+        let rust_bin = rust_sysroot.join("bin");
+        let rust_lib = rust_sysroot.join("lib");
+        Self {
+            root,
+            aeneas_bin_dir,
+            rust_sysroot,
+            rust_bin,
+            rust_lib,
+        }
     }
 }
 
-pub fn run_setup(args: SetupArgs) -> Result<()> {
+pub fn run_setup(args: SetupArgs) -> anyhow::Result<()> {
     let location = if std::env::var("__ANNEAL_LOCAL_DEV").is_ok() {
         exocrate::Location::Local
     } else {
@@ -75,3 +124,89 @@ pub fn run_setup(args: SetupArgs) -> Result<()> {
     log::info!("anneal toolchain is installed at {:?}", installation_dir);
     Ok(())
 }
+
+#[cfg(feature = "exocrate_tests")]
+pub fn run_test_setup() -> anyhow::Result<()> {
+    // FIXME: Add GitHub actions that will block changes that would update
+    // tests/toolchains/ files if TestSetup were invoked without committing them.
+    
+    println!("Running standard setup...");
+    run_setup(SetupArgs {
+        local_archive: Some("target/anneal-exocrate.tar.zst".into()),
+    })?;
+
+    let toolchain = Toolchain::resolve()?;
+    let dest_dir = std::path::PathBuf::from(env!("CARGO_MANIFEST_DIR"))
+        .join("tests")
+        .join("toolchains")
+        .join("charon-only");
+
+    if dest_dir.exists() {
+        println!("Cleaning existing test toolchain at {:?}", dest_dir);
+        std::fs::remove_dir_all(&dest_dir).context("Failed to clean test toolchain dir")?;
+    }
+    std::fs::create_dir_all(&dest_dir)?;
+
+    let copy_file = |src: &std::path::Path, dest: &std::path::Path| -> anyhow::Result<()> {
+        if let Some(parent) = dest.parent() {
+            std::fs::create_dir_all(parent)?;
+        }
+        std::fs::copy(src, dest)?;
+        let meta = std::fs::metadata(src)?;
+        std::fs::set_permissions(dest, meta.permissions())?;
+        Ok(())
+    };
+
+    println!("Copying Charon binaries...");
+    copy_file(
+        &toolchain.aeneas_bin_dir().join("charon"),
+        &dest_dir.join("aeneas").join("bin").join("charon"),
+    )?;
+    copy_file(
+        &toolchain.aeneas_bin_dir().join("charon-driver"),
+        &dest_dir.join("aeneas").join("bin").join("charon-driver"),
+    )?;
+
+    println!("Copying rustc binary...");
+    copy_file(
+        &toolchain.rust_bin().join("rustc"),
+        &dest_dir.join("rust").join("bin").join("rustc"),
+    )?;
+
+    println!("Copying rust libraries (this may take a while)...");
+    let src_lib = toolchain.rust_lib();
+    let dest_lib = dest_dir.join("rust").join("lib");
+    
+    for entry in walkdir::WalkDir::new(&src_lib) {
+        let entry = entry?;
+        let rel_path = entry.path().strip_prefix(&src_lib)?;
+        let dest_path = dest_lib.join(rel_path);
+        if entry.file_type().is_dir() {
+            std::fs::create_dir_all(&dest_path)?;
+        } else {
+            copy_file(entry.path(), &dest_path)?;
+        }
+    }
+
+    println!("Test toolchain successfully set up at {:?}", dest_dir);
+    Ok(())
+}
+
+#[cfg(all(test, feature = "exocrate_tests"))]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_toolchain_paths() {
+        // Ensure toolchain is installed locally for test.
+        unsafe { std::env::set_var("__ANNEAL_LOCAL_DEV", "1"); }
+        
+        let toolchain = Toolchain::resolve().expect("Failed to resolve toolchain");
+        
+        assert!(toolchain.root.is_dir(), "root is not a directory: {:?}", toolchain.root);
+        assert!(toolchain.aeneas_bin_dir().is_dir(), "aeneas_bin_dir is not a directory: {:?}", toolchain.aeneas_bin_dir());
+        assert!(toolchain.rust_sysroot().is_dir(), "rust_sysroot is not a directory: {:?}", toolchain.rust_sysroot());
+        assert!(toolchain.rust_bin().is_dir(), "rust_bin is not a directory: {:?}", toolchain.rust_bin());
+        assert!(toolchain.rust_lib().is_dir(), "rust_lib is not a directory: {:?}", toolchain.rust_lib());
+    }
+}
diff --git a/anneal/v2/src/util.rs b/anneal/v2/src/util.rs
index 4d1dcefa8c..af365b048e 100644
--- a/anneal/v2/src/util.rs
+++ b/anneal/v2/src/util.rs
@@ -1,8 +1,6 @@
-use std::path::{Path, PathBuf};
-
-use anyhow::{Context, Result};
-use fs2::FileExt;
-use walkdir::WalkDir;
+use anyhow::Context as _;
+use fs2::FileExt as _;
+use std::io::BufRead as _;
 
 /// Represents an active, exclusive lock on a directory.
 ///
@@ -10,8 +8,8 @@ use walkdir::WalkDir;
 /// guarding the specified directory.
 pub struct DirLock {
     /// The path to the directory being guarded.
-    pub path: PathBuf,
-    // Kept alive to hold the flock
+    pub path: std::path::PathBuf,
+    // Kept alive to hold the flock.
     _file: std::fs::File,
 }
 
@@ -23,7 +21,7 @@ impl DirLock {
     /// the directory itself to avoid platform-specific issues with
     /// directory locking and to ensure the lock file persists even if
     /// the directory is cleaned.
-    pub fn lock_exclusive(path: PathBuf) -> Result<Self> {
+    pub fn lock_exclusive(path: std::path::PathBuf) -> anyhow::Result<Self> {
         let file = Self::open_lock_file(&path)?;
         file.lock_exclusive()
             .with_context(|| format!("Failed to acquire exclusive lock on {:?}", path))?;
@@ -34,17 +32,17 @@ impl DirLock {
     ///
     /// Multiple processes can hold shared locks simultaneously, but an
     /// exclusive lock will block until all shared locks are released.
-    pub fn lock_shared(path: PathBuf) -> Result<Self> {
+    pub fn lock_shared(path: std::path::PathBuf) -> anyhow::Result<Self> {
         let file = Self::open_lock_file(&path)?;
         file.lock_shared()
             .with_context(|| format!("Failed to acquire shared lock on {:?}", path))?;
         Ok(Self { path, _file: file })
     }
 
-    fn open_lock_file(path: &std::path::Path) -> Result<std::fs::File> {
+    fn open_lock_file(path: &std::path::Path) -> anyhow::Result<std::fs::File> {
         let lock_path = path.join(".lock");
 
-        // Ensure the directory exists
+        // Ensure the directory exists.
         if let Some(parent) = lock_path.parent() {
             std::fs::create_dir_all(parent).with_context(|| {
                 format!("Failed to create directory for lock file: {:?}", parent)
@@ -72,9 +70,9 @@ impl DirLock {
 
 /// Walks a directory recursively and replaces string patterns inside `.trace`
 /// files. This is used to patch non-portable paths generated by Lake.
-pub fn patch_trace_files(dir: &Path, replacements: &[(&str, &str)]) -> Result<()> {
+pub fn patch_trace_files(dir: &std::path::Path, replacements: &[(&str, &str)]) -> anyhow::Result<()> {
     if dir.exists() {
-        let walker = WalkDir::new(dir).into_iter();
+        let walker = walkdir::WalkDir::new(dir).into_iter();
         for entry in walker {
             let entry = entry.context("Failed to walk directory for trace patching")?;
             let path = entry.path();
@@ -94,3 +92,86 @@ pub fn patch_trace_files(dir: &Path, replacements: &[(&str, &str)]) -> Result<()
     }
     Ok(())
 }
+
+/// Prepends a path to an existing environment variable,
+/// separating them with a colon if the variable is not empty. This is used
+/// to inject our managed Rust toolchain paths before the system paths.
+pub(crate) fn prepend_to_env_var(var_name: &str, new_path: &std::path::Path) -> std::ffi::OsString {
+    let current_val = std::env::var_os(var_name).unwrap_or_default();
+    let mut combined = new_path.to_path_buf().into_os_string();
+    if !current_val.is_empty() {
+        combined.push(":");
+        combined.push(current_val);
+    }
+    combined
+}
+
+/// OS command-line length limits (Windows is ~32k; Linux `ARG_MAX` is
+/// usually larger, but variable).
+pub(crate) const ARG_CHAR_LIMIT: usize = 32_768;
+
+pub(crate) struct ProcessOutput {
+    pub status: std::process::ExitStatus,
+    pub stderr_lines: Vec<String>,
+}
+
+/// Spawns a child process, drains its stderr in a background thread, and processes
+/// its stdout line-by-line in the main thread while showing a progress spinner.
+pub(crate) fn run_command_with_progress<F>(
+    mut cmd: std::process::Command,
+    progress_msg: &str,
+    mut process_stdout_line: F,
+) -> anyhow::Result<ProcessOutput>
+where
+    F: FnMut(&str, &indicatif::ProgressBar) -> anyhow::Result<()>,
+{
+    cmd.stdout(std::process::Stdio::piped());
+    cmd.stderr(std::process::Stdio::piped());
+
+    let mut child = cmd.spawn().context("Failed to spawn child process")?;
+
+    let stderr_buffer = std::sync::Arc::new(std::sync::Mutex::new(Vec::new()));
+    let stderr_buffer_clone = std::sync::Arc::clone(&stderr_buffer);
+
+    let mut stderr_thread = None;
+    if let Some(stderr) = child.stderr.take() {
+        stderr_thread = Some(std::thread::spawn(move || {
+            let reader = std::io::BufReader::new(stderr);
+            for line in reader.lines().map_while(Result::ok) {
+                stderr_buffer_clone.lock().unwrap().push(line);
+            }
+        }));
+    }
+
+    let pb = indicatif::ProgressBar::new_spinner();
+    pb.set_style(
+        indicatif::ProgressStyle::default_spinner()
+            .template("{spinner:.green} {msg}")
+            .unwrap(),
+    );
+    pb.enable_steady_tick(std::time::Duration::from_millis(100));
+    pb.set_message(progress_msg.to_string());
+
+    if let Some(stdout) = child.stdout.take() {
+        let reader = std::io::BufReader::new(stdout);
+        for line in reader.lines().map_while(Result::ok) {
+            process_stdout_line(&line, &pb)?;
+            pb.tick();
+        }
+    }
+
+    pb.finish_and_clear();
+
+    let status = child.wait().context("Failed to wait for child process")?;
+
+    if let Some(thread) = stderr_thread {
+        let _ = thread.join();
+    }
+
+    let stderr_lines = std::sync::Arc::try_unwrap(stderr_buffer)
+        .unwrap()
+        .into_inner()
+        .unwrap();
+
+    Ok(ProcessOutput { status, stderr_lines })
+}