diff --git a/anneal/v2/Cargo.lock b/anneal/v2/Cargo.lock
index b546668876..0d13555673 100644
--- a/anneal/v2/Cargo.lock
+++ b/anneal/v2/Cargo.lock
@@ -2,12 +2,33 @@
 # It is not intended for manual editing.
 version = 4
 
+[[package]]
+name = "addr2line"
+version = "0.25.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1b5d307320b3181d6d7954e663bd7c774a838b8220fe0593c86d9fb09f498b4b"
+dependencies = [
+ "gimli",
+]
+
 [[package]]
 name = "adler2"
 version = "2.0.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "320119579fcad9c21884f5c4861d16174d0e06250625266f50fe6898340abefa"
 
+[[package]]
+name = "ahash"
+version = "0.8.12"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5a15f179cd60c4584b8a8c596927aadc462e27f2ca70c04e0071964a73ba7a75"
+dependencies = [
+ "cfg-if",
+ "once_cell",
+ "version_check",
+ "zerocopy",
+]
+
 [[package]]
 name = "aho-corasick"
 version = "1.1.4"
@@ -17,6 +38,32 @@ dependencies = [
  "memchr",
 ]
 
+[[package]]
+name = "annotate-snippets"
+version = "0.12.16"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f211a51805bc641f3ad5b7664c77d2547af685cc33b4cd8d31964027a46f13f1"
+dependencies = [
+ "anstyle",
+ "memchr",
+ "unicode-width 0.2.2",
+]
+
+[[package]]
+name = "anstream"
+version = "0.6.21"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "43d5b281e737544384e969a5ccad3f1cdd24b48086a0fc1b2a5262a26b8f4f4a"
+dependencies = [
+ "anstyle",
+ "anstyle-parse 0.2.7",
+ "anstyle-query",
+ "anstyle-wincon",
+ "colorchoice",
+ "is_terminal_polyfill",
+ "utf8parse",
+]
+
 [[package]]
 name = "anstream"
 version = "1.0.0"
@@ -24,7 +71,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "824a212faf96e9acacdbd09febd34438f8f711fb84e09a8916013cd7815ca28d"
 dependencies = [
  "anstyle",
- "anstyle-parse",
+ "anstyle-parse 1.0.0",
  "anstyle-query",
  "anstyle-wincon",
  "colorchoice",
@@ -38,6 +85,15 @@ version = "1.0.14"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "940b3a0ca603d1eade50a4846a2afffd5ef57a9feac2c0e2ec2e14f9ead76000"
 
+[[package]]
+name = "anstyle-parse"
+version = "0.2.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "4e7644824f0aa2c7b9384579234ef10eb7efb6a0deb83f9630a49594dd9c15c2"
+dependencies = [
+ "utf8parse",
+]
+
 [[package]]
 name = "anstyle-parse"
 version = "1.0.0"
@@ -73,6 +129,75 @@ version = "1.0.102"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "7f202df86484c868dbad7eaa557ef785d5c66295e41b460ef922eca0723b842c"
 
+[[package]]
+name = "ar_archive_writer"
+version = "0.5.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7eb93bbb63b9c227414f6eb3a0adfddca591a8ce1e9b60661bb08969b87e340b"
+dependencies = [
+ "object",
+]
+
+[[package]]
+name = "arrayvec"
+version = "0.7.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7c02d123df017efcdfbd739ef81735b36c5ba83ec3c59c80a9d7ecc718f92e50"
+
+[[package]]
+name = "assert_cmd"
+version = "2.2.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2aa3a22042e45de04255c7bf3626e239f450200fd0493c1e382263544b20aea6"
+dependencies = [
+ "anstyle",
+ "bstr",
+ "libc",
+ "predicates",
+ "predicates-core",
+ "predicates-tree",
+ "wait-timeout",
+]
+
+[[package]]
+name = "atomic-polyfill"
+version = "1.0.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8cf2bce30dfe09ef0bfaef228b9d414faaf7e563035494d7fe092dba54b300f4"
+dependencies = [
+ "critical-section",
+]
+
+[[package]]
+name = "autocfg"
+version = "1.5.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f2032f911046de80f0a198e0901378627c33f59ea0ac00e363d481118bd70a53"
+
+[[package]]
+name = "backtrace"
+version = "0.3.76"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "bb531853791a215d7c62a30daf0dde835f381ab5de4589cfe7c649d2cbe92bd6"
+dependencies = [
+ "addr2line",
+ "cfg-if",
+ "libc",
+ "miniz_oxide",
+ "object",
+ "rustc-demangle",
+ "windows-link",
+]
+
+[[package]]
+name = "backtrace-ext"
+version = "0.2.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "537beee3be4a18fb023b570f80e3ae28003db9167a751266b259926e25539d50"
+dependencies = [
+ "backtrace",
+]
+
 [[package]]
 name = "base64"
 version = "0.22.1"
@@ -81,9 +206,9 @@ checksum = "72b3254f16251a8381aa12e40e3c4d2f0199f8c6508fbecb9d91f575e0fbb8c6"
 
 [[package]]
 name = "bitflags"
-version = "2.11.1"
+version = "2.12.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "c4512299f36f043ab09a583e57bceb5a5aab7a73db1805848e8fef3c9e8c78b3"
+checksum = "84d7ced0ae9557296835c32bf1b1e02b44c746701f898460fb000d7eaa84f00a"
 
 [[package]]
 name = "block-buffer"
@@ -94,28 +219,107 @@ dependencies = [
  "generic-array",
 ]
 
+[[package]]
+name = "brownstone"
+version = "3.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c5839ee4f953e811bfdcf223f509cb2c6a3e1447959b0bff459405575bc17f22"
+dependencies = [
+ "arrayvec",
+]
+
+[[package]]
+name = "bstr"
+version = "1.12.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "63044e1ae8e69f3b5a92c736ca6269b8d12fa7efe39bf34ddb06d102cf0e2cab"
+dependencies = [
+ "memchr",
+ "regex-automata",
+ "serde",
+]
+
+[[package]]
+name = "bumpalo"
+version = "3.20.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "72f5acc6cb2ba439de613abc23857ec3d78374d8ed5ac84e9d11336e87da8649"
+
+[[package]]
+name = "byteorder"
+version = "1.5.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1fd0f2584146f6f2ef48085050886acf353beff7305ebd1ae69500e27c67f64b"
+
 [[package]]
 name = "bytes"
 version = "1.11.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "1e748733b7cbc798e1434b6ac524f0c1ff2ab456fe201501e6497c8417a4fc33"
 
+[[package]]
+name = "camino"
+version = "1.2.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e629a66d692cb9ff1a1c664e41771b3dcaf961985a9774c0eb0bd1b51cf60a48"
+dependencies = [
+ "serde_core",
+]
+
 [[package]]
 name = "cargo-anneal"
 version = "0.1.0-alpha.22"
 dependencies = [
+ "anyhow",
+ "cargo_metadata",
+ "charon",
  "clap",
+ "clap-cargo",
  "env_logger",
  "exocrate",
+ "fs2",
+ "indicatif",
  "log",
+ "miette",
+ "rayon",
+ "serde",
+ "serde_json",
+ "sha2",
+ "tempfile",
+ "thiserror",
  "toml_const",
+ "walkdir",
+]
+
+[[package]]
+name = "cargo-platform"
+version = "0.3.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "dd0061da739915fae12ea00e16397555ed4371a6bb285431aab930f61b0aa4ba"
+dependencies = [
+ "serde",
+ "serde_core",
+]
+
+[[package]]
+name = "cargo_metadata"
+version = "0.23.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ef987d17b0a113becdd19d3d0022d04d7ef41f9efe4f3fb63ac44ba61df3ade9"
+dependencies = [
+ "camino",
+ "cargo-platform",
+ "semver",
+ "serde",
+ "serde_json",
+ "thiserror",
 ]
 
 [[package]]
 name = "cc"
-version = "1.2.62"
+version = "1.2.63"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a1dce859f0832a7d088c4f1119888ab94ef4b5d6795d1ce05afb7fe159d79f98"
+checksum = "556e016178bb5662a08681bbe0f00f8e17631781a4dfc8c45e466e4b185ec27f"
 dependencies = [
  "find-msvc-tools",
  "jobserver",
@@ -129,6 +333,57 @@ version = "1.0.4"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801"
 
+[[package]]
+name = "charon"
+version = "0.1.210"
+source = "git+https://github.com/AeneasVerif/charon.git?rev=0c91ca1a8e002d6bfa8d8f1f452804fce2f92cf1#0c91ca1a8e002d6bfa8d8f1f452804fce2f92cf1"
+dependencies = [
+ "annotate-snippets",
+ "anstream 0.6.21",
+ "anyhow",
+ "assert_cmd",
+ "clap",
+ "colored",
+ "convert_case",
+ "derive_generic_visitor",
+ "either",
+ "env_logger",
+ "extension-traits",
+ "fraction",
+ "hashbrown 0.15.5",
+ "hax-adt-into",
+ "index_vec",
+ "indexmap",
+ "indoc",
+ "itertools",
+ "lazy_static",
+ "log",
+ "macros",
+ "nom",
+ "nom-supreme",
+ "num-bigint",
+ "paste",
+ "petgraph",
+ "postcard",
+ "rustc-hash",
+ "rustc_version",
+ "serde",
+ "serde_json",
+ "serde_stacker",
+ "serde_state",
+ "smallvec",
+ "stacker",
+ "strip-ansi-escapes",
+ "take_mut",
+ "tempfile",
+ "toml 0.8.23",
+ "tracing",
+ "tracing-subscriber",
+ "tracing-tree",
+ "ustr",
+ "which",
+]
+
 [[package]]
 name = "clap"
 version = "4.6.1"
@@ -139,13 +394,26 @@ dependencies = [
  "clap_derive",
 ]
 
+[[package]]
+name = "clap-cargo"
+version = "0.18.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "936551935c8258754bb8216aec040957d261f977303754b9bf1a213518388006"
+dependencies = [
+ "anstyle",
+ "cargo_metadata",
+ "clap",
+ "serde",
+ "serde_json",
+]
+
 [[package]]
 name = "clap_builder"
 version = "4.6.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "714a53001bf66416adb0e2ef5ac857140e7dc3a0c48fb28b2f10762fc4b5069f"
 dependencies = [
- "anstream",
+ "anstream 1.0.0",
  "anstyle",
  "clap_lex",
  "strsim",
@@ -160,7 +428,7 @@ dependencies = [
  "heck",
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.117",
 ]
 
 [[package]]
@@ -169,12 +437,52 @@ version = "1.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "c8d4a3bb8b1e0c1050499d1815f5ab16d04f0959b233085fb31653fbfc9d98f9"
 
+[[package]]
+name = "cobs"
+version = "0.3.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0fa961b519f0b462e3a3b4a34b64d119eeaca1d59af726fe450bbba07a9fc0a1"
+dependencies = [
+ "thiserror",
+]
+
 [[package]]
 name = "colorchoice"
 version = "1.0.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "1d07550c9036bf2ae0c684c4297d503f838287c83c53686d05370d0e139ae570"
 
+[[package]]
+name = "colored"
+version = "2.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "117725a109d387c937a1533ce01b450cbde6b88abceea8473c4d7a85853cda3c"
+dependencies = [
+ "lazy_static",
+ "windows-sys 0.59.0",
+]
+
+[[package]]
+name = "console"
+version = "0.16.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d64e8af5551369d19cf50138de61f1c42074ab970f74e99be916646777f8fc87"
+dependencies = [
+ "encode_unicode",
+ "libc",
+ "unicode-width 0.2.2",
+ "windows-sys 0.61.2",
+]
+
+[[package]]
+name = "convert_case"
+version = "0.6.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ec182b0ca2f35d8fc196cf3404988fd8b8c739a4d270ff118a398feb0cbec1ca"
+dependencies = [
+ "unicode-segmentation",
+]
+
 [[package]]
 name = "cpufeatures"
 version = "0.2.17"
@@ -193,6 +501,37 @@ dependencies = [
  "cfg-if",
 ]
 
+[[package]]
+name = "critical-section"
+version = "1.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "790eea4361631c5e7d22598ecd5723ff611904e3344ce8720784c93e3d83d40b"
+
+[[package]]
+name = "crossbeam-deque"
+version = "0.8.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9dd111b7b7f7d55b72c0a6ae361660ee5853c9af73f70c3c2ef6858b950e2e51"
+dependencies = [
+ "crossbeam-epoch",
+ "crossbeam-utils",
+]
+
+[[package]]
+name = "crossbeam-epoch"
+version = "0.9.18"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5b82ac4a3c2ca9c3460964f020e1402edd5753411d7737aa39c3714ad1b5420e"
+dependencies = [
+ "crossbeam-utils",
+]
+
+[[package]]
+name = "crossbeam-utils"
+version = "0.8.21"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d0a5c400df2834b80a4c3327b3aad3a4c4cd4de0629063962b03235697506a28"
+
 [[package]]
 name = "crypto-common"
 version = "0.1.7"
@@ -203,6 +542,79 @@ dependencies = [
  "typenum",
 ]
 
+[[package]]
+name = "darling"
+version = "0.20.11"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "fc7f46116c46ff9ab3eb1597a45688b6715c6e628b5c133e288e709a29bcb4ee"
+dependencies = [
+ "darling_core",
+ "darling_macro",
+]
+
+[[package]]
+name = "darling_core"
+version = "0.20.11"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0d00b9596d185e565c2207a0b01f8bd1a135483d02d9b7b0a54b11da8d53412e"
+dependencies = [
+ "fnv",
+ "ident_case",
+ "proc-macro2",
+ "quote",
+ "strsim",
+ "syn 2.0.117",
+]
+
+[[package]]
+name = "darling_macro"
+version = "0.20.11"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "fc34b93ccb385b40dc71c6fceac4b2ad23662c7eeb248cf10d529b7e055b6ead"
+dependencies = [
+ "darling_core",
+ "quote",
+ "syn 2.0.117",
+]
+
+[[package]]
+name = "deranged"
+version = "0.5.8"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7cd812cc2bc1d69d4764bd80df88b4317eaef9e773c75226407d9bc0876b211c"
+dependencies = [
+ "powerfmt",
+]
+
+[[package]]
+name = "derive_generic_visitor"
+version = "0.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "21588db07753dafe6460b13faad18bd7e46548ce91ee38f0bc0f7529b3864b82"
+dependencies = [
+ "derive_generic_visitor_macros",
+]
+
+[[package]]
+name = "derive_generic_visitor_macros"
+version = "0.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f3aed1890235ebcf844a24263ecc395c4e57a970f13bcc9948989f22aa051aa7"
+dependencies = [
+ "convert_case",
+ "darling",
+ "itertools",
+ "proc-macro2",
+ "quote",
+ "syn 2.0.117",
+]
+
+[[package]]
+name = "difflib"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6184e33543162437515c2e2b48714794e37845ec9851711914eec9d308f6ebe8"
+
 [[package]]
 name = "digest"
 version = "0.10.7"
@@ -234,6 +646,30 @@ dependencies = [
  "windows-sys 0.61.2",
 ]
 
+[[package]]
+name = "either"
+version = "1.16.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "91622ff5e7162018101f2fea40d6ebf4a78bbe5a49736a2020649edf9693679e"
+
+[[package]]
+name = "embedded-io"
+version = "0.4.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ef1a6892d9eef45c8fa6b9e0086428a2cca8491aca8f787c534a3d6d0bcb3ced"
+
+[[package]]
+name = "embedded-io"
+version = "0.6.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "edd0f118536f44f5ccd48bcb8b111bdc3de888b58c74639dfb034a357d0f206d"
+
+[[package]]
+name = "encode_unicode"
+version = "1.0.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "34aa73646ffb006b8f5147f3dc182bd4bcb190227ce861fc4a4844bf8e3cb2c0"
+
 [[package]]
 name = "env_filter"
 version = "1.0.1"
@@ -244,13 +680,19 @@ dependencies = [
  "regex",
 ]
 
+[[package]]
+name = "env_home"
+version = "0.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c7f84e12ccf0a7ddc17a6c41c93326024c42920d7ee630d04950e6926645c0fe"
+
 [[package]]
 name = "env_logger"
 version = "0.11.10"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "0621c04f2196ac3f488dd583365b9c09be011a4ab8b9f37248ffcc8f6198b56a"
 dependencies = [
- "anstream",
+ "anstream 1.0.0",
  "anstyle",
  "env_filter",
  "jiff",
@@ -288,6 +730,35 @@ dependencies = [
  "zstd",
 ]
 
+[[package]]
+name = "ext-trait"
+version = "1.0.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d772df1c1a777963712fb68e014235e80863d6a91a85c4e06ba2d16243a310e5"
+dependencies = [
+ "ext-trait-proc_macros",
+]
+
+[[package]]
+name = "ext-trait-proc_macros"
+version = "1.0.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1ab7934152eaf26aa5aa9f7371408ad5af4c31357073c9e84c3b9d7f11ad639a"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn 1.0.109",
+]
+
+[[package]]
+name = "extension-traits"
+version = "1.0.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a296e5a895621edf9fa8329c83aa1cb69a964643e36cf54d8d7a69b789089537"
+dependencies = [
+ "ext-trait",
+]
+
 [[package]]
 name = "fastrand"
 version = "2.4.1"
@@ -310,6 +781,12 @@ version = "0.1.9"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "5baebc0774151f905a1a2cc41989300b1e6fbb29aff0ceffa1064fdd3088d582"
 
+[[package]]
+name = "fixedbitset"
+version = "0.5.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1d674e81391d1e1ab681a28d99df07927c6d4aa5b027d7da16ba32d1d21ecd99"
+
 [[package]]
 name = "flate2"
 version = "1.1.9"
@@ -320,12 +797,28 @@ dependencies = [
  "miniz_oxide",
 ]
 
+[[package]]
+name = "fnv"
+version = "1.0.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3f9eec918d3f24069decb9af1554cad7c880e2da24a9afd88aca000531ab82c1"
+
 [[package]]
 name = "foldhash"
 version = "0.1.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "d9c4f5dac5e15c24eb999c26181a6ca40b39fe946cbe4c263c7209467bc83af2"
 
+[[package]]
+name = "fraction"
+version = "0.15.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e076045bb43dac435333ed5f04caf35c7463631d0dae2deb2638d94dd0a5b872"
+dependencies = [
+ "lazy_static",
+ "num",
+]
+
 [[package]]
 name = "fs2"
 version = "0.4.3"
@@ -336,6 +829,30 @@ dependencies = [
  "winapi",
 ]
 
+[[package]]
+name = "futures-core"
+version = "0.3.32"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7e3450815272ef58cec6d564423f6e755e25379b217b0bc688e295ba24df6b1d"
+
+[[package]]
+name = "futures-task"
+version = "0.3.32"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "037711b3d59c33004d3856fbdc83b99d4ff37a24768fa1be9ce3538a1cde4393"
+
+[[package]]
+name = "futures-util"
+version = "0.3.32"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "389ca41296e6190b48053de0321d02a77f32f8a5d2461dd38762c0593805c6d6"
+dependencies = [
+ "futures-core",
+ "futures-task",
+ "pin-project-lite",
+ "slab",
+]
+
 [[package]]
 name = "generic-array"
 version = "0.14.7"
@@ -382,6 +899,21 @@ dependencies = [
  "wasip3",
 ]
 
+[[package]]
+name = "gimli"
+version = "0.32.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "e629b9b98ef3dd8afe6ca2bd0f89306cec16d43d907889945bc5d6687f2f13c7"
+
+[[package]]
+name = "hash32"
+version = "0.2.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b0c35f58762feb77d74ebe43bdbc3210f09be9fe6742234d573bacc26ed92b67"
+dependencies = [
+ "byteorder",
+]
+
 [[package]]
 name = "hashbrown"
 version = "0.15.5"
@@ -397,6 +929,32 @@ version = "0.17.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "ed5909b6e89a2db4456e54cd5f673791d7eca6732202bbf2a9cc504fe2f9b84a"
 
+[[package]]
+name = "hax-adt-into"
+version = "0.3.5"
+source = "git+https://github.com/AeneasVerif/charon.git?rev=0c91ca1a8e002d6bfa8d8f1f452804fce2f92cf1#0c91ca1a8e002d6bfa8d8f1f452804fce2f92cf1"
+dependencies = [
+ "itertools",
+ "proc-macro2",
+ "quote",
+ "syn 1.0.109",
+ "tracing",
+]
+
+[[package]]
+name = "heapless"
+version = "0.7.17"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "cdc6457c0eb62c71aac4bc17216026d8410337c4126773b9c5daba343f17964f"
+dependencies = [
+ "atomic-polyfill",
+ "hash32",
+ "rustc_version",
+ "serde",
+ "spin",
+ "stable_deref_trait",
+]
+
 [[package]]
 name = "heck"
 version = "0.5.0"
@@ -425,6 +983,27 @@ version = "2.3.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "3d3067d79b975e8844ca9eb072e16b31c3c1c36928edf9c6789548c524d0d954"
 
+[[package]]
+name = "ident_case"
+version = "1.0.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b9e0384b61958566e926dc50660321d12159025e767c18e043daf26b70104c39"
+
+[[package]]
+name = "indent_write"
+version = "2.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0cfe9645a18782869361d9c8732246be7b410ad4e919d3609ebabdac00ba12c3"
+
+[[package]]
+name = "index_vec"
+version = "0.1.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "44faf5bb8861a9c72e20d3fb0fdbd59233e43056e2b80475ab0aacdc2e781355"
+dependencies = [
+ "serde",
+]
+
 [[package]]
 name = "indexmap"
 version = "2.14.0"
@@ -437,99 +1016,354 @@ dependencies = [
  "serde_core",
 ]
 
+[[package]]
+name = "indicatif"
+version = "0.18.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "25470f23803092da7d239834776d653104d551bc4d7eacaf31e6837854b8e9eb"
+dependencies = [
+ "console",
+ "portable-atomic",
+ "unicode-segmentation",
+ "unicode-width 0.2.2",
+ "unit-prefix",
+ "web-time",
+]
+
+[[package]]
+name = "indoc"
+version = "2.0.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "79cf5c93f93228cf8efb3ba362535fb11199ac548a09ce117c9b1adc3030d706"
+dependencies = [
+ "rustversion",
+]
+
+[[package]]
+name = "is_ci"
+version = "1.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7655c9839580ee829dfacba1d1278c2b7883e50a277ff7541299489d6bdfdc45"
+
 [[package]]
 name = "is_terminal_polyfill"
 version = "1.70.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a6cb138bb79a146c1bd460005623e142ef0181e3d0219cb493e02f7d08a35695"
+checksum = "a6cb138bb79a146c1bd460005623e142ef0181e3d0219cb493e02f7d08a35695"
+
+[[package]]
+name = "itertools"
+version = "0.13.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "413ee7dfc52ee1a4949ceeb7dbc8a33f2d6c088194d9f922fb8318faf1f01186"
+dependencies = [
+ "either",
+]
+
+[[package]]
+name = "itoa"
+version = "1.0.18"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8f42a60cbdf9a97f5d2305f08a87dc4e09308d1276d28c869c684d7777685682"
+
+[[package]]
+name = "jiff"
+version = "0.2.28"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "4603d3033e49e2b0e31229fcab20a5d40089c607d975cd9c80551dc69eed9102"
+dependencies = [
+ "jiff-static",
+ "log",
+ "portable-atomic",
+ "portable-atomic-util",
+ "serde_core",
+]
+
+[[package]]
+name = "jiff-static"
+version = "0.2.28"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "782d32378dddf207193ac91cefb848ad41abb58195c95168e1291227a0832b47"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn 2.0.117",
+]
+
+[[package]]
+name = "jobserver"
+version = "0.1.34"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9afb3de4395d6b3e67a780b6de64b51c978ecf11cb9a462c66be7d4ca9039d33"
+dependencies = [
+ "getrandom 0.3.4",
+ "libc",
+]
+
+[[package]]
+name = "joinery"
+version = "2.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "72167d68f5fce3b8655487b8038691a3c9984ee769590f93f2a631f4ad64e4f5"
+
+[[package]]
+name = "js-sys"
+version = "0.3.99"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "142bc4740e452c1e57ade0cbc129f139c9093e354346f0872ef985f4f5cf5f11"
+dependencies = [
+ "cfg-if",
+ "futures-util",
+ "once_cell",
+ "wasm-bindgen",
+]
+
+[[package]]
+name = "lazy_static"
+version = "1.5.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "bbd2bcb4c963f2ddae06a2efc7e9f3591312473c50c6685e1f298068316e66fe"
+
+[[package]]
+name = "leb128fmt"
+version = "0.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "09edd9e8b54e49e587e4f6295a7d29c3ea94d469cb40ab8ca70b288248a81db2"
+
+[[package]]
+name = "libc"
+version = "0.2.186"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "68ab91017fe16c622486840e4c83c9a37afeff978bd239b5293d61ece587de66"
+
+[[package]]
+name = "libredox"
+version = "0.1.17"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f02ab6bace2054fb888a3c16f990117b579d14a3088e472d63c6011fa185c9d3"
+dependencies = [
+ "libc",
+]
+
+[[package]]
+name = "linux-raw-sys"
+version = "0.12.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "32a66949e030da00e8c7d4434b251670a91556f4144941d37452769c25d58a53"
+
+[[package]]
+name = "lock_api"
+version = "0.4.14"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "224399e74b87b5f3557511d98dff8b14089b3dadafcab6bb93eab67d3aace965"
+dependencies = [
+ "scopeguard",
+]
+
+[[package]]
+name = "log"
+version = "0.4.31"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "113b30b4cd05f7c06868fdb2854f66a7b9fece9a48425351cd532e810d74024f"
+
+[[package]]
+name = "macros"
+version = "0.1.0"
+source = "git+https://github.com/AeneasVerif/charon.git?rev=0c91ca1a8e002d6bfa8d8f1f452804fce2f92cf1#0c91ca1a8e002d6bfa8d8f1f452804fce2f92cf1"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn 1.0.109",
+]
+
+[[package]]
+name = "matchers"
+version = "0.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d1525a2a28c7f4fa0fc98bb91ae755d1e2d1505079e05539e35bc876b5d65ae9"
+dependencies = [
+ "regex-automata",
+]
+
+[[package]]
+name = "memchr"
+version = "2.8.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6b947ae49db0d222b1dbc6b113ce7248a3fc3a6ca21b696717bfc000ba4484d8"
+
+[[package]]
+name = "miette"
+version = "7.6.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5f98efec8807c63c752b5bd61f862c165c115b0a35685bdcfd9238c7aeb592b7"
+dependencies = [
+ "backtrace",
+ "backtrace-ext",
+ "cfg-if",
+ "miette-derive",
+ "owo-colors",
+ "supports-color",
+ "supports-hyperlinks",
+ "supports-unicode",
+ "terminal_size",
+ "textwrap",
+ "unicode-width 0.1.14",
+]
+
+[[package]]
+name = "miette-derive"
+version = "7.6.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "db5b29714e950dbb20d5e6f74f9dcec4edbcc1067bb7f8ed198c097b8c1a818b"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn 2.0.117",
+]
+
+[[package]]
+name = "minimal-lexical"
+version = "0.2.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "68354c5c6bd36d73ff3feceb05efa59b6acb7626617f4962be322a825e61f79a"
+
+[[package]]
+name = "miniz_oxide"
+version = "0.8.9"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1fa76a2c86f704bdb222d66965fb3d63269ce38518b83cb0575fca855ebb6316"
+dependencies = [
+ "adler2",
+ "simd-adler32",
+]
+
+[[package]]
+name = "nom"
+version = "7.1.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d273983c5a657a70a3e8f2a01329822f3b8c8172b73826411a55751e404a0a4a"
+dependencies = [
+ "memchr",
+ "minimal-lexical",
+]
+
+[[package]]
+name = "nom-supreme"
+version = "0.8.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2bd3ae6c901f1959588759ff51c95d24b491ecb9ff91aa9c2ef4acc5b1dcab27"
+dependencies = [
+ "brownstone",
+ "indent_write",
+ "joinery",
+ "memchr",
+ "nom",
+]
 
 [[package]]
