diff --git a/anneal/Cargo.lock b/anneal/Cargo.lock
index ae6af54417..71f5b81087 100644
--- a/anneal/Cargo.lock
+++ b/anneal/Cargo.lock
@@ -219,7 +219,7 @@ dependencies = [
 
 [[package]]
 name = "cargo-anneal"
-version = "0.1.0-alpha.15"
+version = "0.1.0-alpha.16"
 dependencies = [
  "anyhow",
  "assert_cmd",
diff --git a/anneal/Cargo.toml b/anneal/Cargo.toml
index 29effaf1be..20655a010c 100644
--- a/anneal/Cargo.toml
+++ b/anneal/Cargo.toml
@@ -4,7 +4,7 @@ members = [".", "tools/doc_gen"]
 [package]
 name = "cargo-anneal"
 edition = "2024"
-version = "0.1.0-alpha.15"
+version = "0.1.0-alpha.16"
 description = "Formally verify that your safety comments are correct."
 categories = [
   "development-tools::cargo-plugins",
@@ -84,7 +84,7 @@ similar = "2.7.0"
 #
 # FIXME: Add a CI step to verify that this commit exists and matches the
 # toolchain version.
-aeneas_rev = "42c0e90dacf486f7d3ed5b6cde3a9a81f04915a4"
+aeneas_rev = "d1c3c2677f6a052133a2cf12314cebe6ce9279cc"
 
 # The Lean toolchain version to use. This must match the version of Lean used
 # by Aeneas in the `lean-toolchain` file in the commit above.
@@ -112,22 +112,22 @@ charon_rust_toolchain = "nightly-2026-02-07"
 
 [package.metadata.anneal.dependencies.aeneas]
 # The per-commit release tag from AeneasVerif/charon
-tag = "build-2026.04.07.112215-42c0e90dacf486f7d3ed5b6cde3a9a81f04915a4"
+tag = "build-2026.04.14.134747-d1c3c2677f6a052133a2cf12314cebe6ce9279cc"
 
 [package.metadata.anneal.dependencies.aeneas.checksums]
-linux-aarch64 = "a250ef38be509f69ff4c5fb35eded165255fae6f659172837cd3053978de863f"
+linux-aarch64 = "e739cbb93145a926c1fb1cf03127f18d5dbfb78b4c4c5e3d4d482501251f8d88"
 linux-aarch64-aeneas = "fca0dedece748b406f180341ba83d764eb7b2bf5f11fbb54668fc26609a3032d"
 linux-aarch64-charon = "471883ad31629b569e727e256e4f5ab2c1726bfb3060cb6585037c7088062ed3"
 linux-aarch64-charon-driver = "df2622bb873ae9d10b25294b291cbc07bca32c26554c4f825f3a6d2f094cdbe4"
-linux-x86_64 = "a448682a154590e65b0794c42487583352375fc04bdd6b2418324f6ecafcc94f"
+linux-x86_64 = "b6af446d501dd7c4291316eca332d13be41fb0820cb821d2a5d99bd08aff6782"
 linux-x86_64-aeneas = "306d908964df4e54bfc57b2fc3d88809eace9e77ac639adf5c0f0d5a8574397e"
 linux-x86_64-charon = "bcdc1ef536f863f21367973bd639e5557d36872cd9135d4b13ff84c2bc6df836"
 linux-x86_64-charon-driver = "20379b2051dd51dbea8d720e4041d55afe9241b95ab911e3b06492110450ecd0"
-macos-aarch64 = "1dbeaafe875bec173e0d2cf3c6bbfa63d6c591d3ec554bafb0d2c3c52e1ded6d"
+macos-aarch64 = "0d3402d3ff07b75abc4fc5515184aa654805b3b61cf908f39daf767cece37704"
 macos-aarch64-aeneas = "f85db47ef602108c727bfac23d1e27fb52d4fb1010b0f55ffb748da65fb0a1b6"
 macos-aarch64-charon = "6510ace82180cd78875b0631638a200d8e55bc9090c9372ea1dc8eb08511b6fb"
 macos-aarch64-charon-driver = "3c11fcb6c5cd65cd14d9747c7f8ddd1522b608a1e79041c907cb79d3118054b2"
-macos-x86_64 = "e977c28b72ec041d4f13df0acc77ab59040743a9659b4eefffb71eb420cd5df6"
+macos-x86_64 = "c0434a49fee1de1a4ad3dd66c69b741ef5ad534ead66839d7ea852fe8e1902c3"
 macos-x86_64-aeneas = "ceb3d8ee898f941861efb1545537681e0f4419f332482468e520621a809cb09e"
 macos-x86_64-charon = "926c5ff8495c19b7a6f3aff1a3861970bae11bd374cf114ac3924a27bcae9ee7"
 macos-x86_64-charon-driver = "03e6617fe122f29111bf16538a5ba8f0beac6698ce473d99069439d30fa552e8"
diff --git a/anneal/README.md b/anneal/README.md
index 2b0f033050..08d1e04b3f 100644
--- a/anneal/README.md
+++ b/anneal/README.md
@@ -97,7 +97,7 @@ impl std::ops::Div<PositiveUsize> for usize {
 Install Anneal and its required toolchains (Charon and Aeneas):
 
 ```bash
-cargo install cargo-anneal@0.1.0-alpha.15
+cargo install cargo-anneal@0.1.0-alpha.16
 cargo anneal setup
 ```
 
diff --git a/anneal/testdata/setup/aeneas-linux-aarch64.tar.gz b/anneal/testdata/setup/aeneas-linux-aarch64.tar.gz
index 98b74c81f7..6a38dc5482 100644
Binary files a/anneal/testdata/setup/aeneas-linux-aarch64.tar.gz and b/anneal/testdata/setup/aeneas-linux-aarch64.tar.gz differ
diff --git a/anneal/testdata/setup/aeneas-linux-x86_64.tar.gz b/anneal/testdata/setup/aeneas-linux-x86_64.tar.gz
index 7cb0da992e..95c457d780 100644
Binary files a/anneal/testdata/setup/aeneas-linux-x86_64.tar.gz and b/anneal/testdata/setup/aeneas-linux-x86_64.tar.gz differ
diff --git a/anneal/testdata/setup/aeneas-macos-aarch64.tar.gz b/anneal/testdata/setup/aeneas-macos-aarch64.tar.gz
index 322cdf500e..1a9a8a0029 100644
Binary files a/anneal/testdata/setup/aeneas-macos-aarch64.tar.gz and b/anneal/testdata/setup/aeneas-macos-aarch64.tar.gz differ
diff --git a/anneal/testdata/setup/aeneas-macos-x86_64.tar.gz b/anneal/testdata/setup/aeneas-macos-x86_64.tar.gz
index 5dd9e14c0d..b35f4fa1f1 100644
Binary files a/anneal/testdata/setup/aeneas-macos-x86_64.tar.gz and b/anneal/testdata/setup/aeneas-macos-x86_64.tar.gz differ
diff --git a/anneal/tests/fixtures/setup_e2e/expected.stdout b/anneal/tests/fixtures/setup_e2e/expected.stdout
index dbbc9d579f..346b3559db 100644
--- a/anneal/tests/fixtures/setup_e2e/expected.stdout
+++ b/anneal/tests/fixtures/setup_e2e/expected.stdout
@@ -2,5 +2,5 @@ Checking for elan...
 elan is already installed.
 Installing Lean toolchain leanprover/lean4:v4.28.0-rc1...
 Lean toolchain leanprover/lean4:v4.28.0-rc1 is already installed.
-Downloading: http://127.0.0.1:<PORT>/build-2026.04.07.112215-42c0e90dacf486f7d3ed5b6cde3a9a81f04915a4/aeneas-linux-x86_64.tar.gz
-Successfully installed toolchain vbuild-2026.04.07.112215-42c0e90dacf486f7d3ed5b6cde3a9a81f04915a4
+Downloading: http://127.0.0.1:<PORT>/build-2026.04.14.134747-d1c3c2677f6a052133a2cf12314cebe6ce9279cc/aeneas-linux-x86_64.tar.gz
+Successfully installed toolchain vbuild-2026.04.14.134747-d1c3c2677f6a052133a2cf12314cebe6ce9279cc
diff --git a/anneal/tests/integration.rs b/anneal/tests/integration.rs
index cdbef9e14b..7574f78e3b 100644
--- a/anneal/tests/integration.rs
+++ b/anneal/tests/integration.rs
@@ -869,6 +869,16 @@ fn smart_clone_cache(source: &Path, target: &Path) -> io::Result<()> {
                 perms.set_readonly(false);
                 fs::set_permissions(&target_path, perms)?;
             } else {
+                // Make sure the source file is read-only to prevent accidental modification
+                // through symlinks!
+                if let Ok(metadata) = fs::metadata(source_path) {
+                    let mut perms = metadata.permissions();
+                    if !perms.readonly() {
+                        perms.set_readonly(true);
+                        fs::set_permissions(source_path, perms)
+                            .expect("Failed to set permissions to read-only");
+                    }
+                }
                 // NOTE: It is crucial that we *don't* provide a deep-copy
                 // fallback path here. The symlinked files consume a huge amount
                 // of disk space. Deep copying instead would consume many times