-name = "itoa"
-version = "1.0.18"
+name = "nu-ansi-term"
+version = "0.50.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "8f42a60cbdf9a97f5d2305f08a87dc4e09308d1276d28c869c684d7777685682"
+checksum = "7957b9740744892f114936ab4a57b3f487491bbeafaf8083688b16841a4240e5"
+dependencies = [
+ "windows-sys 0.61.2",
+]
 
 [[package]]
-name = "jiff"
-version = "0.2.27"
+name = "num"
+version = "0.4.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "392c70591e8749fe235ddaf513e6f58b26bce3dcc16524cecc8936f75afa161e"
+checksum = "35bd024e8b2ff75562e5f34e7f4905839deb4b22955ef5e73d2fea1b9813cb23"
 dependencies = [
- "jiff-static",
- "log",
- "portable-atomic",
- "portable-atomic-util",
- "serde_core",
+ "num-bigint",
+ "num-complex",
+ "num-integer",
+ "num-iter",
+ "num-rational",
+ "num-traits",
 ]
 
 [[package]]
-name = "jiff-static"
-version = "0.2.27"
+name = "num-bigint"
+version = "0.4.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "47b605b0c050d845fc355bb11eb3f9a8deddc218ea60c76e61aa1f2adfb2c96a"
+checksum = "a5e44f723f1133c9deac646763579fdb3ac745e418f2a7af9cd0c431da1f20b9"
 dependencies = [
- "proc-macro2",
- "quote",
- "syn",
+ "num-integer",
+ "num-traits",
 ]
 
 [[package]]
-name = "jobserver"
-version = "0.1.34"
+name = "num-complex"
+version = "0.4.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "9afb3de4395d6b3e67a780b6de64b51c978ecf11cb9a462c66be7d4ca9039d33"
+checksum = "73f88a1307638156682bada9d7604135552957b7818057dcef22705b4d509495"
 dependencies = [
- "getrandom 0.3.4",
- "libc",
+ "num-traits",
 ]
 
 [[package]]
-name = "leb128fmt"
-version = "0.1.0"
+name = "num-conv"
+version = "0.2.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "09edd9e8b54e49e587e4f6295a7d29c3ea94d469cb40ab8ca70b288248a81db2"
+checksum = "521739c6d2bac4aa25192232afe6841231376b2b26d4d9fae5ecf8ca5772e441"
 
 [[package]]
-name = "libc"
-version = "0.2.186"
+name = "num-integer"
+version = "0.1.46"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "68ab91017fe16c622486840e4c83c9a37afeff978bd239b5293d61ece587de66"
+checksum = "7969661fd2958a5cb096e56c8e1ad0444ac2bbcd0061bd28660485a44879858f"
+dependencies = [
+ "num-traits",
+]
 
 [[package]]
-name = "libredox"
-version = "0.1.17"
+name = "num-iter"
+version = "0.1.45"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "f02ab6bace2054fb888a3c16f990117b579d14a3088e472d63c6011fa185c9d3"
+checksum = "1429034a0490724d0075ebb2bc9e875d6503c3cf69e235a8941aa757d83ef5bf"
 dependencies = [
- "libc",
+ "autocfg",
+ "num-integer",
+ "num-traits",
 ]
 
 [[package]]
-name = "linux-raw-sys"
-version = "0.12.1"
+name = "num-rational"
+version = "0.4.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "32a66949e030da00e8c7d4434b251670a91556f4144941d37452769c25d58a53"
+checksum = "f83d14da390562dca69fc84082e73e548e1ad308d24accdedd2720017cb37824"
+dependencies = [
+ "num-bigint",
+ "num-integer",
+ "num-traits",
+]
 
 [[package]]
-name = "log"
-version = "0.4.30"
+name = "num-traits"
+version = "0.2.19"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "616ec5685824bcc94416c6d4a7a446eea774a31efd7062c8480ba6fd06d7a6e5"
+checksum = "071dfc062690e90b734c0b2273ce72ad0ffa95f0c74596bc250dcfd960262841"
+dependencies = [
+ "autocfg",
+]
 
 [[package]]
-name = "memchr"
-version = "2.8.1"
+name = "num_threads"
+version = "0.1.7"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "6b947ae49db0d222b1dbc6b113ce7248a3fc3a6ca21b696717bfc000ba4484d8"
+checksum = "5c7398b9c8b70908f6371f47ed36737907c87c52af34c268fed0bf0ceb92ead9"
+dependencies = [
+ "libc",
+]
 
 [[package]]
-name = "miniz_oxide"
-version = "0.8.9"
+name = "object"
+version = "0.37.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "1fa76a2c86f704bdb222d66965fb3d63269ce38518b83cb0575fca855ebb6316"
+checksum = "ff76201f031d8863c38aa7f905eca4f53abbfa15f609db4277d44cd8938f33fe"
 dependencies = [
- "adler2",
- "simd-adler32",
+ "memchr",
 ]
 
 [[package]]
@@ -550,12 +1384,59 @@ version = "0.2.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "04744f49eae99ab78e0d5c0b603ab218f515ea8cfe5a456d7629ad883a3b6e7d"
 
+[[package]]
+name = "owo-colors"
+version = "4.3.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d211803b9b6b570f68772237e415a029d5a50c65d382910b879fb19d3271f94d"
+
+[[package]]
+name = "parking_lot"
+version = "0.12.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "93857453250e3077bd71ff98b6a65ea6621a19bb0f559a85248955ac12c45a1a"
+dependencies = [
+ "lock_api",
+ "parking_lot_core",
+]
+
+[[package]]
+name = "parking_lot_core"
+version = "0.9.12"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2621685985a2ebf1c516881c026032ac7deafcda1a2c9b7850dc81e3dfcb64c1"
+dependencies = [
+ "cfg-if",
+ "libc",
+ "redox_syscall",
+ "smallvec",
+ "windows-link",
+]
+
+[[package]]
+name = "paste"
+version = "1.0.15"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "57c0d7b74b563b49d38dae00a0c37d4d6de9b432382b2892f0574ddcae73fd0a"
+
 [[package]]
 name = "percent-encoding"
 version = "2.3.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "9b4f627cb1b25917193a259e49bdad08f671f8d9708acfd5fe0a8c1455d87220"
 
+[[package]]
+name = "petgraph"
+version = "0.8.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8701b58ea97060d5e5b155d383a69952a60943f0e6dfe30b04c287beb0b27455"
+dependencies = [
+ "fixedbitset",
+ "hashbrown 0.15.5",
+ "indexmap",
+ "serde",
+]
+
 [[package]]
 name = "phf"
 version = "0.13.1"
@@ -587,7 +1468,7 @@ dependencies = [
  "phf_shared",
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.117",
 ]
 
 [[package]]
@@ -599,6 +1480,12 @@ dependencies = [
  "siphasher",
 ]
 
+[[package]]
+name = "pin-project-lite"
+version = "0.2.17"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "a89322df9ebe1c1578d689c92318e070967d1042b512afbe49518723f4e6d5cd"
+
 [[package]]
 name = "pkg-config"
 version = "0.3.33"
@@ -620,6 +1507,52 @@ dependencies = [
  "portable-atomic",
 ]
 
+[[package]]
+name = "postcard"
+version = "1.1.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6764c3b5dd454e283a30e6dfe78e9b31096d9e32036b5d1eaac7a6119ccb9a24"
+dependencies = [
+ "cobs",
+ "embedded-io 0.4.0",
+ "embedded-io 0.6.1",
+ "heapless",
+ "serde",
+]
+
+[[package]]
+name = "powerfmt"
+version = "0.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "439ee305def115ba05938db6eb1644ff94165c5ab5e9420d1c1bcedbba909391"
+
+[[package]]
+name = "predicates"
+version = "3.1.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ada8f2932f28a27ee7b70dd6c1c39ea0675c55a36879ab92f3a715eaa1e63cfe"
+dependencies = [
+ "anstyle",
+ "difflib",
+ "predicates-core",
+]
+
+[[package]]
+name = "predicates-core"
+version = "1.0.10"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "cad38746f3166b4031b1a0d39ad9f954dd291e7854fcc0eed52ee41a0b50d144"
+
+[[package]]
+name = "predicates-tree"
+version = "1.0.13"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d0de1b847b39c8131db0467e9df1ff60e6d0562ab8e9a16e568ad0fdb372e2f2"
+dependencies = [
+ "predicates-core",
+ "termtree",
+]
+
 [[package]]
 name = "prettyplease"
 version = "0.2.37"
@@ -627,7 +1560,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "479ca8adacdd7ce8f1fb39ce9ecccbfe93a3f1344b3d0d97f20bc0196208f62b"
 dependencies = [
  "proc-macro2",
- "syn",
+ "syn 2.0.117",
 ]
 
 [[package]]
@@ -639,6 +1572,16 @@ dependencies = [
  "unicode-ident",
 ]
 
+[[package]]
+name = "psm"
+version = "0.1.31"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "645dbe486e346d9b5de3ef16ede18c26e6c70ad97418f4874b8b1889d6e761ea"
+dependencies = [
+ "ar_archive_writer",
+ "cc",
+]
+
 [[package]]
 name = "quote"
 version = "1.0.45"
@@ -660,6 +1603,35 @@ version = "6.0.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "f8dcc9c7d52a811697d2151c701e0d08956f92b0e24136cf4cf27b57a6a0d9bf"
 
+[[package]]
+name = "rayon"
+version = "1.12.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "fb39b166781f92d482534ef4b4b1b2568f42613b53e5b6c160e24cfbfa30926d"
+dependencies = [
+ "either",
+ "rayon-core",
+]
+
+[[package]]
+name = "rayon-core"
+version = "1.13.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "22e18b0f0062d30d4230b2e85ff77fdfe4326feb054b9783a3460d8435c8ab91"
+dependencies = [
+ "crossbeam-deque",
+ "crossbeam-utils",
+]
+
+[[package]]
+name = "redox_syscall"
+version = "0.5.18"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ed2bf2547551a7053d6fdfafda3f938979645c44812fbfcda098faae3f1a362d"
+dependencies = [
+ "bitflags",
+]
+
 [[package]]
 name = "redox_users"
 version = "0.5.2"
@@ -714,6 +1686,27 @@ dependencies = [
  "windows-sys 0.52.0",
 ]
 
+[[package]]
+name = "rustc-demangle"
+version = "0.1.27"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b50b8869d9fc858ce7266cce0194bd74df58b9d0e3f6df3a9fc8eb470d95c09d"
+
+[[package]]
+name = "rustc-hash"
+version = "2.1.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "94300abf3f1ae2e2b8ffb7b58043de3d399c73fa6f4b73826402a5c457614dbe"
+
+[[package]]
+name = "rustc_version"
+version = "0.4.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "cfcb3a22ef46e85b45de6ee7e79d063319ebb6594faafcf1c225ea92ab6e9b92"
+dependencies = [
+ "semver",
+]
+
 [[package]]
 name = "rustix"
 version = "1.1.4"
@@ -762,11 +1755,36 @@ dependencies = [
  "untrusted",
 ]
 
+[[package]]
+name = "rustversion"
+version = "1.0.22"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b39cdef0fa800fc44525c84ccb54a029961a8215f9619753635a9c0d2538d46d"
+
+[[package]]
+name = "same-file"
+version = "1.0.6"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "93fc1dc3aaa9bfed95e02e6eadabb4baf7e3078b0bd1b4d7b6b0b68378900502"
+dependencies = [
+ "winapi-util",
+]
+
+[[package]]
+name = "scopeguard"
+version = "1.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "94143f37725109f92c262ed2cf5e59bce7498c01bcc1502d7b9afe439a4e9f49"
+
 [[package]]
 name = "semver"
 version = "1.0.28"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "8a7852d02fc848982e0c167ef163aaff9cd91dc640ba85e263cb1ce46fae51cd"
+dependencies = [
+ "serde",
+ "serde_core",
+]
 
 [[package]]
 name = "serde"
@@ -775,6 +1793,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "9a8e94ea7f378bd32cbbd37198a4a91436180c5bb472411e48b5ec2e2124ae9e"
 dependencies = [
  "serde_core",
+ "serde_derive",
 ]
 
 [[package]]
@@ -794,7 +1813,7 @@ checksum = "d540f220d3187173da220f885ab66608367b6574e925011a9353e4badda91d79"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.117",
 ]
 
 [[package]]
@@ -810,6 +1829,15 @@ dependencies = [
  "zmij",
 ]
 
+[[package]]
+name = "serde_spanned"
+version = "0.6.9"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "bf41e0cfaf7226dca15e8197172c295a782857fcb97fad1808a166870dee75a3"
+dependencies = [
+ "serde",
+]
+
 [[package]]
 name = "serde_spanned"
 version = "1.1.1"
@@ -819,52 +1847,172 @@ dependencies = [
  "serde_core",
 ]
 
+[[package]]
+name = "serde_stacker"
+version = "0.1.14"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d4936375d50c4be7eff22293a9344f8e46f323ed2b3c243e52f89138d9bb0f4a"
+dependencies = [
+ "serde",
+ "serde_core",
+ "stacker",
+]
+
+[[package]]
+name = "serde_state"
+version = "1.0.0"
+source = "git+https://github.com/Nadrieril/serde_state?branch=main#9bffbc1b28fd93533bbd3ca835385f29cb51888f"
+dependencies = [
+ "serde",
+ "serde_state_derive",
+]
+
+[[package]]
+name = "serde_state_derive"
+version = "1.0.0"
+source = "git+https://github.com/Nadrieril/serde_state?branch=main#9bffbc1b28fd93533bbd3ca835385f29cb51888f"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn 2.0.117",
+]
+
 [[package]]
 name = "sha2"
 version = "0.10.9"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "a7507d819769d01a365ab707794a4084392c824f54a7a6a7862f8c3d0892b283"
+checksum = "a7507d819769d01a365ab707794a4084392c824f54a7a6a7862f8c3d0892b283"
+dependencies = [
+ "cfg-if",
+ "cpufeatures",
+ "digest",
+]
+
+[[package]]
+name = "sha2-const"
+version = "0.1.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "dbb83f144cbda94be5d2278400eee9e0a03eb68b5504349943655b7b1603c4af"
+
+[[package]]
+name = "sharded-slab"
+version = "0.1.7"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f40ca3c46823713e0d4209592e8d6e826aa57e928f09752619fc696c499637f6"
+dependencies = [
+ "lazy_static",
+]
+
+[[package]]
+name = "shlex"
+version = "2.0.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f8fadd59c855ef2080decdef8ff161eb6661b86933c9d82e5ba29dc602a55aba"
+
+[[package]]
+name = "simd-adler32"
+version = "0.3.9"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "703d5c7ef118737c72f1af64ad2f6f8c5e1921f818cdcb97b8fe6fc69bf66214"
+
+[[package]]
+name = "siphasher"
+version = "1.0.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8ee5873ec9cce0195efcb7a4e9507a04cd49aec9c83d0389df45b1ef7ba2e649"
+
+[[package]]
+name = "slab"
+version = "0.4.12"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0c790de23124f9ab44544d7ac05d60440adc586479ce501c1d6d7da3cd8c9cf5"
+
+[[package]]
+name = "smallvec"
+version = "1.15.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "67b1b7a3b5fe4f1376887184045fcf45c69e92af734b7aaddc05fb777b6fbd03"
+
+[[package]]
+name = "spin"
+version = "0.9.8"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6980e8d7511241f8acf4aebddbb1ff938df5eebe98691418c4468d0b72a96a67"
+dependencies = [
+ "lock_api",
+]
+
+[[package]]
+name = "stable_deref_trait"
+version = "1.2.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "6ce2be8dc25455e1f91df71bfa12ad37d7af1092ae736f3a6cd0e37bc7810596"
+
+[[package]]
+name = "stacker"
+version = "0.1.24"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "640c8cdd92b6b12f5bcb1803ca3bbf5ab96e5e6b6b96b9ab77dabe9e880b3190"
+dependencies = [
+ "cc",
+ "cfg-if",
+ "libc",
+ "psm",
+ "windows-sys 0.61.2",
+]
+
+[[package]]
+name = "strip-ansi-escapes"
+version = "0.2.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2a8f8038e7e7969abb3f1b7c2a811225e9296da208539e0f79c5251d6cac0025"
 dependencies = [
- "cfg-if",
- "cpufeatures",
- "digest",
+ "vte",
 ]
 
 [[package]]
-name = "sha2-const"
-version = "0.1.3"
+name = "strsim"
+version = "0.11.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "dbb83f144cbda94be5d2278400eee9e0a03eb68b5504349943655b7b1603c4af"
+checksum = "7da8b5736845d9f2fcb837ea5d9e2628564b3b043a70948a3f0b778838c5fb4f"
 
 [[package]]
-name = "shlex"
-version = "1.3.0"
+name = "subtle"
+version = "2.6.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "0fda2ff0d084019ba4d7c6f371c95d8fd75ce3524c3cb8fb653a3023f6323e64"
+checksum = "13c2bddecc57b384dee18652358fb23172facb8a2c51ccc10d74c157bdea3292"
 
 [[package]]
-name = "simd-adler32"
-version = "0.3.9"
+name = "supports-color"
+version = "3.0.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "703d5c7ef118737c72f1af64ad2f6f8c5e1921f818cdcb97b8fe6fc69bf66214"
+checksum = "c64fc7232dd8d2e4ac5ce4ef302b1d81e0b80d055b9d77c7c4f51f6aa4c867d6"
+dependencies = [
+ "is_ci",
+]
 
 [[package]]
-name = "siphasher"
-version = "1.0.3"
+name = "supports-hyperlinks"
+version = "3.2.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "8ee5873ec9cce0195efcb7a4e9507a04cd49aec9c83d0389df45b1ef7ba2e649"
+checksum = "e396b6523b11ccb83120b115a0b7366de372751aa6edf19844dfb13a6af97e91"
 
 [[package]]
-name = "strsim"
-version = "0.11.1"
+name = "supports-unicode"
+version = "3.0.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "7da8b5736845d9f2fcb837ea5d9e2628564b3b043a70948a3f0b778838c5fb4f"
+checksum = "b7401a30af6cb5818bb64852270bb722533397edcfc7344954a38f420819ece2"
 
 [[package]]
-name = "subtle"
-version = "2.6.1"
+name = "syn"
+version = "1.0.109"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "13c2bddecc57b384dee18652358fb23172facb8a2c51ccc10d74c157bdea3292"
+checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "unicode-ident",
+]
 
 [[package]]
 name = "syn"
@@ -877,6 +2025,12 @@ dependencies = [
  "unicode-ident",
 ]
 
+[[package]]
+name = "take_mut"
+version = "0.2.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f764005d11ee5f36500a149ace24e00e3da98b0158b3e2d53a7495660d3f4d60"
+
 [[package]]
 name = "tar"
 version = "0.4.46"
@@ -901,6 +2055,32 @@ dependencies = [
  "windows-sys 0.61.2",
 ]
 
+[[package]]
+name = "terminal_size"
+version = "0.4.4"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "230a1b821ccbd75b185820a1f1ff7b14d21da1e442e22c0863ea5f08771a8874"
+dependencies = [
+ "rustix",
+ "windows-sys 0.61.2",
+]
+
+[[package]]
+name = "termtree"
+version = "0.5.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "8f50febec83f5ee1df3015341d8bd429f2d1cc62bcba7ea2076759d315084683"
+
+[[package]]
+name = "textwrap"
+version = "0.16.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c13547615a44dc9c452a8a534638acdf07120d4b6847c8178705da06306a3057"
+dependencies = [
+ "unicode-linebreak",
+ "unicode-width 0.2.2",
+]
+
 [[package]]
 name = "thiserror"
 version = "2.0.18"
@@ -918,7 +2098,61 @@ checksum = "ebc4ee7f67670e9b64d05fa4253e753e016c6c95ff35b89b7941d6b856dec1d5"
 dependencies = [
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.117",
+]
+
+[[package]]
+name = "thread_local"
+version = "1.1.9"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "f60246a4944f24f6e018aa17cdeffb7818b76356965d03b07d6a9886e8962185"
+dependencies = [
+ "cfg-if",
+]
+
+[[package]]
+name = "time"
+version = "0.3.47"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "743bd48c283afc0388f9b8827b976905fb217ad9e647fae3a379a9283c4def2c"
+dependencies = [
+ "deranged",
+ "itoa",
+ "libc",
+ "num-conv",
+ "num_threads",
+ "powerfmt",
+ "serde_core",
+ "time-core",
+ "time-macros",
+]
+
+[[package]]
+name = "time-core"
+version = "0.1.8"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7694e1cfe791f8d31026952abf09c69ca6f6fa4e1a1229e18988f06a04a12dca"
+
+[[package]]
+name = "time-macros"
+version = "0.2.27"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "2e70e4c5a0e0a8a4823ad65dfe1a6930e4f4d756dcd9dd7939022b5e8c501215"
+dependencies = [
+ "num-conv",
+ "time-core",
+]
+
+[[package]]
+name = "toml"
+version = "0.8.23"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "dc1beb996b9d83529a9e75c17a1686767d148d70663143c7854d8b4a09ced362"
+dependencies = [
+ "serde",
+ "serde_spanned 0.6.9",
+ "toml_datetime 0.6.11",
+ "toml_edit",
 ]
 
 [[package]]
@@ -929,8 +2163,8 @@ checksum = "cf92845e79fc2e2def6a5d828f0801e29a2f8acc037becc5ab08595c7d5e9863"
 dependencies = [
  "indexmap",
  "serde_core",
- "serde_spanned",
- "toml_datetime",
+ "serde_spanned 1.1.1",
+ "toml_datetime 0.7.5+spec-1.1.0",
  "toml_parser",
  "toml_writer",
  "winnow 0.7.15",
@@ -943,7 +2177,7 @@ source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "389864cf501669b741746e9bc35e66c67f2b80266482ad04c452e2410433f205"
 dependencies = [
  "phf",
- "toml",
+ "toml 0.9.12+spec-1.1.0",
  "toml_const_macros",
 ]
 
@@ -956,8 +2190,17 @@ dependencies = [
  "indexmap",
  "proc-macro2",
  "quote",
- "syn",
- "toml",
+ "syn 2.0.117",
+ "toml 0.9.12+spec-1.1.0",
+]
+
+[[package]]
+name = "toml_datetime"
+version = "0.6.11"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "22cddaf88f4fbc13c51aebbf5f8eceb5c7c5a9da2ac40a13519eb5b0a0e8f11c"
+dependencies = [
+ "serde",
 ]
 
 [[package]]
@@ -969,6 +2212,20 @@ dependencies = [
  "serde_core",
 ]
 
+[[package]]
+name = "toml_edit"
+version = "0.22.27"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "41fe8c660ae4257887cf66394862d21dbca4a6ddd26f04a3560410406a2f819a"
+dependencies = [
+ "indexmap",
+ "serde",
+ "serde_spanned 0.6.9",
+ "toml_datetime 0.6.11",
+ "toml_write",
+ "winnow 0.7.15",
+]
+
 [[package]]
 name = "toml_parser"
 version = "1.1.2+spec-1.1.0"
@@ -978,17 +2235,96 @@ dependencies = [
  "winnow 1.0.3",
 ]
 
+[[package]]
+name = "toml_write"
+version = "0.1.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5d99f8c9a7727884afe522e9bd5edbfc91a3312b36a77b5fb8926e4c31a41801"
+
 [[package]]
 name = "toml_writer"
 version = "1.1.1+spec-1.1.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "756daf9b1013ebe47a8776667b466417e2d4c5679d441c26230efd9ef78692db"
 
+[[package]]
+name = "tracing"
+version = "0.1.44"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "63e71662fa4b2a2c3a26f570f037eb95bb1f85397f3cd8076caed2f026a6d100"
+dependencies = [
+ "pin-project-lite",
+ "tracing-attributes",
+ "tracing-core",
+]
+
+[[package]]
+name = "tracing-attributes"
+version = "0.1.31"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7490cfa5ec963746568740651ac6781f701c9c5ea257c58e057f3ba8cf69e8da"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn 2.0.117",
+]
+
+[[package]]
+name = "tracing-core"
+version = "0.1.36"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "db97caf9d906fbde555dd62fa95ddba9eecfd14cb388e4f491a66d74cd5fb79a"
+dependencies = [
+ "once_cell",
+ "valuable",
+]
+
+[[package]]
+name = "tracing-log"
+version = "0.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ee855f1f400bd0e5c02d150ae5de3840039a3f54b025156404e34c23c03f47c3"
+dependencies = [
+ "log",
+ "once_cell",
+ "tracing-core",
+]
+
+[[package]]
+name = "tracing-subscriber"
+version = "0.3.23"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "cb7f578e5945fb242538965c2d0b04418d38ec25c79d160cd279bf0731c8d319"
+dependencies = [
+ "matchers",
+ "nu-ansi-term",
+ "once_cell",
+ "regex-automata",
+ "sharded-slab",
+ "smallvec",
+ "thread_local",
+ "tracing",
+ "tracing-core",
+ "tracing-log",
+]
+
+[[package]]
+name = "tracing-tree"
+version = "0.4.0"
+source = "git+https://github.com/Nadrieril/tracing-tree#841286bfffd3c2200810244506cd127013dbeff9"
+dependencies = [
+ "nu-ansi-term",
+ "time",
+ "tracing-core",
+ "tracing-log",
+ "tracing-subscriber",
+]
+
 [[package]]
 name = "typenum"
-version = "1.20.0"
+version = "1.20.1"
 source = "registry+https://github.com/rust-lang/crates.io-index"
-checksum = "40ce102ab67701b8526c123c1bab5cbe42d7040ccfd0f64af1a385808d2f43de"
+checksum = "b6f5e870be6c3b371b77fe0ee0bafb859fa4964b4404c27de1d380043c4dda20"
 
 [[package]]
 name = "unicode-ident"
@@ -996,12 +2332,42 @@ version = "1.0.24"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75"
 
+[[package]]
+name = "unicode-linebreak"
+version = "0.1.5"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3b09c83c3c29d37506a3e260c08c03743a6bb66a9cd432c6934ab501a190571f"
+
+[[package]]
+name = "unicode-segmentation"
+version = "1.13.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c6f5d3c3b1bf09027a88a6bc961fc00497d651009560b5463668dc81b0fa87a8"
+
+[[package]]
+name = "unicode-width"
+version = "0.1.14"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "7dd6e30e90baa6f72411720665d41d89b9a3d039dc45b8faea1ddd07f617f6af"
+
+[[package]]
+name = "unicode-width"
+version = "0.2.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b4ac048d71ede7ee76d585517add45da530660ef4390e49b098733c6e897f254"
+
 [[package]]
 name = "unicode-xid"
 version = "0.2.6"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "ebc1c04c71510c7f702b52b7c350734c9ff1295c464a03335b00bb84fc54f853"
 
+[[package]]
+name = "unit-prefix"
+version = "0.5.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "81e544489bf3d8ef66c953931f56617f423cd4b5494be343d9b9d3dda037b9a3"
+
 [[package]]
 name = "untrusted"
 version = "0.9.0"
@@ -1037,6 +2403,19 @@ dependencies = [
  "log",
 ]
 
+[[package]]
+name = "ustr"
+version = "1.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "18b19e258aa08450f93369cf56dd78063586adf19e92a75b338a800f799a0208"
+dependencies = [
+ "ahash",
+ "byteorder",
+ "lazy_static",
+ "parking_lot",
+ "serde",
+]
+
 [[package]]
 name = "utf8-zero"
 version = "0.8.1"
@@ -1049,12 +2428,46 @@ version = "0.2.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "06abde3611657adf66d383f00b093d7faecc7fa57071cce2578660c9f1010821"
 
+[[package]]
+name = "valuable"
+version = "0.1.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ba73ea9cf16a25df0c8caa16c51acb937d5712a8429db78a3ee29d5dcacd3a65"
+
 [[package]]
 name = "version_check"
 version = "0.9.5"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a"
 
+[[package]]
+name = "vte"
+version = "0.14.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "231fdcd7ef3037e8330d8e17e61011a2c244126acc0a982f4040ac3f9f0bc077"
+dependencies = [
+ "memchr",
+]
+
+[[package]]
+name = "wait-timeout"
+version = "0.2.1"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "09ac3b126d3914f9849036f826e054cbabdc8519970b8998ddaf3b5bd3c65f11"
+dependencies = [
+ "libc",
+]
+
+[[package]]
+name = "walkdir"
+version = "2.5.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "29790946404f91d9c5d06f9874efddea1dc06c5efe94541a7d6863108e3a5e4b"
+dependencies = [
+ "same-file",
+ "winapi-util",
+]
+
 [[package]]
 name = "wasi"
 version = "0.11.1+wasi-snapshot-preview1"
@@ -1079,6 +2492,51 @@ dependencies = [
  "wit-bindgen 0.51.0",
 ]
 
+[[package]]
+name = "wasm-bindgen"
+version = "0.2.122"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3ed04576f974d2b2fba0f38c51dbc5518011e38c36bf1143164be765528fd409"
+dependencies = [
+ "cfg-if",
+ "once_cell",
+ "rustversion",
+ "wasm-bindgen-macro",
+ "wasm-bindgen-shared",
+]
+
+[[package]]
+name = "wasm-bindgen-macro"
+version = "0.2.122"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "916151b09da36bd82f6615cbf3a419e2f0ba23a03c6160e8e92eb6bd4aa1dec6"
+dependencies = [
+ "quote",
+ "wasm-bindgen-macro-support",
+]
+
+[[package]]
+name = "wasm-bindgen-macro-support"
+version = "0.2.122"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "299047362ccbfce148b67ab7e73349f77748e00c8296f9542adfad2ad82c5c5e"
+dependencies = [
+ "bumpalo",
+ "proc-macro2",
+ "quote",
+ "syn 2.0.117",
+ "wasm-bindgen-shared",
+]
+
+[[package]]
+name = "wasm-bindgen-shared"
+version = "0.2.122"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9a929b2c61f11ba3e9bc35b50c1f25cb38e0e892c0c231ae2b8cf78d5dad4437"
+dependencies = [
+ "unicode-ident",
+]
+
 [[package]]
 name = "wasm-encoder"
 version = "0.244.0"
@@ -1113,6 +2571,16 @@ dependencies = [
  "semver",
 ]
 
+[[package]]
+name = "web-time"
+version = "1.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5a6580f308b1fad9207618087a65c04e7a10bc77e02c8e84e9b00dd4b12fa0bb"
+dependencies = [
+ "js-sys",
+ "wasm-bindgen",
+]
+
 [[package]]
 name = "webpki-roots"
 version = "1.0.7"
@@ -1122,6 +2590,18 @@ dependencies = [
  "rustls-pki-types",
 ]
 
+[[package]]
+name = "which"
+version = "7.0.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "24d643ce3fd3e5b54854602a080f34fb10ab75e0b813ee32d00ca2b44fa74762"
+dependencies = [
+ "either",
+ "env_home",
+ "rustix",
+ "winsafe",
+]
+
 [[package]]
 name = "winapi"
 version = "0.3.9"
@@ -1138,6 +2618,15 @@ version = "0.4.0"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "ac3b87c63620426dd9b991e5ce0329eff545bccbbb34f3be09ff6fb6ab51b7b6"
 
+[[package]]
+name = "winapi-util"
+version = "0.1.11"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "c2a7b1c03c876122aa43f3020e6c3c3ee5c05081c9a00739faf7503aeba10d22"
+dependencies = [
+ "windows-sys 0.61.2",
+]
+
 [[package]]
 name = "winapi-x86_64-pc-windows-gnu"
 version = "0.4.0"
@@ -1159,6 +2648,15 @@ dependencies = [
  "windows-targets",
 ]
 
+[[package]]
+name = "windows-sys"
+version = "0.59.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "1e38bc4d79ed67fd075bcc251a1c39b32a1776bbe92e5bef1f0bf1f8c531853b"
+dependencies = [
+ "windows-targets",
+]
+
 [[package]]
 name = "windows-sys"
 version = "0.61.2"
@@ -1237,6 +2735,9 @@ name = "winnow"
 version = "0.7.15"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "df79d97927682d2fd8adb29682d1140b343be4ac0f08fd68b7765d9c059d3945"
+dependencies = [
+ "memchr",
+]
 
 [[package]]
 name = "winnow"
@@ -1244,6 +2745,12 @@ version = "1.0.3"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "0592e1c9d151f854e6fd382574c3a0855250e1d9b2f99d9281c6e6391af352f1"
 
+[[package]]
+name = "winsafe"
+version = "0.0.19"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "d135d17ab770252ad95e9a872d365cf3090e3be864a34ab46f48555993efc904"
+
 [[package]]
 name = "wit-bindgen"
 version = "0.51.0"
@@ -1280,7 +2787,7 @@ dependencies = [
  "heck",
  "indexmap",
  "prettyplease",
- "syn",
+ "syn 2.0.117",
  "wasm-metadata",
  "wit-bindgen-core",
  "wit-component",
@@ -1296,7 +2803,7 @@ dependencies = [
  "prettyplease",
  "proc-macro2",
  "quote",
- "syn",
+ "syn 2.0.117",
  "wit-bindgen-core",
  "wit-bindgen-rust",
 ]
@@ -1348,6 +2855,26 @@ dependencies = [
  "rustix",
 ]
 
+[[package]]
+name = "zerocopy"
+version = "0.8.50"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3b065d4f0e55f82fae73202e189638116a87c55ab6b8e6c2721e13dd9d854ad1"
+dependencies = [
+ "zerocopy-derive",
+]
+
+[[package]]
+name = "zerocopy-derive"
+version = "0.8.50"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "0b631b19d36a892ab55420c92dbc83ccd79274f25be714855d3074aa71cab639"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn 2.0.117",
+]
+
 [[package]]
 name = "zeroize"
 version = "1.8.2"
diff --git a/anneal/v2/Cargo.toml b/anneal/v2/Cargo.toml
index 853b7f7f5c..47d8579834 100644
--- a/anneal/v2/Cargo.toml
+++ b/anneal/v2/Cargo.toml
@@ -4,6 +4,8 @@ members = ["."]
 [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"
@@ -48,5 +50,20 @@ url = "https://example.com/macos-aarch64.tar.zst"
 exocrate = { path = "../../exocrate" }
 toml_const = "1.3.0"
 clap = { version = "4.5", features = ["derive"] }
+clap-cargo = { version = "0.18.3", features = ["cargo_metadata"] }
 env_logger = "0.11"
 log = "0.4"
+anyhow = "1.0.102"
+cargo_metadata = "0.23.1"
+miette = { version = "7.6.0", features = ["derive", "fancy"] }
+thiserror = "2.0.18"
+serde_json = "1.0.149"
+serde = { version = "1.0.228", features = ["derive"] }
+indicatif = { version = "0.18.4", features = ["improved_unicode"] }
+fs2 = "0.4"
+walkdir = "2.5.0"
+sha2 = "0.10"
+tempfile = "3.27.0"
+rayon = "1.11.0"
+# `rev` is `main` branch HEAD on 2026-06-03.
+charon_lib = { package = "charon", git = "https://github.com/AeneasVerif/charon.git", rev = "0c91ca1a8e002d6bfa8d8f1f452804fce2f92cf1", default-features = false }
diff --git a/anneal/v2/examples/simple.rs b/anneal/v2/examples/simple.rs
new file mode 100644
index 0000000000..0b36b00521
--- /dev/null
+++ b/anneal/v2/examples/simple.rs
@@ -0,0 +1,7 @@
+pub fn add(left: usize, right: usize) -> usize {
+    left + right
+}
+
+fn main() {
+    println!("Hello, world! {}", add(1, 2));
+}
diff --git a/anneal/v2/src/charon.rs b/anneal/v2/src/charon.rs
new file mode 100644
index 0000000000..cabe823e11
--- /dev/null
+++ b/anneal/v2/src/charon.rs
@@ -0,0 +1,1055 @@
+// Copyright 2026 The Fuchsia Authors
+//
+// Licensed under the 2-Clause BSD License <LICENSE-BSD or
+// https://opensource.org/license/bsd-2-clause>, Apache License, Version 2.0
+// <LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+// license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
+// This file may not be copied, modified, or distributed except according to
+// those terms.
+
+//! 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 _;
+use rayon::prelude::{IntoParallelRefIterator as _, ParallelIterator as _};
+
+/// Runs Charon on the specified packages to generate LLBC artifacts.
+///
+/// This function requires [`crate::resolve::LockedRoots`] to ensure that it has exclusive access
+/// to the `llbc` output directory. It iterates over each [`crate::scanner::AnnealArtifact`],
+/// constructs the appropriate `charon` command, and executes it.
+///
+/// It handles:
+/// - **Opaque Functions**: identifying `unsafe(axiom)` functions and passing
+///   `--opaque` to Charon.
+/// - **Entry Points**: passing the computed `start_from` roots to Charon to
+///   minimize extraction scope.
+/// - **Output Handling**: capturing stdout/stderr, parsing JSON compiler
+///   messages, and rendering them using [`crate::diagnostics::DiagnosticMapper`].
+pub fn run_charon(
+    args: &crate::resolve::Args,
+    toolchain: &crate::setup::Toolchain,
+    roots: &crate::resolve::LockedRoots,
+    packages: &[crate::scanner::AnnealArtifact],
+    show_progress: bool,
+) -> anyhow::Result<()> {
+    let llbc_root = roots.llbc_root();
+    std::fs::create_dir_all(&llbc_root).context("Failed to create LLBC output directory")?;
+
+    // Prepend to `PATH` to ensure that when `charon` delegates to tools such as
+    // `cargo` and `rustc` it invokes the correct rust toolchain.
+    let new_path = crate::util::prepend_to_env_var("PATH", &toolchain.rust_bin());
+
+    let lib_env_var =
+        if cfg!(target_os = "macos") { "DYLD_LIBRARY_PATH" } else { "LD_LIBRARY_PATH" };
+    // Set `LD_LIBRARY_PATH` (or `DYLD_LIBRARY_PATH` on macOS) to point to the
+    // managed Rust toolchain's `lib` directory so that dynamic executables (like
+    // `charon-driver` which links against `rustc` dynamic libraries) can find them.
+    let new_lib_path = crate::util::prepend_to_env_var(lib_env_var, &toolchain.rust_lib());
+
+    // Global print mutex to prevent interleaved printing of consolidated artifact buffers.
+    let print_mutex = std::sync::Arc::new(std::sync::Mutex::new(()));
+
+    // Initialize MultiProgress if progress is enabled.
+    let mp = if show_progress {
+        Some(std::sync::Arc::new(indicatif::MultiProgress::new()))
+    } else {
+        None
+    };
+
+    packages.par_iter().try_for_each(|artifact| {
+        let pb = mp.as_ref().map(|m| {
+            let pb = m.add(indicatif::ProgressBar::new_spinner());
+            pb.set_style(
+                indicatif::ProgressStyle::default_spinner()
+                    .template("{spinner:.green} {msg}")
+                    .unwrap(),
+            );
+            pb.set_message("Compiling...");
+            pb
+        });
+
+        log::info!("Invoking Charon on package '{}'...", artifact.name.package_name);
+
+        let mut cmd = toolchain.command(crate::setup::Tool::Charon);
+
+        // 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);
+
+        // 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");
+
+        let llbc_path = artifact.llbc_path(roots);
+        cmd.arg("--dest-file").arg(llbc_path);
+
+        // Fail fast on errors: 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");
+
+        // Separator for the underlying cargo command.
+        cmd.arg("--");
+
+        // Ensure cargo emits json msgs which charon-driver natively generates.
+        cmd.arg("--message-format=json");
+
+        cmd.arg("--manifest-path").arg(&artifact.manifest_path);
+
+        use crate::resolve::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]),
+        };
+
+        // Forward all feature-related flags.
+        if args.features.all_features {
+            cmd.arg("--all-features");
+        }
+        if args.features.no_default_features {
+            cmd.arg("--no-default-features");
+        }
+        for feature in &args.features.features {
+            cmd.arg("--features").arg(feature);
+        }
+
+        // Reuse the main target directory for dependencies to save time: share
+        // `CARGO_TARGET_DIR` (`target/anneal/cargo_target`) across all Charon
+        // invocations to enable Cargo's incremental build cache.
+        cmd.env("CARGO_TARGET_DIR", roots.cargo_target_dir());
+
+        log::debug!("Executing charon command: {:?}", cmd);
+
+        let start = std::time::Instant::now();
+        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
+        // 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 safety_buffer = std::sync::Arc::new(std::sync::Mutex::new(Vec::new()));
+        let safety_buffer_clone = std::sync::Arc::clone(&safety_buffer);
+
+        // Local buffer to collect all output (diagnostics) for this artifact.
+        let artifact_diagnostics = std::sync::Arc::new(std::sync::Mutex::new(Vec::new()));
+        let artifact_diagnostics_clone = std::sync::Arc::clone(&artifact_diagnostics);
+
+        let mut mapper = crate::diagnostics::DiagnosticMapper::new(roots.workspace().clone());
+
+        let pb_clone = pb.clone();
+        let res = crate::util::run_command_with_progress(cmd, pb_clone, move |line, pb| {
+            if let Ok(msg) = serde_json::from_str::<cargo_metadata::Message>(line) {
+                match msg {
+                    cargo_metadata::Message::CompilerArtifact(a) => {
+                        if let Some(p) = pb {
+                            p.set_message(format!("Compiling {}", a.target.name));
+                        }
+                    }
+                    cargo_metadata::Message::CompilerMessage(msg) => {
+                        let mut rendered = String::new();
+                        mapper.render_miette(&msg.message, |s| rendered.push_str(&s));
+                        if !rendered.is_empty() {
+                            artifact_diagnostics_clone.lock().unwrap().push(rendered);
+                        }
+                        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);
+                        }
+                    }
+                    cargo_metadata::Message::TextLine(t) => {
+                        safety_buffer_clone.lock().unwrap().push(t);
+                    }
+                    _ => {}
+                }
+            } else {
+                safety_buffer_clone.lock().unwrap().push(line.to_string());
+            }
+            Ok(())
+        })?;
+
+        log::trace!("Charon for '{}' took {:.2?}", artifact.name.package_name, start.elapsed());
+
+        // Lock the print mutex to print this artifact's consolidated output atomically.
+        let _lock = print_mutex.lock().unwrap();
+
+        // Print all collected diagnostics for this artifact.
+        let diags = artifact_diagnostics.lock().unwrap();
+        if !diags.is_empty() {
+            eprintln!("=== Diagnostics for '{}' ===", artifact.name.package_name);
+            for diag in diags.iter() {
+                eprintln!("{}", diag);
+            }
+        }
+
+        if output_error.load(std::sync::atomic::Ordering::Relaxed) {
+            anyhow::bail!("Diagnostic error in charon");
+        } else if !res.status.success() {
+            // Print safety buffer on failure (also atomically since we hold print_mutex).
+            eprintln!("=== Failure output for '{}' ===", artifact.name.package_name);
+            for line in safety_buffer.lock().unwrap().iter() {
+                eprintln!("{}", line);
+            }
+            // 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);
+        }
+
+        Ok(())
+    })?;
+
+    Ok(())
+}
+
+#[cfg(test)]
+mod tests {
+    #[cfg(feature = "exocrate_tests")]
+    use std::fs;
+
+    #[cfg(feature = "exocrate_tests")]
+    use clap::Parser as _;
+
+    #[cfg(feature = "exocrate_tests")]
+    use super::*;
+    #[cfg(feature = "exocrate_tests")]
+    use crate::resolve::{Args, resolve_roots};
+    #[cfg(feature = "exocrate_tests")]
+    use crate::scanner::{ScanMode, scan_workspace};
+
+    // Shared helper to parse LLBC output and verify local status and compiled body variant.
+    #[cfg(feature = "exocrate_tests")]
+    fn assert_fn_body(
+        path: &std::path::Path,
+        components: &[&str],
+        expected_local: bool,
+        expected_structured: bool,
+    ) {
+        let file = std::fs::File::open(path).unwrap();
+        let crate_data: charon_lib::export::CrateData = serde_json::from_reader(file).unwrap();
+
+        let fun = crate_data
+            .translated
+            .fun_decls
+            .iter()
+            .find(|fun| {
+                let name = &fun.item_meta.name;
+                if name.name.len() != components.len() {
+                    return false;
+                }
+                for (i, elem) in name.name.iter().enumerate() {
+                    match elem {
+                        charon_lib::ast::PathElem::Ident(ident, _) => {
+                            if ident != components[i] {
+                                return false;
+                            }
+                        }
+                        _ => return false,
+                    }
+                }
+                true
+            })
+            .unwrap_or_else(|| {
+                panic!("Function with name path {:?} was not found/declared in LLBC!", components)
+            });
+
+        assert_eq!(
+            fun.item_meta.is_local, expected_local,
+            "Local/External status mismatch for function {:?}",
+            components
+        );
+
+        if expected_structured {
+            assert!(
+                matches!(fun.body, charon_lib::ast::Body::Structured(_)),
+                "Function {:?} was expected to contain a compiled structured implementation body!",
+                components
+            );
+        } else {
+            assert!(
+                matches!(fun.body, charon_lib::ast::Body::Opaque),
+                "Function {:?} was expected to be Opaque (referred to but implementation body NOT included)!",
+                components
+            );
+        }
+    }
+
+    #[cfg(feature = "exocrate_tests")]
+    fn resolve_test_toolchain() -> &'static crate::setup::Toolchain {
+        static TOOLCHAIN: std::sync::OnceLock<crate::setup::Toolchain> = std::sync::OnceLock::new();
+        TOOLCHAIN.get_or_init(|| {
+            crate::setup::run_setup(crate::setup::SetupArgs {
+                local_archive: Some("target/anneal-exocrate.tar.zst".into()),
+            })
+            .expect("Failed to run setup");
+            crate::setup::Toolchain::resolve().expect("Failed to resolve toolchain")
+        })
+    }
+
+    #[cfg(feature = "exocrate_tests")]
+    fn write_log_path_dependency_fixture(temp_dir: &tempfile::TempDir) {
+        let log_dir = temp_dir.path().join("vendor").join("log");
+        std::fs::create_dir_all(log_dir.join("src")).unwrap();
+        std::fs::write(
+            log_dir.join("Cargo.toml"),
+            r#"
+[package]
+name = "log"
+version = "0.4.28"
+edition = "2021"
+
+[lib]
+path = "src/lib.rs"
+
+[workspace]
+"#,
+        )
+        .unwrap();
+        std::fs::write(
+            log_dir.join("src/lib.rs"),
+            r#"
+#[macro_export]
+macro_rules! info {
+    ($fmt:literal $(, $arg:expr)* $(,)?) => {{
+        $(let _ = &$arg;)*
+    }};
+    ($($arg:tt)*) => {{}};
+}
+
+pub fn max_level() -> usize {
+    0
+}
+"#,
+        )
+        .unwrap();
+    }
+
+    #[cfg(feature = "exocrate_tests")]
+    #[test]
+    fn test_run_charon_simple() {
+        // 1. Create a temporary directory.
+        let temp_dir = tempfile::tempdir().unwrap();
+        let proj_dir = temp_dir.path().join("test_proj");
+        fs::create_dir_all(&proj_dir).unwrap();
+
+        // 2. Create a simple Cargo.toml.
+        let cargo_toml = r#"
+            [package]
+            name = "test_proj"
+            version = "0.1.0"
+            edition = "2021"
+
+            [lib]
+            path = "src/lib.rs"
+        "#;
+        fs::write(proj_dir.join("Cargo.toml"), cargo_toml).unwrap();
+
+        // 3. Create a simple src/lib.rs.
+        fs::create_dir_all(proj_dir.join("src")).unwrap();
+        let lib_rs = r#"
+            pub fn add(left: usize, right: usize) -> usize {
+                left + right
+            }
+        "#;
+        fs::write(proj_dir.join("src").join("lib.rs"), lib_rs).unwrap();
+
+        // 4. Construct Args pointing to this temp project.
+        let args = Args::try_parse_from(&[
+            "cargo-anneal",
+            "--manifest-path",
+            proj_dir.join("Cargo.toml").to_str().unwrap(),
+        ])
+        .unwrap();
+
+        // 5. Resolve roots.
+        let roots = resolve_roots(&args).unwrap();
+
+        // 6. Scan workspace.
+        let packages = scan_workspace(&roots, ScanMode::WorkspaceOnly).unwrap();
+        assert_eq!(packages.len(), 1);
+
+        // 7. Lock run root.
+        let locked_roots = roots.lock_run_root().unwrap();
+
+        // 8. Resolve standard developer toolchain and run charon.
+        let toolchain = resolve_test_toolchain();
+
+        let res = run_charon(
+            &args,
+            &toolchain,
+            &locked_roots,
+            &packages,
+            false, // show_progress
+        );
+        assert!(res.is_ok(), "charon failed: {:?}", res.err());
+
+        // 9. Verify .llbc file exists.
+        let llbc_path = packages[0].llbc_path(&locked_roots);
+        assert!(llbc_path.exists(), "llbc file not found at {:?}", llbc_path);
+    }
+
+    #[cfg(feature = "exocrate_tests")]
+    #[test]
+    fn test_run_charon_multiple_modules() {
+        let _ = env_logger::builder().is_test(true).try_init();
+
+        // 1. Create a temporary workspace with multiple modules.
+        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 mod foo;
+                pub mod bar;
+            "#,
+            "src/foo.rs" => r#"
+                pub fn foo_fn() {}
+            "#,
+            "src/bar.rs" => r#"
+                pub fn bar_fn() {}
+            "#,
+        });
+
+        // 2. Construct Args pointing to this temp project.
+        let args = Args::try_parse_from(&[
+            "cargo-anneal",
+            "--manifest-path",
+            temp_dir.path().join("Cargo.toml").to_str().unwrap(),
+        ])
+        .unwrap();
+
+        // 3. Resolve roots and scan workspace.
+        let roots = resolve_roots(&args).unwrap();
+        let packages = scan_workspace(&roots, ScanMode::WorkspaceOnly).unwrap();
+        assert_eq!(packages.len(), 1);
+
+        // 4. Lock run root.
+        let locked_roots = roots.lock_run_root().unwrap();
+
+        // 5. Resolve toolchain and run charon.
+        let toolchain = resolve_test_toolchain();
+        let res = run_charon(
+            &args,
+            &toolchain,
+            &locked_roots,
+            &packages,
+            false, // show_progress
+        );
+        assert!(res.is_ok(), "charon failed: {:?}", res.err());
+
+        // 6. Verify .llbc file exists and contains BOTH functions.
+        let llbc_path = packages[0].llbc_path(&locked_roots);
+        assert!(llbc_path.exists(), "llbc file not found at {:?}", llbc_path);
+
+        log::debug!("llbc path: {:?}", llbc_path);
+
+        let llbc_content = std::fs::read_to_string(&llbc_path).expect("failed to read llbc file");
+
+        log::debug!("llbc content:\n'''\n{}\n'''", llbc_content);
+
+        // Assert that the serialized AST contains the names of both functions
+        // defined in separate, independent modules.
+        assert!(llbc_content.contains("foo_fn"), "Function 'foo_fn' was not translated!");
+        assert!(llbc_content.contains("bar_fn"), "Function 'bar_fn' was not translated!");
+    }
+
+    #[cfg(feature = "exocrate_tests")]
+    #[test]
+    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();
+        crate::workspace_fixture!(&temp_dir, {
+            "Cargo.toml" => r#"
+                [package]
+                name = "test_proj"
+                version = "0.1.0"
+                edition = "2021"
+
+                [dependencies]
+                fs2 = "0.4.3"
+
+                [lib]
+                path = "src/lib.rs"
+            "#,
+            "src/lib.rs" => r#"
+                pub fn get_free_space(path: &std::path::Path) -> u64 {
+                    fs2::free_space(path).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();
+        assert_eq!(packages.len(), 1);
+        let locked_roots = roots.lock_run_root().unwrap();
+
+        let toolchain = resolve_test_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());
+
+        // 1. Assert that the local function 'get_free_space' is fully translated with a structured body definition.
+        assert_fn_body(&llbc_path, &["test_proj", "get_free_space"], true, true);
+
+        // 2. Assert that the crates.io dependency 'fs2::free_space' is referred to but NOT translated (opaque).
+        assert_fn_body(&llbc_path, &["fs2", "free_space"], false, false);
+
+        // Standard library calls may be lowered directly into the calling crate rather than
+        // emitted as standalone LLBC declarations.
+    }
+
+    #[cfg(feature = "exocrate_tests")]
+    #[test]
+    fn test_charon_path_dependency_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#"
+                [workspace]
+                resolver = "2"
+                members = [
+                    "test_proj",
+                ]
+            "#,
+            "my_dep/Cargo.toml" => r#"
+                [package]
+                name = "my_dep"
+                version = "0.1.0"
+                edition = "2021"
+
+                [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();
+
+        let roots = resolve_roots(&args).unwrap();
+        let packages = scan_workspace(&roots, ScanMode::WorkspaceOnly).unwrap();
+        assert_eq!(packages.len(), 1);
+        let locked_roots = roots.lock_run_root().unwrap();
+
+        let toolchain = resolve_test_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());
+
+        // 1. Assert that local target function 'call_dep' is fully translated (definition included).
+        assert_fn_body(&llbc_path, &["test_proj", "call_dep"], true, true);
+
+        // 2. Assert that local path dependency 'my_dep::dep_fn' is referred to but NOT translated (opaque).
+        assert_fn_body(&llbc_path, &["my_dep", "dep_fn"], false, false);
+    }
+
+    #[cfg(feature = "exocrate_tests")]
+    #[test]
+    fn test_run_charon_multiple_packages() {
+        let _ = env_logger::builder().is_test(true).try_init();
+
+        // 1. Create a temporary workspace containing multiple packages.
+        let temp_dir = tempfile::tempdir().unwrap();
+        crate::workspace_fixture!(&temp_dir, {
+            "Cargo.toml" => r#"
+                [workspace]
+                resolver = "2"
+                members = [
+                    "package_a",
+                    "package_b",
+                ]
+            "#,
+            "package_a/Cargo.toml" => r#"
+                [package]
+                name = "package_a"
+                version = "0.1.0"
+                edition = "2021"
+
+                [lib]
+                path = "src/lib.rs"
+            "#,
+            "package_a/src/lib.rs" => r#"
+                pub fn func_a() {}
+            "#,
+            "package_b/Cargo.toml" => r#"
+                [package]
+                name = "package_b"
+                version = "0.1.0"
+                edition = "2021"
+
+                [lib]
+                path = "src/lib.rs"
+            "#,
+            "package_b/src/lib.rs" => r#"
+                pub fn func_b() {}
+            "#,
+        });
+
+        // 2. Construct Args pointing to this temp project.
+        let args = Args::try_parse_from(&[
+            "cargo-anneal",
+            "--manifest-path",
+            temp_dir.path().join("Cargo.toml").to_str().unwrap(),
+        ])
+        .unwrap();
+
+        // 3. Resolve roots and scan workspace.
+        let roots = resolve_roots(&args).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.
+        let locked_roots = roots.lock_run_root().unwrap();
+
+        // 5. Resolve toolchain and run charon on both packages.
+        let toolchain = resolve_test_toolchain();
+        let res = run_charon(
+            &args,
+            &toolchain,
+            &locked_roots,
+            &packages,
+            false, // show_progress
+        );
+        assert!(res.is_ok(), "charon failed: {:?}", res.err());
+
+        // 6. Verify .llbc file exists and contains correct code for Package A.
+        let llbc_path_a = packages[0].llbc_path(&locked_roots);
+        assert!(llbc_path_a.exists(), "llbc file for Package A not found at {:?}", llbc_path_a);
+        let llbc_content_a =
+            std::fs::read_to_string(&llbc_path_a).expect("failed to read llbc file A");
+        assert!(
+            llbc_content_a.contains("func_a"),
+            "Function 'func_a' was not translated in Package A!"
+        );
+        assert!(
+            !llbc_content_a.contains("func_b"),
+            "Function 'func_b' was incorrectly translated in Package A!"
+        );
+
+        // 7. Verify .llbc file exists and contains correct code for Package B.
+        let llbc_path_b = packages[1].llbc_path(&locked_roots);
+        assert!(llbc_path_b.exists(), "llbc file for Package B not found at {:?}", llbc_path_b);
+        let llbc_content_b =
+            std::fs::read_to_string(&llbc_path_b).expect("failed to read llbc file B");
+        assert!(
+            llbc_content_b.contains("func_b"),
+            "Function 'func_b' was not translated in Package B!"
+        );
+        assert!(
+            !llbc_content_b.contains("func_a"),
+            "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 = resolve_test_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());
+        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!
+        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
+        );
+        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"
+
+                [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);
+                }
+            "#,
+        });
+
+        write_log_path_dependency_fixture(&temp_dir);
+
+        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 = resolve_test_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", "max_level"], true, true);
+
+        // 6. Verify that the local crate still compiled while depending on the promoted crate.
+        let llbc_path_local = local_target.llbc_path(&locked_roots);
+        assert_fn_body(&llbc_path_local, &["test_proj", "log_info"], true, true);
+    }
+
+    #[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();
+
+        write_log_path_dependency_fixture(&temp_dir);
+
+        // 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 = resolve_test_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", "max_level"], 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 = resolve_test_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());
+
+        assert_fn_body(&llbc_path, &["test_proj", "call_unwrap"], true, true);
+    }
+
+    #[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();
+        assert_eq!(packages.len(), 1);
+        let locked_roots = roots.lock_run_root().unwrap();
+
+        let toolchain = resolve_test_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());
+
+        assert_fn_body(&llbc_path, &["test_proj", "call_unwrap"], true, true);
+    }
+}
diff --git a/anneal/v2/src/diagnostics.rs b/anneal/v2/src/diagnostics.rs
new file mode 100644
index 0000000000..70fdcb98de
--- /dev/null
+++ b/anneal/v2/src/diagnostics.rs
@@ -0,0 +1,336 @@
+// Copyright 2026 The Fuchsia Authors
+//
+// Licensed under the 2-Clause BSD License <LICENSE-BSD or
+// https://opensource.org/license/bsd-2-clause>, Apache License, Version 2.0
+// <LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+// license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
+// This file may not be copied, modified, or distributed except according to
+// those terms.
+
+// Handling of Lean diagnostics and error mapping.
+//
+// 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.
+
+pub use cargo_metadata::diagnostic::{Diagnostic, DiagnosticLevel, DiagnosticSpan};
+
+/// Maps diagnostics from generated intermediate code back to pristine,
+/// original source code files.
+///
+/// Lean has no knowledge of the Rust files that orchestrated its execution.
+/// It only reports errors against the generated `.lean` artifact files.
+///
+/// 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`
+/// workspace files.
+pub struct DiagnosticMapper {
+    user_root: std::path::PathBuf,
+    user_root_canonical: std::path::PathBuf,
+    source_cache: std::collections::HashMap<std::path::PathBuf, String>,
+}
+
+#[derive(thiserror::Error, Debug)]
+#[error("{message}")]
+struct MappedError {
+    message: String,
+    src: miette::NamedSource<String>,
+    labels: Vec<miette::LabeledSpan>,
+    help: Option<String>,
+    related: Vec<MappedError>,
+    severity: Option<miette::Severity>,
+}
+
+impl miette::Diagnostic for MappedError {
+    fn source_code(&self) -> Option<&dyn miette::SourceCode> {
+        Some(&self.src)
+    }
+
+    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())) }
+    }
+
+    fn help(&self) -> Option<Box<dyn std::fmt::Display + '_>> {
+        self.help.as_ref().map(|h| Box::new(h.clone()) as Box<dyn std::fmt::Display>)
+    }
+
+    fn related<'a>(
+        &'a self,
+    ) -> Option<Box<dyn std::iter::Iterator<Item = &'a dyn miette::Diagnostic> + 'a>> {
+        if self.related.is_empty() {
+            None
+        } else {
+            let iter = self.related.iter().map(|e| e as &dyn miette::Diagnostic);
+            Some(Box::new(iter))
+        }
+    }
+
+    fn severity(&self) -> Option<miette::Severity> {
+        self.severity
+    }
+}
+
+impl DiagnosticMapper {
+    /// Creates a new mapper rooted at `user_root`.
+    pub fn new(user_root: std::path::PathBuf) -> Self {
+        let user_root_canonical =
+            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: &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 = std::path::PathBuf::new();
+            for component in p.components() {
+                let most_recent = normalized.components().next_back();
+                match (component, most_recent) {
+                    (std::path::Component::ParentDir, Some(std::path::Component::Normal(_))) => {
+                        normalized.pop();
+                    }
+                    (std::path::Component::CurDir, _) => {}
+                    _ => normalized.push(component),
+                }
+            }
+            normalized
+        };
+
+        // 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: &std::path::Path) -> Option<String> {
+        if let Some(src) = self.source_cache.get(path) {
+            return Some(src.clone());
+        }
+        if let Ok(src) = std::fs::read_to_string(path) {
+            self.source_cache.insert(path.to_path_buf(), src.clone());
+            Some(src)
+        } else {
+            None
+        }
+    }
+
+    /// Renders a diagnostic (from Cargo or Charon) using `miette`.
+    ///
+    /// This is strictly for rendering errors native to Rust processing (where
+    /// the structured error originates from our `syn` parser or Charon's
+    /// processing), bringing them into a unified, colorized `miette` format.
+    pub fn render_miette<F>(&mut self, diag: &Diagnostic, mut printer: F)
+    where
+        F: FnMut(String),
+    {
+        let mut mapped_paths_and_spans: std::collections::HashMap<
+            std::path::PathBuf,
+            Vec<&DiagnosticSpan>,
+        > = std::collections::HashMap::new();
+
+        // 1) Group spans by mapped path.
+        for s in &diag.spans {
+            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);
+            }
+        }
+
+        // TODO: Should we be collecting all of them, not just the first?
+        let help_msg = diag
+            .children
+            .iter()
+            .find(|child| child.level == DiagnosticLevel::Help)
+            .map(|child| child.message.clone());
+
+        if !mapped_paths_and_spans.is_empty() {
+            // Find the path that contains the primary span, or just take the
+            // first one.
+            let primary_path = diag
+                .spans
+                .iter()
+                .find(|s| s.is_primary)
+                .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<std::path::PathBuf> =
+                    mapped_paths_and_spans.keys().cloned().collect();
+                paths.sort_by_key(|p| p != &main_path);
+
+                for p in paths {
+                    if let Some(src) = self.get_source(&p) {
+                        let labels: Vec<_> = mapped_paths_and_spans
+                            .get(&p)
+                            .unwrap()
+                            .iter()
+                            .filter_map(|s| {
+                                let label_text = s.label.clone().unwrap_or_default();
+                                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 = miette::SourceOffset::from(start);
+                                    miette::LabeledSpan::new(Some(label_text), offset.offset(), len)
+                                })
+                            })
+                            .collect();
+
+                        let err = MappedError {
+                            message: if p == main_path {
+                                diag.message.clone()
+                            } else {
+                                format!("related to: {}", p.display())
+                            },
+                            src: miette::NamedSource::new(p.to_string_lossy(), src),
+                            labels,
+                            help: if p == main_path { help_msg.clone() } else { None },
+                            related: Vec::new(),
+                            severity: match diag.level {
+                                DiagnosticLevel::Error | DiagnosticLevel::Ice => {
+                                    Some(miette::Severity::Error)
+                                }
+                                DiagnosticLevel::Warning => Some(miette::Severity::Warning),
+                                _ => Some(miette::Severity::Advice),
+                            },
+                        };
+                        all_errors.push(err);
+                    }
+                }
+
+                if !all_errors.is_empty() {
+                    let mut main_err = all_errors.remove(0);
+                    main_err.related = all_errors;
+                    printer(format!("{:?}", miette::Report::new(main_err)));
+                    return;
+                }
+            }
+        }
+
+        // If we get here, no span was successfully mapped.
+        let prefix = match diag.level {
+            DiagnosticLevel::Error | DiagnosticLevel::Ice => "[External Error]",
+            DiagnosticLevel::Warning => "[External Warning]",
+            _ => "[External Info]",
+        };
+
+        if let Some(span) = diag.spans.first() {
+            printer(format!("{} {}:{}: {}", prefix, span.file_name, span.line_start, diag.message));
+        } else {
+            printer(format!("{} {}", prefix, diag.message));
+        }
+    }
+
+    /// Renders a diagnostic (e.g., from Lean) directly at a mapped byte
+    /// range.
+    ///
+    /// The fundamental workflow for an external error is:
+    /// 1. Lean encounters a verification failure and emits a JSON line
+    ///    containing its local start/end bytes in the `.lean` artifact.
+    /// 2. Anneal checks the cached `SourceMapping` array for that artifact,
+    ///    and discovers exactly where the Lean bytes translate back to Rust
+    ///    bytes.
+    /// 3. Anneal calls this method to print the error onto the Rust file
+    ///    canvas.
+    #[allow(dead_code)]
+    pub fn render_raw<F>(
+        &mut self,
+        file_name: &str,
+        message: String,
+        level: DiagnosticLevel,
+        byte_start: usize,
+        byte_end: usize,
+        mut printer: F,
+    ) where
+        F: FnMut(String),
+    {
+        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)
+        {
+            let start = byte_start;
+            if byte_end >= start {
+                let len = byte_end - start;
+                if start <= src.len() && start + len <= src.len() {
+                    let offset = miette::SourceOffset::from(start);
+                    let label =
+                        miette::LabeledSpan::new(Some("here".to_string()), offset.offset(), len);
+                    let err = MappedError {
+                        message,
+                        src: miette::NamedSource::new(mapped_path.to_string_lossy(), src),
+                        labels: vec![label],
+                        help: None,
+                        related: Vec::new(),
+                        severity: match level {
+                            DiagnosticLevel::Error | DiagnosticLevel::Ice => {
+                                Some(miette::Severity::Error)
+                            }
+                            DiagnosticLevel::Warning => Some(miette::Severity::Warning),
+                            _ => Some(miette::Severity::Advice),
+                        },
+                    };
+                    printer(format!("{:?}", miette::Report::new(err)));
+                    return;
+                }
+            }
+        }
+
+        // Fallback.
+        let prefix = match level {
+            DiagnosticLevel::Error | DiagnosticLevel::Ice => "[External Error]",
+            DiagnosticLevel::Warning => "[External Warning]",
+            _ => "[External Info]",
+        };
+        printer(format!("{} {}: {}", prefix, file_name, message));
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_map_path_traversal() {
+        let temp = tempfile::tempdir().unwrap();
+        let user_root = temp.path().join("workspace");
+        std::fs::create_dir(&user_root).unwrap();
+
+        // 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();
+
+        let mapper = DiagnosticMapper::new(user_root.clone());
+
+        let malicious_path = user_root.join("symlink/../passwd");
+
+        let mapped = mapper.map_path(&malicious_path);
+
+        // The path normalization routine relies on lexical analysis. It
+        // normalizes `workspace/symlink/../passwd` into `workspace/passwd`.
+        // Even though a physical resolution of this path would point to
+        // `outside/passwd` via the symlink, the lexical flattening grounds it
+        // back into the workspace root. Because the mapped path is inside the
+        // tree, the logic considers it sound and explicitly strips the
+        // traversal.
+        //
+        // Conversely, attempts to escape the root directory directly using `..`
+        // without an internal symlink are trapped and rejected.
+        let escaped_path = user_root.join("../outside/passwd");
+        assert_eq!(mapper.map_path(&escaped_path), None, "Path traversal should be rejected");
+
+        // The lexically normalized path inside the symlink safely maps to
+        // `workspace/passwd`.
+        assert_eq!(mapped, Some(user_root.join("passwd")));
+    }
+}
diff --git a/anneal/v2/src/main.rs b/anneal/v2/src/main.rs
index d5b672d035..c98c8b8bea 100644
--- a/anneal/v2/src/main.rs
+++ b/anneal/v2/src/main.rs
@@ -7,8 +7,16 @@
 // This file may not be copied, modified, or distributed except according to
 // those terms.
 
+use anyhow::Context as _;
 use clap::Parser as _;
 
+mod charon;
+mod diagnostics;
+mod resolve;
+mod scanner;
+mod setup;
+mod util;
+
 /// Anneal
 #[derive(clap::Parser, Debug)]
 #[command(name = "cargo-anneal", version, about, long_about = None)]
@@ -21,50 +29,86 @@ struct Cli {
 enum Commands {
     /// Setup Anneal dependencies
     Setup(SetupArgs),
+    /// Expand a crate (runs Charon)
+    Expand(ExpandArgs),
+
+    /// Helper to acquire shared or exclusive locks for multi-process integration testing (dev only)
+    #[cfg(feature = "exocrate_tests")]
+    TestLockHelper {
+        /// The role to run as: 'reader-a', 'reader-b', 'writer-a', or 'reader-exclusion'
+        #[arg(long)]
+        role: String,
+        /// Path to the directory to lock
+        #[arg(long)]
+        lock_dir: std::path::PathBuf,
+        /// Path to the shared log file where lock transitions are appended
+        #[arg(long)]
+        log_file: std::path::PathBuf,
+        /// Path to the temporary synchronization signal file
+        #[arg(long)]
+        sig_file: std::path::PathBuf,
+    },
 }
 
 #[derive(clap::Parser, Debug)]
 pub struct SetupArgs {
-    /// Path to a local dependency archive to use instead of downloading.
+    /// Path to a local dependency archive to use instead of downloading
     #[arg(long, value_name = "path-to-local-archive")]
     pub local_archive: Option<std::path::PathBuf>,
 }
 
-exocrate::config! {
-    const CONFIG: Config = Config {
-        rel_dir_path: [".anneal", "toolchain"],
-        versioned_files: &["../Cargo.toml", "../Cargo.lock"],
-    };
+#[derive(clap::Parser, Debug)]
+pub struct ExpandArgs {
+    #[command(flatten)]
+    pub resolve_args: crate::resolve::Args,
+
+    /// Controls where LLBC output is placed on the filesystem
+    #[arg(long, value_name = "output-dir")]
+    pub output_dir: Option<std::path::PathBuf>,
+
+    /// 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,
 }
 
-exocrate::parse_remote_archive! {
-    const REMOTE: RemoteArchive = "Cargo.toml" [
-        (linux, x86_64),
-        (macos, x86_64),
-        (linux, aarch64),
-        (macos, aarch64),
-    ];
+fn setup(args: SetupArgs) -> anyhow::Result<()> {
+    crate::setup::run_setup(crate::setup::SetupArgs { local_archive: args.local_archive })
+        .context("Failed to setup toolchain")
 }
 
-fn setup(args: SetupArgs) {
-    let location = if std::env::var("__ANNEAL_LOCAL_DEV").is_ok() {
-        exocrate::Location::LocalDev
+fn expand(args: ExpandArgs) -> anyhow::Result<()> {
+    let roots = crate::resolve::resolve_roots(&args.resolve_args)?;
+    let mode = if args.include_dependencies {
+        crate::scanner::ScanMode::FollowDependencies
     } else {
-        exocrate::Location::UserGlobal
+        crate::scanner::ScanMode::WorkspaceOnly
     };
-    let source = match args.local_archive {
-        Some(local_archive) => exocrate::Source::Local(local_archive),
-        None => exocrate::Source::Remote(REMOTE),
-    };
-
-    let installation_dir = CONFIG
-        .resolve_installation_dir_or_install(location, source)
-        // FIXME: Implement unified error reporting (e.g., via `anyhow`).
-        .expect("failed to resolve-or-install dependencies");
-    log::info!("anneal toolchain is installed at {:?}", installation_dir);
+    let packages = crate::scanner::scan_workspace(&roots, mode)?;
+    if packages.is_empty() {
+        log::warn!("No targets found to expand.");
+        return Ok(());
+    }
+    let mut locked_roots = roots.lock_run_root()?;
+    if let Some(output_dir) = args.output_dir {
+        locked_roots.llbc_override = Some(output_dir);
+    }
+    let toolchain = crate::setup::Toolchain::resolve()?;
+    let show_progress = !args.no_progress;
+    crate::charon::run_charon(
+        &args.resolve_args,
+        &toolchain,
+        &locked_roots,
+        &packages,
+        show_progress,
+    )?;
+    Ok(())
 }
 
-fn main() {
+fn main() -> anyhow::Result<()> {
     // Suppressing timestamps removes a source of nondeterminism that is
     // difficult to work around in integration tests.
     env_logger::builder().format_timestamp(None).init();
@@ -79,6 +123,12 @@ fn main() {
 
     match args.command {
         Commands::Setup(args) => setup(args),
+        Commands::Expand(args) => expand(args),
+
+        #[cfg(feature = "exocrate_tests")]
+        Commands::TestLockHelper { role, lock_dir, log_file, sig_file } => {
+            crate::util::run_test_lock_helper(&role, &lock_dir, &log_file, &sig_file)
+        }
     }
 }
 
@@ -86,11 +136,42 @@ fn main() {
 mod tests {
     #[cfg(feature = "exocrate_tests")]
     #[test]
-    fn test_setup() {
+    fn test_setup_and_toolchain_paths() {
+        // 1. Run setup.
         super::setup(super::SetupArgs {
             // ASSUMPTION: Dependency builder installs archive at
             // `target/anneal-exocrate.tar.zst`.
             local_archive: Some("target/anneal-exocrate.tar.zst".into()),
         })
+        .expect("Failed to run setup");
+
+        // 2. Once setup completes successfully, resolve the toolchain.
+        let toolchain = crate::setup::Toolchain::resolve().expect("Failed to resolve toolchain");
+
+        // 3. Verify that all returned paths exist as directories.
+        // Note: these assertions would be more appropriate in the setup.rs module,
+        // but including them here avoids introducing multiple tests that attempt to
+        // extract the (large) anneal exocrate archive.
+        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/resolve.rs b/anneal/v2/src/resolve.rs
new file mode 100644
index 0000000000..91cf5d9e44
--- /dev/null
+++ b/anneal/v2/src/resolve.rs
@@ -0,0 +1,486 @@
+// Copyright 2026 The Fuchsia Authors
+//
+// Licensed under the 2-Clause BSD License <LICENSE-BSD or
+// https://opensource.org/license/bsd-2-clause>, Apache License, Version 2.0
+// <LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+// license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
+// This file may not be copied, modified, or distributed except according to
+// those terms.
+
+use anyhow::Context as _;
+use sha2::Digest as _;
+
+#[derive(clap::Parser, Debug)]
+pub struct Args {
+    #[command(flatten)]
+    pub manifest: clap_cargo::Manifest,
+
+    #[command(flatten)]
+    pub workspace: clap_cargo::Workspace,
+
+    #[command(flatten)]
+    pub features: clap_cargo::Features,
+
+    /// Verify the library target.
+    #[arg(long)]
+    pub lib: bool,
+
+    /// Verify specific binary targets.
+    #[arg(long)]
+    pub bin: Vec<String>,
+
+    /// Verify all binary targets.
+    #[arg(long)]
+    pub bins: bool,
+
+    /// Verify specific example targets.
+    #[arg(long)]
+    pub example: Vec<String>,
+
+    /// Verify all example targets.
+    #[arg(long)]
+    pub examples: bool,
+
+    /// Verify specific test targets.
+    #[arg(long)]
+    pub test: Vec<String>,
+
+    /// Verify all test targets.
+    #[arg(long)]
+    pub tests: bool,
+
+    /// Allow `sorry` in proofs and inject `sorry` for missing proofs.
+    #[arg(long)]
+    pub allow_sorry: bool,
+
+    /// 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
+    /// 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.
+    ///
+    /// Once the `syn` parser supports parsing `unsafe` fields (which are
+    /// already supported in a nightly Rust feature), Anneal will require that
+    /// `isValid` is only used on `unsafe` fields.
+    #[arg(long)]
+    pub unsound_allow_is_valid: bool,
+}
+
+#[derive(clap::Parser, Debug)]
+pub struct SetupArgs {}
+
+#[derive(Debug, Copy, Clone, PartialEq, Eq, Hash)]
+#[repr(u8)]
+pub enum AnnealTargetKind {
+    /// A library target (generic).
+    Lib,
+    /// A Rust library.
+    RLib,
+    /// A procedural macro library.
+    ProcMacro,
+    /// A C-compatible dynamic library.
+    CDyLib,
+    /// A dynamic Rust library.
+    DyLib,
+    /// A static system library.
+    StaticLib,
+    /// A binary executable.
+    Bin,
+    /// A documentation example.
+    Example,
+    /// An integration test.
+    Test,
+}
+
+impl AnnealTargetKind {
+    pub fn is_lib(&self) -> bool {
+        use AnnealTargetKind::*;
+        matches!(self, Lib | RLib | ProcMacro | CDyLib | DyLib | StaticLib)
+    }
+}
+
+impl std::convert::TryFrom<&cargo_metadata::TargetKind> for AnnealTargetKind {
+    type Error = ();
+
+    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),
+            ProcMacro => Ok(Self::ProcMacro),
+            CDyLib => Ok(Self::CDyLib),
+            DyLib => Ok(Self::DyLib),
+            StaticLib => Ok(Self::StaticLib),
+            Bin => Ok(Self::Bin),
+            Example => Ok(Self::Example),
+            Test => Ok(Self::Test),
+            // Need `_` because `TargetKind` is `#[non_exhaustive]`.
+            Bench | CustomBuild | _ => Err(()),
+        }
+    }
+}
+
+#[derive(Clone, Debug, Hash, PartialEq, Eq)]
+pub struct AnnealTargetName {
+    pub package_name: cargo_metadata::PackageName,
+    pub target_name: String,
+    pub kind: AnnealTargetKind,
+}
+
+/// A fully resolved target ready for verification.
+///
+/// This struct bridges the gap between `cargo_metadata`'s view of the world
+/// and Anneal's verification pipeline. It contains absolute paths to critical
+/// files, ensuring that downstream tools (Scanner, Charon) don't need to resolve
+/// paths relative to the CWD or workspace root again.
+#[derive(Debug)]
+pub struct AnnealTarget {
+    pub name: AnnealTargetName,
+    pub kind: AnnealTargetKind,
+
+    /// Path to the `Cargo.toml` for this target.
+    pub manifest_path: std::path::PathBuf,
+}
+
+#[derive(Debug)]
+pub struct Roots {
+    pub workspace: std::path::PathBuf,
+    // E.g., `target/anneal`.
+    anneal_global_root: std::path::PathBuf,
+    // E.g., `target/anneal/<hash>`.
+    anneal_run_root: std::path::PathBuf,
+    pub roots: Vec<AnnealTarget>,
+    pub metadata: cargo_metadata::Metadata,
+}
+
+impl Roots {
+    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) -> std::path::PathBuf {
+        self.anneal_global_root.join("cargo_target")
+    }
+}
+
+/// 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
+/// filesystem operations are guarded by the `BuildLock`.
+pub struct LockedRoots<'a> {
+    roots: &'a Roots,
+    anneal_run_root: crate::util::DirLock,
+    pub llbc_override: Option<std::path::PathBuf>,
+}
+
+impl<'a> LockedRoots<'a> {
+    pub fn llbc_root(&self) -> std::path::PathBuf {
+        if let Some(ref over) = self.llbc_override {
+            over.clone()
+        } else {
+            self.anneal_run_root.path.join("llbc")
+        }
+    }
+
+    #[allow(dead_code)]
+    pub fn lean_root(&self) -> std::path::PathBuf {
+        self.anneal_run_root.path.join("lean")
+    }
+
+    #[allow(dead_code)]
+    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) -> std::path::PathBuf {
+        self.roots.cargo_target_dir()
+    }
+
+    pub fn workspace(&self) -> &std::path::PathBuf {
+        &self.roots.workspace
+    }
+}
+
+/// Resolves all verification roots.
+///
+/// Each entry represents a distinct compilation artifact to be verified.
+pub fn resolve_roots(args: &Args) -> anyhow::Result<Roots> {
+    log::trace!("resolve_roots({:?})", args);
+    let mut cmd = cargo_metadata::MetadataCommand::new();
+
+    if let Some(path) = &args.manifest.manifest_path {
+        cmd.manifest_path(path);
+    }
+
+    // Forward features to ensure dependency resolution matches the user's
+    // request. This is critical because conditional compilation
+    // (via `#[cfg(feature = "...")]`) can completely change the shape of
+    // the dependency graph and the source code itself. If we resolved
+    // metadata without these flags, we might miss dependencies or include
+    // dependencies that are not actually used in the build.
+    args.features.forward_metadata(&mut cmd);
+
+    let metadata = cmd.exec().context("Failed to run 'cargo metadata'")?;
+    // We enforce that all local dependencies are contained within the workspace
+    // root. This is a temporary limitation to simplify the verification model
+    // and ensure a "hermetic-like" boundary for analysis. It prevents issues
+    // where experimental or local forks of dependencies might be picked up
+    // unpredictably, or where Charon might struggle to locate source files
+    // outside the standard project structure.
+    check_for_external_deps(&metadata)?;
+
+    let selected_packages =
+        resolve_packages(&metadata, &args.workspace, args.manifest.manifest_path.as_deref())?;
+
+    let (anneal_global_root, anneal_run_root) = resolve_run_roots(&metadata);
+    let mut roots = Roots {
+        workspace: metadata.workspace_root.as_std_path().to_owned(),
+        // cargo_target_dir: metadata.target_directory.as_std_path().to_owned(),
+        anneal_global_root,
+        anneal_run_root,
+        roots: Vec::new(),
+        metadata: metadata.clone(), // `metadata` must outlive `selected_packages`.
+    };
+
+    for package in selected_packages {
+        log::trace!("Scanning package: {}", package.name);
+
+        let targets = resolve_targets(package, args)?;
+
+        if targets.is_empty() {
+            log::warn!("No matching targets found for package '{}'", package.name);
+            continue;
+        }
+
+        roots.roots.extend(targets.into_iter().map(|(target, kind)| AnnealTarget {
+            name: AnnealTargetName {
+                package_name: package.name.clone(),
+                target_name: target.name.clone(),
+                kind,
+            },
+            kind,
+            // We convert to absolute paths here to establish a canonical
+            // reference for the rest of the pipeline. This avoids ambiguity
+            // if the CWD changes or if we're working with complex workspace
+            // structures.
+            manifest_path: package.manifest_path.as_std_path().to_owned(),
+        }));
+    }
+
+    Ok(roots)
+}
+
+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.
+    let target_dir = metadata.target_directory.as_std_path();
+    let anneal_global = target_dir.join("anneal");
+
+    // Used by integration tests to ensure deterministic shadow dir names.
+    if let Ok(name) = std::env::var("ANNEAL_TEST_DIR_NAME") {
+        let run_root = anneal_global.join(name);
+        return (anneal_global, run_root);
+    }
+
+    // Hash the path to the workspace root to avoid collisions between different
+    // workspaces using the same target directory. We use SHA-256 (truncated to
+    // 64 bits) for stable hashing across Rust versions. This ensures that the
+    // build directory name remains consistent for the same workspace root,
+    // avoiding unnecessary cache invalidation.
+    let workspace_root_hash = {
+        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();
+        let mut bytes = [0u8; 8];
+        bytes.copy_from_slice(&result[0..8]);
+        u64::from_le_bytes(bytes)
+    };
+
+    let run_root = anneal_global.join(format!("{workspace_root_hash:x}"));
+    (anneal_global, run_root)
+}
+
+/// Resolves which packages to process based on workspace flags and CWD.
+fn resolve_packages<'a>(
+    metadata: &'a cargo_metadata::Metadata,
+    args: &clap_cargo::Workspace,
+    manifest_path: Option<&std::path::Path>,
+) -> 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).
+        args.package
+            .iter()
+            .map(|name| {
+                metadata
+                    .packages
+                    .iter()
+                    .find(|p| p.name == *name)
+                    .ok_or_else(|| anyhow::anyhow!("Package '{}' not found in workspace", name))
+            })
+            .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
+        // in the graph but are not members (e.g. dependencies).
+        metadata
+            .workspace_members
+            .iter()
+            .filter_map(|id| metadata.packages.iter().find(|p| &p.id == id))
+            .collect()
+    } else {
+        // Resolve default (Current Working Directory). This mimics Cargo's
+        // behavior: if we are inside a package, we build that package. If we
+        // are at the workspace root, we build the whole workspace.
+        let cwd = {
+            let cwd_candidate = manifest_path
+                .map(|p| p.to_path_buf())
+                .unwrap_or_else(|| std::env::current_dir().unwrap_or_default())
+                .canonicalize()
+                .context("Failed to canonicalize CWD")?;
+
+            // If the user explicitly provided `--manifest-path`, Cargo treats
+            // its parent directory as the effective CWD.
+            if manifest_path.is_some() {
+                cwd_candidate.parent().unwrap_or(&cwd_candidate).to_path_buf()
+            } else {
+                cwd_candidate
+            }
+        };
+
+        // 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)
+        });
+
+        if let Some(pkg) = current_pkg {
+            vec![pkg]
+        } else {
+            // Fallback: If we are at the workspace root (virtual manifest),
+            // behave like --workspace.
+            if cwd == metadata.workspace_root.as_std_path() {
+                metadata
+                    .workspace_members
+                    .iter()
+                    .filter_map(|id| metadata.packages.iter().find(|p| &p.id == id))
+                    .collect()
+            } else {
+                return Err(anyhow::anyhow!(
+                    "Could not determine package from current directory. Please use -p <NAME> or --workspace."
+                ));
+            }
+        }
+    };
+
+    // Filter out excluded packages (--exclude).
+    if !args.exclude.is_empty() {
+        packages.retain(|p| !args.exclude.contains(&p.name));
+    }
+
+    Ok(packages)
+}
+
+/// Flattening Resolver:
+/// Returns a list of (Target, TargetKind) pairs.
+/// If a target is defined as `crate-type = ["rlib", "cdylib"]`, and both are
+/// requested, this returns two entries, allowing them to be verified
+/// independently.
+///
+/// This flattening is critical because different crate types may be compiled
+/// with different flags or conditional compilation options (although the
+/// current scanner is CFG-agnostic, future improvements might respect this).
+/// Verifying them independently ensures we cover all intended compilation
+/// modes.
+fn resolve_targets<'a>(
+    package: &'a cargo_metadata::Package,
+    args: &Args,
+) -> anyhow::Result<Vec<(&'a cargo_metadata::Target, AnnealTargetKind)>> {
+    log::trace!("resolve_targets({})", package.name);
+    let default_mode = !args.lib
+        && args.bin.is_empty()
+        && !args.bins
+        && args.example.is_empty()
+        && !args.examples
+        && args.test.is_empty()
+        && !args.tests;
+
+    // Filter targets based on the requested verification mode.
+    // Unlike Cargo, which might build everything by default, we try to be
+    // selectively inclusive to avoid overwhelming the user with verification
+    // tasks they didn't ask for.
+    let selected_artifacts: Vec<_> = package
+        .targets
+        .iter()
+        .flat_map(|target| {
+            target.kind.iter().filter_map(move |raw_kind| {
+                let kind = AnnealTargetKind::try_from(raw_kind).ok()?;
+
+                let include = if default_mode {
+                    kind.is_lib() || kind == AnnealTargetKind::Bin
+                } else {
+                    (args.lib && kind.is_lib())
+                        || (args.bins && kind == AnnealTargetKind::Bin)
+                        || (args.bin.contains(&target.name) && kind == AnnealTargetKind::Bin)
+                        || (args.examples && kind == AnnealTargetKind::Example)
+                        || (args.example.contains(&target.name)
+                            && kind == AnnealTargetKind::Example)
+                        || (args.tests && kind == AnnealTargetKind::Test)
+                        || (args.test.contains(&target.name) && kind == AnnealTargetKind::Test)
+                };
+
+                include.then_some((target, kind))
+            })
+        })
+        .collect();
+
+    Ok(selected_artifacts)
+}
+
+/// 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: &cargo_metadata::Metadata) -> anyhow::Result<()> {
+    log::trace!("check_for_external_deps");
+    // 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 {
+        // We only care about packages that are "local" (source is None).
+        // If source is Some(...), it's from crates.io or git, which is fine
+        // (handled by Cargo).
+        if pkg.source.is_none() {
+            let pkg_path = pkg.manifest_path.as_std_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.
+            if !canonical_pkg_path.starts_with(&workspace_root) {
+                anyhow::bail!(
+                    "Unsupported external dependency: '{}' at {:?}.\n\
+                     Anneal currently only supports verifying workspaces where all local \
+                     dependencies are contained within the workspace root.",
+                    pkg.name,
+                    pkg_path
+                );
+            }
+        }
+    }
+
+    Ok(())
+}
diff --git a/anneal/v2/src/scanner.rs b/anneal/v2/src/scanner.rs
new file mode 100644
index 0000000000..a7d51f9da6
--- /dev/null
+++ b/anneal/v2/src/scanner.rs
@@ -0,0 +1,152 @@
+// Copyright 2026 The Fuchsia Authors
+//
+// Licensed under the 2-Clause BSD License <LICENSE-BSD or
+// https://opensource.org/license/bsd-2-clause>, Apache License, Version 2.0
+// <LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+// license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
+// This file may not be copied, modified, or distributed except according to
+// those terms.
+
+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,
+    /// The path to the crate's `Cargo.toml`.
+    pub manifest_path: std::path::PathBuf,
+}
+
+impl AnnealArtifact {
+    /// Returns a unique, Lean-compatible "slug" for this artifact that matches
+    /// the name that Aeneas will expect for the corresponding Lean module.
+    ///
+    /// Guarantees uniqueness based on manifest path even if multiple packages
+    /// have the same name. The slug is guaranteed to be a valid Lean
+    /// identifier (no hyphens).
+    pub fn artifact_slug(&self) -> String {
+        fn hash(data: &[u8]) -> u64 {
+            let mut hasher = sha2::Sha256::new();
+            hasher.update(data);
+            let result = hasher.finalize();
+            let mut bytes = [0u8; 8];
+            bytes.copy_from_slice(&result[0..8]);
+            u64::from_le_bytes(bytes)
+        }
+
+        // Double-hash to make sure we can distinguish between e.g.
+        // (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
+        // `DefaultHasher` doesn't guarantee stability even across runs of the
+        // same binary.
+        //
+        // `ANNEAL_HASH_WITH_REMOVED_PREFIX` allows our integration test
+        // framework to strip the randomized sandbox prefix from the manifest
+        // path before hashing, ensuring deterministic hashes even when running
+        // in a sandboxed environment.
+        let mut manifest_path_to_hash = self.manifest_path.as_path();
+        if let Ok(prefix) = std::env::var("ANNEAL_HASH_WITH_REMOVED_PREFIX") {
+            if let Ok(stripped) = self.manifest_path.strip_prefix(&prefix) {
+                manifest_path_to_hash = stripped;
+            }
+        }
+        let h0 = hash(manifest_path_to_hash.as_os_str().as_encoded_bytes());
+        let h1 = hash(self.name.target_name.as_bytes());
+        let h2 = hash(&[self.target_kind as u8]);
+        let hashes = [h0, h1, h2];
+        let h = hash(&hashes.map(u64::to_ne_bytes).concat());
+
+        // Converts kebab-case -> PascalCase.
+        // We convert both package and target names to PascalCase to ensure
+        // the generated Lean module name is a valid and idiomatic Lean
+        // identifier, matching Aeneas's output format.
+        let to_pascal = |s: &str| {
+            s.split(['-', '_'])
+                .map(|segment| {
+                    let mut chars = segment.chars();
+                    match chars.next() {
+                        None => String::new(),
+                        Some(f) => f.to_uppercase().collect::<String>() + chars.as_str(),
+                    }
+                })
+                .collect::<String>()
+        };
+
+        let pkg = to_pascal(self.name.package_name.as_str());
+        let target = to_pascal(&self.name.target_name);
+
+        // We use the hash to ensure uniqueness.
+        format!("{}{}{:08x}", pkg, target, h)
+    }
+
+    /// Returns the name of the `.llbc` file to use for this artifact.
+    pub fn llbc_file_name(&self) -> String {
+        format!("{}.llbc", self.artifact_slug())
+    }
+
+    /// Returns the name of the `.lean` spec file to use for this artifact.
+    #[allow(dead_code)]
+    pub fn lean_spec_file_name(&self) -> String {
+        format!("{}.lean", self.artifact_slug())
+    }
+
+    /// Returns the absolute path to the .llbc file.
+    ///
+    /// 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: &crate::resolve::LockedRoots) -> std::path::PathBuf {
+        roots.llbc_root().join(self.llbc_file_name())
+    }
+}
+
+/// 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,
+    mode: ScanMode,
+) -> anyhow::Result<Vec<AnnealArtifact>> {
+    let mut artifacts = Vec::new();
+    for target in &roots.roots {
+        artifacts.push(AnnealArtifact {
+            name: target.name.clone(),
+            target_kind: target.kind,
+            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)
+}
diff --git a/anneal/v2/src/setup.rs b/anneal/v2/src/setup.rs
new file mode 100644
index 0000000000..9764400ac0
--- /dev/null
+++ b/anneal/v2/src/setup.rs
@@ -0,0 +1,115 @@
+// Copyright 2026 The Fuchsia Authors
+//
+// Licensed under the 2-Clause BSD License <LICENSE-BSD or
+// https://opensource.org/license/bsd-2-clause>, Apache License, Version 2.0
+// <LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+// license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
+// This file may not be copied, modified, or distributed except according to
+// those terms.
+
+use anyhow::Context as _;
+
+pub struct SetupArgs {
+    pub local_archive: Option<std::path::PathBuf>,
+}
+
+exocrate::config! {
+    pub const CONFIG: Config = Config {
+        rel_dir_path: [".anneal", "toolchain"],
+        versioned_files: &["../Cargo.toml", "../Cargo.lock"],
+    };
+}
+
+exocrate::parse_remote_archive! {
+    pub const REMOTE: RemoteArchive = "Cargo.toml" [
+        (linux, x86_64),
+        (macos, x86_64),
+        (linux, aarch64),
+        (macos, aarch64),
+    ];
+}
+
+pub enum Tool {
+    Charon,
+}
+
+impl Tool {
+    pub fn name(&self) -> &'static str {
+        match self {
+            Self::Charon => "charon",
+        }
+    }
+
+    pub fn path(&self, toolchain: &Toolchain) -> std::path::PathBuf {
+        match self {
+            Self::Charon => toolchain.aeneas_bin_dir().join(self.name()),
+        }
+    }
+}
+
+const AENEAS_DIR: &str = "aeneas";
+const RUST_SYSROOT: &str = "rust";
+const AENEAS_BIN_DIR: &str = "bin";
+const RUST_BIN_DIR: &str = "bin";
+const RUST_LIB_DIR: &str = "lib";
+
+pub struct Toolchain {
+    root: std::path::PathBuf,
+}
+
+impl Toolchain {
+    pub fn resolve() -> anyhow::Result<Self> {
+        let location = if std::env::var("__ANNEAL_LOCAL_DEV").is_ok() {
+            exocrate::Location::LocalDev
+        } else {
+            exocrate::Location::UserGlobal
+        };
+        let root = CONFIG
+            .resolve_installation_dir(location)
+            .context("Toolchain not installed. Please run 'cargo anneal setup' first.")?;
+        Ok(Self { root })
+    }
+
+    #[allow(dead_code)]
+    pub fn root(&self) -> &std::path::Path {
+        &self.root
+    }
+
+    pub fn aeneas_bin_dir(&self) -> std::path::PathBuf {
+        self.root.join(AENEAS_DIR).join(AENEAS_BIN_DIR)
+    }
+
+    pub fn rust_sysroot(&self) -> std::path::PathBuf {
+        self.root.join(RUST_SYSROOT)
+    }
+
+    pub fn rust_bin(&self) -> std::path::PathBuf {
+        self.rust_sysroot().join(RUST_BIN_DIR)
+    }
+
+    pub fn rust_lib(&self) -> std::path::PathBuf {
+        self.rust_sysroot().join(RUST_LIB_DIR)
+    }
+
+    pub fn command(&self, tool: Tool) -> std::process::Command {
+        std::process::Command::new(tool.path(self))
+    }
+}
+
+pub fn run_setup(args: SetupArgs) -> anyhow::Result<()> {
+    let location = if std::env::var("__ANNEAL_LOCAL_DEV").is_ok() {
+        exocrate::Location::LocalDev
+    } else {
+        exocrate::Location::UserGlobal
+    };
+    let source = match args.local_archive {
+        Some(local_archive) => exocrate::Source::Local(local_archive),
+        None => exocrate::Source::Remote(REMOTE),
+    };
+
+    let installation_dir = CONFIG
+        .resolve_installation_dir_or_install(location, source)
+        .context("failed to resolve-or-install dependencies")?;
+    log::info!("anneal toolchain is installed at {:?}", installation_dir);
+    Ok(())
+}
diff --git a/anneal/v2/src/util.rs b/anneal/v2/src/util.rs
new file mode 100644
index 0000000000..230f4b475c
--- /dev/null
+++ b/anneal/v2/src/util.rs
@@ -0,0 +1,341 @@
+// Copyright 2026 The Fuchsia Authors
+//
+// Licensed under the 2-Clause BSD License <LICENSE-BSD or
+// https://opensource.org/license/bsd-2-clause>, Apache License, Version 2.0
+// <LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+// license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
+// This file may not be copied, modified, or distributed except according to
+// those terms.
+
+use std::io::BufRead as _;
+
+use anyhow::Context as _;
+use fs2::FileExt as _;
+
+/// Represents an active, exclusive lock on a directory.
+///
+/// This struct guarantees that the process holds an OS-level file lock
+/// guarding the specified directory.
+pub(crate) struct DirLock {
+    /// The path to the directory being guarded.
+    pub(crate) path: std::path::PathBuf,
+    // Kept alive to hold the flock.
+    _file: std::fs::File,
+}
+
+impl DirLock {
+    /// Acquires an exclusive lock on the specified directory.
+    ///
+    /// This function blocks until the lock can be acquired. We use a
+    /// separate `.lock` file within the directory rather than locking
+    /// 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(crate) 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))?;
+        Ok(Self { path, _file: file })
+    }
+
+    /// Acquires a shared lock on the specified directory.
+    ///
+    /// Multiple processes can hold shared locks simultaneously, but an
+    /// exclusive lock will block until all shared locks are released.
+    #[allow(dead_code)]
+    pub(crate) 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) -> anyhow::Result<std::fs::File> {
+        let lock_path = path.join(".lock");
+
+        // 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)
+            })?;
+        }
+        // If the lock file already exists, we open it in read-only mode.
+        // This prevents failures if the file is read-only (e.g., after
+        // making the toolchain directory read-only), while still allowing
+        // us to acquire shared and exclusive locks on the file descriptor.
+        if lock_path.exists() {
+            std::fs::OpenOptions::new()
+                .read(true)
+                .open(&lock_path)
+                .with_context(|| format!("Failed to open lock file at {:?}", lock_path))
+        } else {
+            std::fs::OpenOptions::new()
+                .read(true)
+                .write(true)
+                .create(true)
+                .open(&lock_path)
+                .with_context(|| format!("Failed to create lock file at {:?}", lock_path))
+        }
+    }
+}
+
+/// Walks a directory recursively and replaces string patterns inside `.trace`
+/// files. This is used to patch non-portable paths generated by Lake.
+#[allow(dead_code)]
+pub(crate) fn patch_trace_files(
+    dir: &std::path::Path,
+    replacements: &[(&str, &str)],
+) -> anyhow::Result<()> {
+    if dir.exists() {
+        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();
+            if path.is_file() && path.extension().map_or(false, |ext| ext == "trace") {
+                let content = std::fs::read_to_string(path)
+                    .with_context(|| format!("Failed to read trace file {:?}", path))?;
+                let mut new_content = content.clone();
+                for (from, to) in replacements {
+                    new_content = new_content.replace(from, to);
+                }
+                if new_content != content {
+                    std::fs::write(path, new_content)
+                        .with_context(|| format!("Failed to write trace file {:?}", path))?;
+                }
+            }
+        }
+    }
+    Ok(())
+}
+
+/// Prepends a path to an existing environment variable,
+/// separating them with a colon if the variable is not empty. This contains the
+/// pure string formatting logic.
+fn prepend_to_env_var_impl(
+    current_val: std::ffi::OsString,
+    new_path: &std::path::Path,
+) -> std::ffi::OsString {
+    let mut combined = new_path.to_path_buf().into_os_string();
+    if !current_val.is_empty() {
+        combined.push(":");
+        combined.push(current_val);
+    }
+    combined
+}
+
+/// Prepends a path to an existing environment variable in the active process
+/// environment, 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();
+    prepend_to_env_var_impl(current_val, new_path)
+}
+
+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,
+    pb: Option<indicatif::ProgressBar>,
+    mut process_stdout_line: F,
+) -> anyhow::Result<ProcessOutput>
+where
+    F: FnMut(&str, Option<&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);
+            }
+        }));
+    }
+
+    if let Some(ref p) = pb {
+        p.enable_steady_tick(std::time::Duration::from_millis(100));
+    }
+
+    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.as_ref())?;
+            if let Some(ref p) = pb {
+                p.tick();
+            }
+        }
+    }
+
+    if let Some(ref p) = pb {
+        p.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 })
+}
+
+#[cfg(feature = "exocrate_tests")]
+pub(crate) fn run_test_lock_helper(
+    role: &str,
+    lock_dir: &std::path::Path,
+    log_file: &std::path::Path,
+    sig_file: &std::path::Path,
+) -> anyhow::Result<()> {
+    use std::io::Write as _;
+
+    let append_log = |msg: &str| -> anyhow::Result<()> {
+        let mut file = std::fs::OpenOptions::new().create(true).append(true).open(log_file)?;
+        writeln!(file, "{}", msg)?;
+        Ok(())
+    };
+
+    let wait_for_sig = || -> anyhow::Result<()> {
+        let start = std::time::Instant::now();
+        while !sig_file.exists() {
+            if start.elapsed() > std::time::Duration::from_secs(3) {
+                anyhow::bail!("Timeout waiting for signal file {:?}", sig_file);
+            }
+            std::thread::sleep(std::time::Duration::from_millis(50));
+        }
+        Ok(())
+    };
+
+    match role {
+        "reader-a" => {
+            let _lock = DirLock::lock_shared(lock_dir.to_path_buf())?;
+            append_log("SHARED_START_A")?;
+            wait_for_sig()?;
+            append_log("SHARED_END_A")?;
+        }
+        "reader-b" => {
+            let _lock = DirLock::lock_shared(lock_dir.to_path_buf())?;
+            append_log("SHARED_START_B")?;
+            std::fs::write(sig_file, "")?;
+            append_log("SHARED_END_B")?;
+        }
+        "writer-a" => {
+            let _lock = DirLock::lock_exclusive(lock_dir.to_path_buf())?;
+            append_log("EXCLUSIVE_START_A")?;
+            wait_for_sig()?;
+            append_log("EXCLUSIVE_END_A")?;
+        }
+        "reader-exclusion" => {
+            std::fs::write(sig_file, "")?;
+            let _lock = DirLock::lock_shared(lock_dir.to_path_buf())?;
+            append_log("SHARED_START_B")?;
+            append_log("SHARED_END_B")?;
+        }
+        _ => anyhow::bail!("Unknown test-lock-helper role: {}", role),
+    }
+
+    Ok(())
+}
+
+#[cfg(test)]
+#[macro_export]
+macro_rules! workspace_fixture {
+    ($dir:expr, { $($path:expr => $content:expr),* $(,)? }) => {{
+        let root = $dir.path();
+        $(
+            let file_path = root.join($path);
+            if let Some(parent) = file_path.parent() {
+                std::fs::create_dir_all(parent).unwrap();
+            }
+            std::fs::write(&file_path, $content).unwrap();
+        )*
+    }};
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_prepend_to_env_var() {
+        // Test when current value is empty.
+        let path1 = std::path::Path::new("/path/one");
+        let res1 = prepend_to_env_var_impl(std::ffi::OsString::new(), path1);
+        assert_eq!(res1, "/path/one");
+
+        // Test when current value is not empty.
+        let path2 = std::path::Path::new("/path/two");
+        let res2 = prepend_to_env_var_impl(res1, path2);
+        assert_eq!(res2, "/path/two:/path/one");
+    }
+
+    #[test]
+    fn test_dir_lock_exclusive_mutual_exclusion() {
+        let temp_dir = tempfile::tempdir().unwrap();
+        let lock_path = temp_dir.path().to_path_buf();
+
+        let barrier = std::sync::Arc::new(std::sync::Barrier::new(2));
+        let barrier_clone = std::sync::Arc::clone(&barrier);
+        let lock_path_clone = lock_path.clone();
+
+        let lock_released = std::sync::Arc::new(std::sync::atomic::AtomicBool::new(false));
+        let lock_released_clone = std::sync::Arc::clone(&lock_released);
+
+        // Thread A acquires the lock.
+        let thread_a = std::thread::spawn(move || {
+            let _lock = DirLock::lock_exclusive(lock_path_clone).expect("Failed to lock exclusive");
+            barrier_clone.wait(); // Signal Thread B that A holds the lock.
+
+            // Simulate brief work holding the lock.
+            std::thread::sleep(std::time::Duration::from_millis(100));
+            lock_released_clone.store(true, std::sync::atomic::Ordering::Relaxed);
+            // _lock drops here, releasing the lock.
+        });
+
+        // Thread B waits for Thread A to acquire the lock, then tries to acquire it itself.
+        let thread_b = std::thread::spawn(move || {
+            barrier.wait(); // Wait for Thread A to acquire lock.
+
+            // Attempt to acquire lock. This should block until Thread A releases it.
+            let _lock = DirLock::lock_exclusive(lock_path).expect("Failed to lock exclusive in B");
+
+            // Assert that B only successfully locked the directory AFTER A released it.
+            assert!(
+                lock_released.load(std::sync::atomic::Ordering::Relaxed),
+                "Thread B acquired lock before Thread A released it!"
+            );
+        });
+
+        thread_a.join().unwrap();
+        thread_b.join().unwrap();
+    }
+
+    #[test]
+    fn test_dir_lock_shared_coexistence() {
+        let temp_dir = tempfile::tempdir().unwrap();
+        let lock_path = temp_dir.path().to_path_buf();
+
+        // Thread A acquires shared lock.
+        let lock_a = DirLock::lock_shared(lock_path.clone()).expect("Failed to lock shared");
+
+        // Thread B should be able to acquire shared lock immediately without blocking.
+        let lock_b = DirLock::lock_shared(lock_path).expect("Failed to lock shared concurrently");
+
+        // Both locks are held.
+        drop(lock_a);
+        drop(lock_b);
+    }
+}
diff --git a/anneal/v2/tests/integration.rs b/anneal/v2/tests/integration.rs
new file mode 100644
index 0000000000..6b6721ccf3
--- /dev/null
+++ b/anneal/v2/tests/integration.rs
@@ -0,0 +1,128 @@
+// Copyright 2026 The Fuchsia Authors
+//
+// Licensed under the 2-Clause BSD License <LICENSE-BSD or
+// https://opensource.org/license/bsd-2-clause>, Apache License, Version 2.0
+// <LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+// license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
+// This file may not be copied, modified, or distributed except according to
+// those terms.
+
+#[cfg(feature = "exocrate_tests")]
+use std::{
+    fs,
+    path::{Path, PathBuf},
+    process::Command,
+    sync::OnceLock,
+};
+
+#[cfg(feature = "exocrate_tests")]
+fn cargo_anneal_bin_path() -> PathBuf {
+    std::env::var("CARGO_BIN_EXE_cargo-anneal")
+        .or_else(|_| std::env::var("CARGO_BIN_EXE_cargo_anneal"))
+        .expect("CARGO_BIN_EXE_* not set")
+        .into()
+}
+
+#[cfg(feature = "exocrate_tests")]
+fn ensure_test_toolchain(bin_path: &Path) {
+    static SETUP_RESULT: OnceLock<Result<(), String>> = OnceLock::new();
+
+    let result = SETUP_RESULT.get_or_init(|| {
+        let manifest_dir = Path::new(env!("CARGO_MANIFEST_DIR"));
+        let output = Command::new(bin_path)
+            .arg("setup")
+            .arg("--local-archive")
+            .arg(manifest_dir.join("target/anneal-exocrate.tar.zst"))
+            .env("__ANNEAL_LOCAL_DEV", "1")
+            .env("CARGO_MANIFEST_DIR", manifest_dir)
+            .output()
+            .map_err(|err| format!("failed to execute cargo-anneal setup: {err}"))?;
+
+        if output.status.success() {
+            return Ok(());
+        }
+
+        Err(format!(
+            "cargo-anneal setup failed\nstdout: {}\nstderr: {}",
+            String::from_utf8_lossy(&output.stdout),
+            String::from_utf8_lossy(&output.stderr)
+        ))
+    });
+
+    if let Err(err) = result {
+        panic!("{err}");
+    }
+}
+
+#[cfg(feature = "exocrate_tests")]
+#[test]
+fn test_expand_subcommand_simple() {
+    let temp_dir = tempfile::tempdir().unwrap();
+    let project_dir = temp_dir.path().join("project");
+    let output_dir = temp_dir.path().join("llbc_out");
+    fs::create_dir_all(project_dir.join("examples")).unwrap();
+    fs::write(
+        project_dir.join("Cargo.toml"),
+        r#"
+            [package]
+            name = "test_proj"
+            version = "0.1.0"
+            edition = "2021"
+
+            [[example]]
+            name = "simple"
+            path = "examples/simple.rs"
+        "#,
+    )
+    .unwrap();
+    fs::write(
+        project_dir.join("examples").join("simple.rs"),
+        r#"
+            pub fn add(left: usize, right: usize) -> usize {
+                left + right
+            }
+
+            fn main() {
+                println!("Hello, world! {}", add(1, 2));
+            }
+        "#,
+    )
+    .unwrap();
+
+    let bin_path = cargo_anneal_bin_path();
+    ensure_test_toolchain(&bin_path);
+
+    let mut cmd = Command::new(bin_path);
+    cmd.arg("expand")
+        .arg("--manifest-path")
+        .arg(project_dir.join("Cargo.toml"))
+        .arg("--example")
+        .arg("simple")
+        .arg("--output-dir")
+        .arg(&output_dir);
+    cmd.arg("--no-progress");
+
+    cmd.env("__ANNEAL_LOCAL_DEV", "1");
+    cmd.env("CARGO_MANIFEST_DIR", env!("CARGO_MANIFEST_DIR"));
+
+    let output = cmd.output().expect("failed to execute cargo-anneal");
+
+    println!("stdout: {}", String::from_utf8_lossy(&output.stdout));
+    println!("stderr: {}", String::from_utf8_lossy(&output.stderr));
+
+    assert!(output.status.success(), "cargo-anneal failed");
+
+    let mut found_llbc = false;
+    if output_dir.exists() {
+        for entry in fs::read_dir(&output_dir).unwrap() {
+            let entry = entry.unwrap();
+            let path = entry.path();
+            if path.is_file() && path.extension().map_or(false, |ext| ext == "llbc") {
+                found_llbc = true;
+                break;
+            }
+        }
+    }
+
+    assert!(found_llbc, "No .llbc file found in output directory {:?}", output_dir);
+}
diff --git a/anneal/v2/tests/lock_integration.rs b/anneal/v2/tests/lock_integration.rs
new file mode 100644
index 0000000000..e4d1ce5fdb
--- /dev/null
+++ b/anneal/v2/tests/lock_integration.rs
@@ -0,0 +1,163 @@
+// Copyright 2026 The Fuchsia Authors
+//
+// Licensed under the 2-Clause BSD License <LICENSE-BSD or
+// https://opensource.org/license/bsd-2-clause>, Apache License, Version 2.0
+// <LICENSE-APACHE or https://www.apache.org/licenses/LICENSE-2.0>, or the MIT
+// license <LICENSE-MIT or https://opensource.org/licenses/MIT>, at your option.
+// This file may not be copied, modified, or distributed except according to
+// those terms.
+
+#![cfg(feature = "exocrate_tests")]
+
+use std::{fs, process::Command};
+
+fn wait_with_timeout(
+    child: &mut std::process::Child,
+    timeout: std::time::Duration,
+) -> anyhow::Result<std::process::ExitStatus> {
+    let start = std::time::Instant::now();
+    loop {
+        if let Some(status) = child.try_wait()? {
+            return Ok(status);
+        }
+        if start.elapsed() > timeout {
+            child.kill()?;
+            anyhow::bail!("Child process timed out after {:?}", timeout);
+        }
+        std::thread::sleep(std::time::Duration::from_millis(50));
+    }
+}
+
+#[test]
+fn test_dir_lock_coexistence_integration() {
+    let temp_dir = tempfile::tempdir().unwrap();
+    let lock_dir = temp_dir.path().join("lock_dir");
+    let log_file = temp_dir.path().join("concurrency_log.txt");
+    let sig_file = temp_dir.path().join("sig_b_active.tmp");
+
+    let bin_path = std::env::var("CARGO_BIN_EXE_cargo-anneal")
+        .or_else(|_| std::env::var("CARGO_BIN_EXE_cargo_anneal"))
+        .expect("CARGO_BIN_EXE_* not set");
+
+    // 1. Spawn Reader A
+    let mut child_a = Command::new(&bin_path)
+        .arg("test-lock-helper")
+        .arg("--role")
+        .arg("reader-a")
+        .arg("--lock-dir")
+        .arg(&lock_dir)
+        .arg("--log-file")
+        .arg(&log_file)
+        .arg("--sig-file")
+        .arg(&sig_file)
+        .spawn()
+        .expect("failed to spawn reader-a");
+
+    // Give A a tiny bit of time to acquire the lock.
+    std::thread::sleep(std::time::Duration::from_millis(100));
+
+    // 2. Spawn Reader B
+    let mut child_b = Command::new(&bin_path)
+        .arg("test-lock-helper")
+        .arg("--role")
+        .arg("reader-b")
+        .arg("--lock-dir")
+        .arg(&lock_dir)
+        .arg("--log-file")
+        .arg(&log_file)
+        .arg("--sig-file")
+        .arg(&sig_file)
+        .spawn()
+        .expect("failed to spawn reader-b");
+
+    // 3. Wait for both with a strict timeout.
+    let status_a = wait_with_timeout(&mut child_a, std::time::Duration::from_secs(5))
+        .expect("Reader A failed or timed out");
+    let status_b = wait_with_timeout(&mut child_b, std::time::Duration::from_secs(5))
+        .expect("Reader B failed or timed out");
+
+    assert!(status_a.success(), "Reader A exited with failure");
+    assert!(status_b.success(), "Reader B exited with failure");
+
+    // 4. Read trace and assert overlap.
+    let trace = fs::read_to_string(&log_file).expect("failed to read log");
+    let lines: Vec<&str> = trace.lines().collect();
+    assert_eq!(lines.len(), 4, "Expected exactly 4 log lines");
+
+    // Expected overlap trace:
+    // SHARED_START_A
+    // SHARED_START_B
+    // SHARED_END_B
+    // SHARED_END_A
+    assert_eq!(lines[0], "SHARED_START_A");
+    assert_eq!(lines[1], "SHARED_START_B");
+    assert_eq!(lines[2], "SHARED_END_B");
+    assert_eq!(lines[3], "SHARED_END_A");
+}
+
+#[test]
+fn test_dir_lock_exclusion_integration() {
+    let temp_dir = tempfile::tempdir().unwrap();
+    let lock_dir = temp_dir.path().join("lock_dir");
+    let log_file = temp_dir.path().join("concurrency_log.txt");
+    let sig_file = temp_dir.path().join("sig_b_attempt.tmp");
+
+    let bin_path = std::env::var("CARGO_BIN_EXE_cargo-anneal")
+        .or_else(|_| std::env::var("CARGO_BIN_EXE_cargo_anneal"))
+        .expect("CARGO_BIN_EXE_* not set");
+
+    // 1. Spawn Writer A
+    let mut child_a = Command::new(&bin_path)
+        .arg("test-lock-helper")
+        .arg("--role")
+        .arg("writer-a")
+        .arg("--lock-dir")
+        .arg(&lock_dir)
+        .arg("--log-file")
+        .arg(&log_file)
+        .arg("--sig-file")
+        .arg(&sig_file)
+        .spawn()
+        .expect("failed to spawn writer-a");
+
+    // Give A a tiny bit of time to acquire the lock.
+    std::thread::sleep(std::time::Duration::from_millis(100));
+
+    // 2. Spawn Reader B
+    let mut child_b = Command::new(&bin_path)
+        .arg("test-lock-helper")
+        .arg("--role")
+        .arg("reader-exclusion")
+        .arg("--lock-dir")
+        .arg(&lock_dir)
+        .arg("--log-file")
+        .arg(&log_file)
+        .arg("--sig-file")
+        .arg(&sig_file)
+        .spawn()
+        .expect("failed to spawn reader-exclusion");
+
+    // 3. Wait for both with a strict timeout.
+    let status_a = wait_with_timeout(&mut child_a, std::time::Duration::from_secs(5))
+        .expect("Writer A failed or timed out");
+    let status_b = wait_with_timeout(&mut child_b, std::time::Duration::from_secs(5))
+        .expect("Reader B failed or timed out");
+
+    assert!(status_a.success(), "Writer A exited with failure");
+    assert!(status_b.success(), "Reader B exited with failure");
+
+    // 4. Read trace and assert exclusion.
+    let trace = fs::read_to_string(&log_file).expect("failed to read log");
+    let lines: Vec<&str> = trace.lines().collect();
+    assert_eq!(lines.len(), 4, "Expected exactly 4 log lines");
+
+    // Expected sequential trace (since A blocks B):
+    // EXCLUSIVE_START_A
+    // EXCLUSIVE_END_A
+    // SHARED_START_B
+    // SHARED_END_B
+    assert_eq!(lines[0], "EXCLUSIVE_START_A");
+    assert_eq!(lines[1], "EXCLUSIVE_END_A");
+    assert_eq!(lines[2], "SHARED_START_B");
+    assert_eq!(lines[3], "SHARED_END_B");
+}
diff --git a/exocrate/src/lib.rs b/exocrate/src/lib.rs
index 17f0eb441b..cb485a89ee 100644
--- a/exocrate/src/lib.rs
+++ b/exocrate/src/lib.rs
@@ -186,6 +186,29 @@ pub enum Source {
     Local(PathBuf),
 }
 
+/// Paths passed to an installation fixup hook.
+///
+/// The staging directory is the mutable, freshly extracted archive directory.
+/// The final directory is the stable path where the staging directory will be
+/// atomically published after the hook returns successfully.
+#[derive(Clone, Copy)]
+pub struct FixupPaths<'a> {
+    staging_dir: &'a Path,
+    final_dir: &'a Path,
+}
+
+impl<'a> FixupPaths<'a> {
+    /// The mutable directory containing freshly extracted archive contents.
+    pub fn staging_dir(&self) -> &'a Path {
+        self.staging_dir
+    }
+
+    /// The stable installation path that will exist after publication.
+    pub fn final_dir(&self) -> &'a Path {
+        self.final_dir
+    }
+}
+
 impl Config {
     /// Resolves the dependency directory, failing if it doesn't exist.
     pub fn resolve_installation_dir(&self, location: Location) -> IoResult<PathBuf> {
@@ -199,13 +222,29 @@ impl Config {
         &self,
         location: Location,
         source: Source,
+    ) -> IoResult<PathBuf> {
+        self.resolve_installation_dir_or_install_with_fixup(location, source, |_| Ok(()))
+    }
+
+    /// Resolves the dependency directory, installing and fixing it up if needed.
+    ///
+    /// The `fixup` hook runs once after a fresh archive extraction, but before
+    /// the managed directory is published. Mutate files through
+    /// [`FixupPaths::staging_dir`]; use [`FixupPaths::final_dir`] only for
+    /// fixups that need to write stable install-root references into those
+    /// staged files.
+    pub fn resolve_installation_dir_or_install_with_fixup(
+        &self,
+        location: Location,
+        source: Source,
+        fixup: impl FnOnce(FixupPaths<'_>) -> IoResult<()>,
     ) -> IoResult<PathBuf> {
         let dir_path = self.dir_path(location);
         if ManagedDirName::new(&dir_path).check_exists().is_ok() {
             return Ok(dir_path);
         }
         let (reader, expected_sha) = self.open_source(source)?;
-        install(reader, &dir_path, expected_sha)?;
+        install_with_fixup(reader, &dir_path, expected_sha, fixup)?;
         Ok(dir_path)
     }
 
@@ -268,7 +307,17 @@ impl Config {
 
 /// Extracts the `.tar.zst` from `reader` and installs it at `dst`, optionally
 /// validating its hash.
+#[cfg(test)]
 fn install(mut reader: impl Read, dst: &Path, expected_sha256: Option<[u8; 32]>) -> IoResult<()> {
+    install_with_fixup(&mut reader, dst, expected_sha256, |_| Ok(()))
+}
+
+fn install_with_fixup(
+    mut reader: impl Read,
+    dst: &Path,
+    expected_sha256: Option<[u8; 32]>,
+    fixup: impl FnOnce(FixupPaths<'_>) -> IoResult<()>,
+) -> IoResult<()> {
     struct HashingReader<R> {
         reader: R,
         hasher: sha2::Sha256,
@@ -282,14 +331,20 @@ fn install(mut reader: impl Read, dst: &Path, expected_sha256: Option<[u8; 32]>)
         }
     }
 
-    sync::ManagedDirName::new(dst)
-        .check_exists_or_create(|target_dir| {
+    fn unpack_tar_zst(reader: impl Read, target_dir: &Path) -> IoResult<()> {
+        let decoder = zstd::stream::read::Decoder::new(reader)?;
+        let mut archive = tar::Archive::new(decoder);
+        archive.set_mask(0);
+        archive.set_preserve_permissions(true);
+        archive.unpack(target_dir)
+    }
+
+    let (_dir, _created) =
+        sync::ManagedDirName::new(dst).check_exists_or_create_with_status(|target_dir| {
             if let Some(expected) = expected_sha256 {
                 let mut hash_reader = HashingReader { reader, hasher: sha2::Sha256::new() };
                 {
-                    let decoder = zstd::stream::read::Decoder::new(&mut hash_reader)?;
-                    let mut archive = tar::Archive::new(decoder);
-                    archive.unpack(target_dir)?;
+                    unpack_tar_zst(&mut hash_reader, target_dir)?;
                 }
 
                 // Ensure any remaining trailing bytes in the stream are read
@@ -308,13 +363,13 @@ fn install(mut reader: impl Read, dst: &Path, expected_sha256: Option<[u8; 32]>)
                     ));
                 }
             } else {
-                let decoder = zstd::stream::read::Decoder::new(&mut reader)?;
-                let mut archive = tar::Archive::new(decoder);
-                archive.unpack(target_dir)?;
+                unpack_tar_zst(&mut reader, target_dir)?;
             }
+            fixup(FixupPaths { staging_dir: target_dir, final_dir: dst })?;
             Ok(())
-        })
-        .map(|_| ())
+        })?;
+
+    Ok(())
 }
 
 /// Parses a [`RemoteArchive`] from the `Cargo.toml` at `$cargo_toml_path`.
@@ -545,13 +600,19 @@ mod tests {
     use super::*;
 
     fn create_dummy_tar_zst(files: &[(&str, &[u8])]) -> Vec<u8> {
+        let files =
+            files.iter().map(|(name, content)| (*name, *content, 0o644)).collect::<Vec<_>>();
+        create_dummy_tar_zst_with_modes(&files)
+    }
+
+    fn create_dummy_tar_zst_with_modes(files: &[(&str, &[u8], u32)]) -> Vec<u8> {
         let mut zstd_enc = zstd::stream::write::Encoder::new(Vec::new(), 0).unwrap();
         {
             let mut tar_builder = tar::Builder::new(&mut zstd_enc);
-            for (name, content) in files {
+            for (name, content, mode) in files {
                 let mut header = tar::Header::new_gnu();
                 header.set_size(content.len() as u64);
-                header.set_mode(0o644);
+                header.set_mode(*mode);
                 header.set_cksum();
                 tar_builder.append_data(&mut header, name, *content).unwrap();
             }
@@ -595,6 +656,82 @@ mod tests {
         assert_eq!(fs::read(dst.join("nested/dir/data.bin")).unwrap(), b"\x01\x02\x03");
     }
 
+    #[test]
+    fn test_install_with_fixup() {
+        let temp = tempfile::tempdir().unwrap();
+        let dst = temp.path().join("install_target");
+        let tar_zst = create_dummy_tar_zst(&[("hello.txt", b"hello world")]);
+
+        install_with_fixup(tar_zst.as_slice(), &dst, None, |paths| {
+            assert_ne!(paths.staging_dir(), paths.final_dir());
+            assert!(
+                !paths.final_dir().exists(),
+                "final directory should not be visible until fixup completes"
+            );
+            fs::write(paths.staging_dir().join("fixed.txt"), "fixed")
+        })
+        .unwrap();
+
+        assert_eq!(fs::read_to_string(dst.join("hello.txt")).unwrap(), "hello world");
+        assert_eq!(fs::read_to_string(dst.join("fixed.txt")).unwrap(), "fixed");
+    }
+
+    #[test]
+    fn test_install_fixup_not_rerun_for_existing_dir() {
+        let temp = tempfile::tempdir().unwrap();
+        let dst = temp.path().join("install_target");
+        fs::create_dir_all(&dst).unwrap();
+        fs::write(dst.join("existing.txt"), "existing content").unwrap();
+
+        let bad_data = b"invalid archive data";
+        install_with_fixup(&bad_data[..], &dst, None, |_| {
+            panic!("fixup should not run for an existing installation");
+        })
+        .unwrap();
+
+        assert_eq!(fs::read_to_string(dst.join("existing.txt")).unwrap(), "existing content");
+    }
+
+    #[test]
+    fn test_install_fixup_failure_removes_installation() {
+        let temp = tempfile::tempdir().unwrap();
+        let dst = temp.path().join("install_target");
+        let tar_zst = create_dummy_tar_zst(&[("hello.txt", b"hello world")]);
+
+        let result = install_with_fixup(tar_zst.as_slice(), &dst, None, |_| {
+            Err(std::io::Error::new(std::io::ErrorKind::Other, "fixup failed"))
+        });
+
+        assert!(result.is_err());
+        assert!(!dst.exists());
+        let entries: Vec<_> = fs::read_dir(temp.path())
+            .unwrap()
+            .map(|e| e.unwrap().file_name())
+            .filter(|n| n != "install_target.lock")
+            .collect();
+        assert!(entries.is_empty());
+    }
+
+    #[cfg(unix)]
+    #[test]
+    fn test_install_preserves_read_only_permissions() {
+        use std::os::unix::fs::PermissionsExt as _;
+
+        let temp = tempfile::tempdir().unwrap();
+        let dst = temp.path().join("install_target");
+        let tar_zst = create_dummy_tar_zst_with_modes(&[
+            ("readonly.txt", b"locked", 0o444),
+            ("bin/tool", b"tool", 0o555),
+        ]);
+
+        install(tar_zst.as_slice(), &dst, None).unwrap();
+
+        let readonly_mode = fs::metadata(dst.join("readonly.txt")).unwrap().permissions().mode();
+        let tool_mode = fs::metadata(dst.join("bin/tool")).unwrap().permissions().mode();
+        assert_eq!(readonly_mode & 0o777, 0o444);
+        assert_eq!(tool_mode & 0o777, 0o555);
+    }
+
     #[test]
     fn test_install_without_hash_validation() {
         let temp = tempfile::tempdir().unwrap();
diff --git a/exocrate/src/sync.rs b/exocrate/src/sync.rs
index 85b6e20352..0f213706ff 100644
--- a/exocrate/src/sync.rs
+++ b/exocrate/src/sync.rs
@@ -66,12 +66,20 @@ impl<'a> ManagedDirName<'a> {
     ///
     /// `check_exists_or_create` is **not** concurrency-safe if multiple
     /// concurrent calls are made *from the same process*.
+    #[cfg(test)]
     pub(crate) fn check_exists_or_create(
         self,
         populate: impl FnOnce(&Path) -> IoResult<()>,
     ) -> IoResult<ManagedDir<'a>> {
+        self.check_exists_or_create_with_status(populate).map(|(dir, _created)| dir)
+    }
+
+    pub(crate) fn check_exists_or_create_with_status(
+        self,
+        populate: impl FnOnce(&Path) -> IoResult<()>,
+    ) -> IoResult<(ManagedDir<'a>, bool)> {
         if let Ok(dir) = self.check_exists() {
-            return Ok(dir);
+            return Ok((dir, false));
         }
 
         if let Some(parent) = self.path.parent() {
@@ -117,7 +125,7 @@ impl<'a> ManagedDirName<'a> {
         // another process populated the directory.
         if let Ok(dir) = self.check_exists() {
             guard.completed = true;
-            return Ok(dir);
+            return Ok((dir, false));
         }
 
         // Clean up from any previous failed attempt to populate the directory.
@@ -142,7 +150,7 @@ impl<'a> ManagedDirName<'a> {
         })?;
 
         guard.completed = true;
-        Ok(ManagedDir { path: self.path })
+        Ok((ManagedDir { path: self.path }, true))
     }
 
     fn staging(&self) -> PathBuf {