diff --git a/.github/workflows/hermes.yml b/.github/workflows/hermes.yml
index 6ec1d24dcc..07f2af65b3 100644
--- a/.github/workflows/hermes.yml
+++ b/.github/workflows/hermes.yml
@@ -28,7 +28,7 @@ env:
 jobs:
   hermes_tests:
     name: Hermes Tests
-    runs-on: ubuntu-latest
+    runs-on: ubuntu-24.04-64core
     steps:
       - uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
         with:
@@ -49,7 +49,7 @@ jobs:
         run: |
           set -eo pipefail
           CHARON_TOOLCHAIN="$(cargo metadata --no-deps --format-version 1 \
-            | jq -r '.packages[] | select(.name == "cargo-hermes") | .metadata.hermes.dependencies.charon.rust_toolchain')"
+            | jq -r '.packages[] | select(.name == "cargo-hermes") | .metadata.build_rs.charon_rust_toolchain')"
           rustup toolchain install "$CHARON_TOOLCHAIN"
 
       - name: Install elan (Lean toolchain manager)
diff --git a/tools/hermes/Cargo.toml b/tools/hermes/Cargo.toml
index f51129f53f..34d82a11bb 100644
--- a/tools/hermes/Cargo.toml
+++ b/tools/hermes/Cargo.toml
@@ -69,13 +69,13 @@ regex.workspace = true
 strip-ansi-escapes = "0.2.1"
 similar = "2.7.0"
 
-[package.metadata.build-rs]
+[package.metadata.build_rs]
 
 # The commit hash of the Aeneas repository to use.
 #
 # FIXME: Add a CI step to verify that this commit exists and matches the
 # toolchain version.
-aeneas_rev = "5918d4719139b5e5ae6e7b63f584b036620b41b7"
+aeneas_rev = "1180be60c7a0e642cb442bfe90fe5cd8c1bb853f"
 
 # 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.
@@ -94,27 +94,31 @@ lean_toolchain = "leanprover/lean4:v4.28.0-rc1"
 # version/commit ID once that's supported
 charon_version = "0.1.174"
 
+# The Rust toolchain required by Charon.
+#
+# FIXME(#3165):
+# - Roll this from `tools/roll-pinned-prebuilts.py`
+# - Auto-install via `rustup` during `cargo hermes setup`
+charon_rust_toolchain = "nightly-2026-02-07"
+
 [package.metadata.hermes.dependencies.aeneas]
 # The per-commit release tag from AeneasVerif/charon
-tag = "build-2026.03.24.085418-5918d4719139b5e5ae6e7b63f584b036620b41b7"
+tag = "build-2026.03.29.102514-1180be60c7a0e642cb442bfe90fe5cd8c1bb853f"
 
 [package.metadata.hermes.dependencies.aeneas.checksums]
-linux-x86_64 = "fd706bf0f39701953d9d8734e9b0a9b8a6c9e71111006d093516748974a0d09a"
-linux-x86_64-aeneas = "1ed68728e18299ba961bc76c0c4897e582fdcfe30ec9b01919e250dc3cb6e65d"
+linux-x86_64 = "8224c76225329c8852e5a8cacf21fee9dc8bf93141a2a9a6ee2a52e3cfc2213f"
+linux-x86_64-aeneas = "0efc2c1c2f695e8e8fc268e6d3aaa20b7bf0a52790250f6ac45dd5f261d52a82"
 linux-x86_64-charon = "bcdc1ef536f863f21367973bd639e5557d36872cd9135d4b13ff84c2bc6df836"
 linux-x86_64-charon-driver = "20379b2051dd51dbea8d720e4041d55afe9241b95ab911e3b06492110450ecd0"
-macos-aarch64 = "d8284bf025cb768aa24cf49bdb66d6723f3c266d9ac95870bd5099d7db677e64"
-macos-aarch64-aeneas = "85f9bbda808c764095fae086e35214e485f40e4c9666f6b84916481e5c7263f8"
+macos-aarch64 = "7a5e9ded37dd21b288dffc68686ea4d254864c7a6b58a49d0bddab44d721114e"
+macos-aarch64-aeneas = "079a6565a1b5ec142548e50cc32db25ce05ae9ee97ee7148da2cb80d7286bd4e"
 macos-aarch64-charon = "6510ace82180cd78875b0631638a200d8e55bc9090c9372ea1dc8eb08511b6fb"
 macos-aarch64-charon-driver = "3c11fcb6c5cd65cd14d9747c7f8ddd1522b608a1e79041c907cb79d3118054b2"
-macos-x86_64 = "72ab5f3a22f7e666acd4c954600f4d963e34e22b900f222ce26b267939a0b4d2"
-macos-x86_64-aeneas = "72a9078abeb9c989f07da25a7f541f01e0ad62214a9475e27d24cf58ebd8a740"
+macos-x86_64 = "a909c3aa7813dd5f32b481d0c96e2b5ea3a729fa1898470b993055e778576459"
+macos-x86_64-aeneas = "7a001aa2b9f786a3978a25a68291dd0f56c0c4f069b59b782f7fb84ab206a49e"
 macos-x86_64-charon = "926c5ff8495c19b7a6f3aff1a3861970bae11bd374cf114ac3924a27bcae9ee7"
 macos-x86_64-charon-driver = "03e6617fe122f29111bf16538a5ba8f0beac6698ce473d99069439d30fa552e8"
 
-[package.metadata.hermes.dependencies.charon]
-rust_toolchain = "nightly-2025-01-26"
-
 [[test]]
 name = "integration"
 harness = false
diff --git a/tools/hermes/build.rs b/tools/hermes/build.rs
index 236131ab31..d19dc5e281 100644
--- a/tools/hermes/build.rs
+++ b/tools/hermes/build.rs
@@ -17,18 +17,19 @@ fn main() {
     let cargo_toml: toml::Value =
         toml::from_str(&cargo_toml_content).expect("failed to parse Cargo.toml");
 
-    // We expect the metadata to be under `[package.metadata.build-rs]`.
+    // We expect the metadata to be under `[package.metadata.build_rs]`.
     let build_rs_metadata = cargo_toml
         .get("package")
         .and_then(|p| p.get("metadata"))
-        .and_then(|m| m.get("build-rs"))
-        .expect("Cargo.toml must have [package.metadata.build-rs] section");
+        .and_then(|m| m.get("build_rs"))
+        .expect("Cargo.toml must have [package.metadata.build_rs] section");
 
     // Key in `Cargo.toml` -> Environment variable name
     let vars = [
         ("aeneas_rev", "HERMES_AENEAS_REV"),
         ("lean_toolchain", "HERMES_LEAN_TOOLCHAIN"),
         ("charon_version", "HERMES_CHARON_EXPECTED_VERSION"),
+        ("charon_rust_toolchain", "HERMES_CHARON_RUST_TOOLCHAIN"),
     ];
 
     for (key, env_var) in vars {
diff --git a/tools/hermes/examples/const_generics.rs b/tools/hermes/examples/const_generics.rs
index 8240b359f8..ff2e8cf2bc 100644
--- a/tools/hermes/examples/const_generics.rs
+++ b/tools/hermes/examples/const_generics.rs
@@ -1,4 +1,15 @@
-/// ```lean, hermes, spec
+/// ```hermes
+/// isValid self := N > 0
+/// ```
+pub struct ConstGen<const N: usize>;
+
+/// ```hermes
+/// isSafe : N > 0
+/// ```
+pub unsafe trait ConstTrait<const N: usize> {}
+
+/// ```hermes
+/// ensures: if N.val = 0 then ret.val = 0 else True
 /// ```
 pub fn use_const<const N: usize>(arr: [u8; N]) -> u8 {
     if N > 0 { arr[0] } else { 0 }
diff --git a/tools/hermes/src/charon.rs b/tools/hermes/src/charon.rs
index fd2f214f7e..ddb8f09931 100644
--- a/tools/hermes/src/charon.rs
+++ b/tools/hermes/src/charon.rs
@@ -288,10 +288,7 @@ fn check_charon_version(toolchain: &crate::setup::Toolchain) -> Result<()> {
 /// installed via rustup. If it is missing, we provide a helpful error message
 /// with the installation command.
 fn check_rustup_toolchain() -> Result<()> {
-    // FIXME: We should probably parse this from Charon's metadata or a central
-    // place. For now, it's pinned to a specific nightly in Charon's build.
-    // In the future, Hermes could also manage the rustup toolchain.
-    let nightly_version = "nightly-2025-01-26";
+    let nightly_version = env!("HERMES_CHARON_RUST_TOOLCHAIN");
 
     let output = Command::new("rustup")
         .args(["toolchain", "list"])
diff --git a/tools/hermes/testdata/setup/aeneas-linux-x86_64.tar.gz b/tools/hermes/testdata/setup/aeneas-linux-x86_64.tar.gz
index b9bb51acd0..9999bc0ac1 100644
Binary files a/tools/hermes/testdata/setup/aeneas-linux-x86_64.tar.gz and b/tools/hermes/testdata/setup/aeneas-linux-x86_64.tar.gz differ
diff --git a/tools/hermes/testdata/setup/aeneas-macos-aarch64.tar.gz b/tools/hermes/testdata/setup/aeneas-macos-aarch64.tar.gz
index 5b62840678..360838e698 100644
Binary files a/tools/hermes/testdata/setup/aeneas-macos-aarch64.tar.gz and b/tools/hermes/testdata/setup/aeneas-macos-aarch64.tar.gz differ
diff --git a/tools/hermes/testdata/setup/aeneas-macos-x86_64.tar.gz b/tools/hermes/testdata/setup/aeneas-macos-x86_64.tar.gz
index ca15838cac..5cf3edbeeb 100644
Binary files a/tools/hermes/testdata/setup/aeneas-macos-x86_64.tar.gz and b/tools/hermes/testdata/setup/aeneas-macos-x86_64.tar.gz differ
diff --git a/tools/hermes/tests/fixtures/associated_types/hermes.toml b/tools/hermes/tests/fixtures/associated_types/hermes.toml
index 37a83639ce..2027a39260 100644
--- a/tools/hermes/tests/fixtures/associated_types/hermes.toml
+++ b/tools/hermes/tests/fixtures/associated_types/hermes.toml
@@ -4,6 +4,8 @@ Behavior: Compiles a Rust source featuring a trait with an associated type (`T::
 """
 
 [test]
+# FIXME(#3089): Update to use valid syntax in `lib.rs`; coalesce with
+# `test_4_6_assoc_types`.
+expected_status = "known_bug"
 stderr_file = "expected.stderr"
-expected_status = "failure"
 args = ["verify", "--allow-sorry"]
diff --git a/tools/hermes/tests/fixtures/design_doc/expected.stderr b/tools/hermes/tests/fixtures/design_doc/expected.stderr
deleted file mode 100644
index 58ed8cd441..0000000000
--- a/tools/hermes/tests/fixtures/design_doc/expected.stderr
+++ /dev/null
@@ -1,16 +0,0 @@
-
-=== Hermes Verification Failed ===
-
-[Hermes Error] hermes::doc_block
-
-  × Documentation block error: `requires` sections are only permitted on
-  │ `unsafe` functions.
-    ╭─[[PROJECT_ROOT]/src/lib.rs:62:1]
- 61 │ /// ```lean, hermes
- 62 │ /// requires: stack.len > 0
-    · ─────────────┬─────────────
-    ·              ╰── problematic block
- 63 │ /// ensures:
-    ╰────
-
-Error: Aborting due to 1 previous errors.
diff --git a/tools/hermes/tests/fixtures/design_doc/hermes.toml b/tools/hermes/tests/fixtures/design_doc/hermes.toml
deleted file mode 100644
index d95580f54b..0000000000
--- a/tools/hermes/tests/fixtures/design_doc/hermes.toml
+++ /dev/null
@@ -1,9 +0,0 @@
-description = """
-Purpose: Tests the Hermes code generation using the exact examples from the design doc.
-Behavior: Exercises the 'isSafe', 'isValid' and 'spec' attribute mapping against functions and structs.
-"""
-
-[test]
-stderr_file = "expected.stderr"
-expected_status = "failure"
-args = ["verify", "--allow-sorry", "--unsound-allow-is-valid"]
diff --git a/tools/hermes/tests/fixtures/design_doc/source/Cargo.toml b/tools/hermes/tests/fixtures/design_doc/source/Cargo.toml
deleted file mode 100644
index a027d7deeb..0000000000
--- a/tools/hermes/tests/fixtures/design_doc/source/Cargo.toml
+++ /dev/null
@@ -1,8 +0,0 @@
-[package]
-name = "design_doc"
-version = "0.1.0"
-edition = "2021"
-
-[dependencies]
-
-[workspace]
diff --git a/tools/hermes/tests/fixtures/design_doc/source/src/lib.rs b/tools/hermes/tests/fixtures/design_doc/source/src/lib.rs
deleted file mode 100644
index 3b7c3c1ef4..0000000000
--- a/tools/hermes/tests/fixtures/design_doc/source/src/lib.rs
+++ /dev/null
@@ -1,73 +0,0 @@
-/// ```lean, hermes, unsafe(axiom)
-/// requires: b.val > 0
-/// ensures:
-///   ///   ///   ret.val = a.val / b.val
-/// ```
-#[allow(unused_unsafe)]
-pub unsafe fn safe_div(a: u32, b: u32) -> u32 {
-    unsafe { a / b }
-}
-
-/// ```lean, hermes, spec
-/// ensures:
-///   ///   ///   ret.val = a.val
-/// proof context:
-/// proof:
-///   rw [wrapper]
-///   obtain ⟨ret_val, h_eq⟩ := safe_div_spec a 1#u32 (by decide)
-///   simp_all [Nat.div_one]
-///   omega
-/// ```
-pub fn wrapper(a: u32) -> u32 {
-    unsafe { safe_div(a, 1) }
-}
-
-/// ```lean, hermes
-/// isValid self := 2 | self.x.val
-/// ```
-pub struct Even {
-    #[allow(dead_code)]
-    x: usize,
-}
-
-/// ```lean, hermes
-/// isSafe :
-///   ...
-/// ```
-pub unsafe trait FromBytes {}
-
-/// ```lean, hermes, spec
-/// ensures:
-///   ///   ///   ret.val = x.val
-/// proof context:
-/// proof:
-///   -- We will use sorry here for unproven things to allow verification to proceed
-///   sorry
-/// ```
-pub fn read_val(x: &u32) -> u32 {
-    *x
-}
-
-/// ```lean, hermes, spec
-/// ensures:
-///   ///   ///   x'.val = x.val + add.val
-/// proof context:
-///   have h_foo : True := True.intro
-/// ```
-pub fn add_in_place(x: &mut u32, add: u32) {
-    *x += add;
-}
-
-/// ```lean, hermes
-/// requires: stack.len > 0
-/// ensures:
-///   ///   ///   stack'.len = stack.len - 1
-/// ensures (h_second):
-///   ///   ///   ret = stack[stack.len - 1]
-/// proof context:
-///   have h_foo : True := True.intro
-/// ```
-pub fn pop(stack: &mut Vec<u32>) -> u32 {
-    stack.pop().unwrap()
-}
-
diff --git a/tools/hermes/tests/fixtures/duplicate_blocks/hermes.toml b/tools/hermes/tests/fixtures/duplicate_blocks/hermes.toml
index cfeec1bd66..37cb609d46 100644
--- a/tools/hermes/tests/fixtures/duplicate_blocks/hermes.toml
+++ b/tools/hermes/tests/fixtures/duplicate_blocks/hermes.toml
@@ -4,6 +4,6 @@ Behavior: Declares a single function with two consecutive `/// ```lean, hermes`
 """
 
 [test]
+expected_status = "failure"
 stderr_file = "expected.stderr"
 args = ["verify", "--allow-sorry"]
-expected_status = "failure"
diff --git a/tools/hermes/tests/fixtures/edge_cases_invariants/test_4_6_assoc_types/hermes.toml b/tools/hermes/tests/fixtures/edge_cases_invariants/test_4_6_assoc_types/hermes.toml
index 32c4af6892..6ab9e06772 100644
--- a/tools/hermes/tests/fixtures/edge_cases_invariants/test_4_6_assoc_types/hermes.toml
+++ b/tools/hermes/tests/fixtures/edge_cases_invariants/test_4_6_assoc_types/hermes.toml
@@ -4,5 +4,7 @@ Behavior: In an `isValid` boundary condition, queries the default instantiation
 """
 
 [test]
-expected_status = "failure"
+# FIXME(#3089): Update the syntax in `lib.rs` to be valid Lean, and get this
+# passing.
+expected_status = "known_bug"
 args = ["verify", "--allow-sorry", "--unsound-allow-is-valid"]
diff --git a/tools/hermes/tests/fixtures/edge_cases_invariants/test_4_6_assoc_types/source/src/lib.rs b/tools/hermes/tests/fixtures/edge_cases_invariants/test_4_6_assoc_types/source/src/lib.rs
index 32eb3ba1d8..9abcb4a866 100644
--- a/tools/hermes/tests/fixtures/edge_cases_invariants/test_4_6_assoc_types/source/src/lib.rs
+++ b/tools/hermes/tests/fixtures/edge_cases_invariants/test_4_6_assoc_types/source/src/lib.rs
@@ -3,7 +3,7 @@ pub trait Iter {
     type Item: Default;
 }
 
-/// ```lean, hermes
+/// ```hermes
 /// proof (h_progress):
 ///   sorry
 /// proof context:
@@ -13,8 +13,9 @@ pub fn check_item<T: Iter>(x: T::Item) -> T::Item {
     x
 }
 
-/// @spec
+/// ```hermes
 /// isValid self := self.val == T::Item::default()
+/// ```
 pub struct Wrapper<T: Iter> where T::Item: PartialEq {
     pub val: T::Item,
 }
diff --git a/tools/hermes/tests/fixtures/edge_cases_naming/test_1_1_lean_keywords_fns/hermes.toml b/tools/hermes/tests/fixtures/edge_cases_naming/test_1_1_lean_keywords_fns/hermes.toml
index d20c2131d8..e7cd6e5f5d 100644
--- a/tools/hermes/tests/fixtures/edge_cases_naming/test_1_1_lean_keywords_fns/hermes.toml
+++ b/tools/hermes/tests/fixtures/edge_cases_naming/test_1_1_lean_keywords_fns/hermes.toml
@@ -4,5 +4,6 @@ Behavior: Asserts that `fn theorem()`, `fn match()`, etc. are strictly escaped i
 """
 
 [test]
-expected_status = "failure"
+# FIXME(#3089): This should succeed
+expected_status = "known_bug"
 args = ["verify", "--allow-sorry"]
diff --git a/tools/hermes/tests/fixtures/edge_cases_naming/test_1_3_rust_keywords_idents/hermes.toml b/tools/hermes/tests/fixtures/edge_cases_naming/test_1_3_rust_keywords_idents/hermes.toml
index 8e56d84d9b..0c6dd38316 100644
--- a/tools/hermes/tests/fixtures/edge_cases_naming/test_1_3_rust_keywords_idents/hermes.toml
+++ b/tools/hermes/tests/fixtures/edge_cases_naming/test_1_3_rust_keywords_idents/hermes.toml
@@ -4,5 +4,5 @@ Behavior: Uses Rust keywords natively (`r#match`, `r#type`). Confirms Charon saf
 """
 
 [test]
-expected_status = "failure"
+expected_status = "known_bug"
 args = ["verify", "--allow-sorry"]
diff --git a/tools/hermes/tests/fixtures/edge_cases_types/test_2_3_zst/hermes.toml b/tools/hermes/tests/fixtures/edge_cases_types/test_2_3_zst/hermes.toml
index 610251cdae..0ef4e1db20 100644
--- a/tools/hermes/tests/fixtures/edge_cases_types/test_2_3_zst/hermes.toml
+++ b/tools/hermes/tests/fixtures/edge_cases_types/test_2_3_zst/hermes.toml
@@ -4,5 +4,6 @@ Behavior: Utilizes explicit zero-sized structs and the common `()` unit type to
 """
 
 [test]
-expected_status = "failure"
-args = ["verify", "--allow-sorry"]
+# FIXME(#3089): This should succeed.
+expected_status = "known_bug"
+args = ["verify", "--allow-sorry", "--unsound-allow-is-valid"]
diff --git a/tools/hermes/tests/fixtures/edge_cases_types/test_2_3_zst/source/src/lib.rs b/tools/hermes/tests/fixtures/edge_cases_types/test_2_3_zst/source/src/lib.rs
index bd902c3321..d4cbe3620f 100644
--- a/tools/hermes/tests/fixtures/edge_cases_types/test_2_3_zst/source/src/lib.rs
+++ b/tools/hermes/tests/fixtures/edge_cases_types/test_2_3_zst/source/src/lib.rs
@@ -1,16 +1,21 @@
-
+/// ```hermes
+/// isValid self := True
+/// ```
 pub struct Empty {}
 
+/// ```hermes
+/// isValid self := True
+/// ```
 pub struct WrapUnit {
     pub f: (),
 }
 
-/// ```lean, hermes
-/// proof (h_progress):
-///   sorry
-/// proof context:
-///   have h_foo : True := True.intro
+/// ```hermes
+/// ensures: True
 /// ```
 pub fn unit_arg(_: ()) {}
 
+/// ```hermes
+/// ensures: True
+/// ```
 pub fn unit_ret() -> () {}
diff --git a/tools/hermes/tests/fixtures/edge_cases_types/test_2_6_nested_refs/hermes.toml b/tools/hermes/tests/fixtures/edge_cases_types/test_2_6_nested_refs/hermes.toml
index 9348e7ee10..e770de59b5 100644
--- a/tools/hermes/tests/fixtures/edge_cases_types/test_2_6_nested_refs/hermes.toml
+++ b/tools/hermes/tests/fixtures/edge_cases_types/test_2_6_nested_refs/hermes.toml
@@ -4,5 +4,5 @@ Behavior: Uses parameters such as `&&u32`, `&mut &u32`, and `&&mut u32`. Validat
 """
 
 [test]
-expected_status = "failure"
+expected_status = "known_bug"
 args = ["verify", "--allow-sorry"]
diff --git a/tools/hermes/tests/fixtures/edge_cases_types/test_2_9_generic_bounds/hermes.toml b/tools/hermes/tests/fixtures/edge_cases_types/test_2_9_generic_bounds/hermes.toml
deleted file mode 100644
index 7d611de900..0000000000
--- a/tools/hermes/tests/fixtures/edge_cases_types/test_2_9_generic_bounds/hermes.toml
+++ /dev/null
@@ -1,8 +0,0 @@
-description = """
-Purpose: Exercises bounded parameters and non-instantiated markers.
-Behavior: Tests generic bounds and unused generic instantiations utilizing `PhantomData<T>`. Verifies standard typing constraints pass into Lean via `variable (T : Type)`.
-"""
-
-[test]
-expected_status = "failure"
-args = ["verify", "--allow-sorry"]
diff --git a/tools/hermes/tests/fixtures/edge_cases_types/test_2_9_generic_bounds/source/Cargo.toml b/tools/hermes/tests/fixtures/edge_cases_types/test_2_9_generic_bounds/source/Cargo.toml
deleted file mode 100644
index 65aea2bde9..0000000000
--- a/tools/hermes/tests/fixtures/edge_cases_types/test_2_9_generic_bounds/source/Cargo.toml
+++ /dev/null
@@ -1,9 +0,0 @@
-
-[package]
-name = "test_2_9_generic_bounds"
-version = "0.1.0"
-edition = "2021"
-
-[dependencies]
-
-[workspace]
diff --git a/tools/hermes/tests/fixtures/edge_cases_types/test_2_9_generic_bounds/source/src/lib.rs b/tools/hermes/tests/fixtures/edge_cases_types/test_2_9_generic_bounds/source/src/lib.rs
deleted file mode 100644
index cdc715d440..0000000000
--- a/tools/hermes/tests/fixtures/edge_cases_types/test_2_9_generic_bounds/source/src/lib.rs
+++ /dev/null
@@ -1,13 +0,0 @@
-pub struct Phantom<T> {
-    _marker: std::marker::PhantomData<T>,
-}
-
-/// ```lean, hermes
-/// proof (h_progress):
-///   sorry
-/// proof context:
-///   have h_foo : True := True.intro
-/// ```
-pub fn unused<T>(x: u32) -> u32 {
-    x
-}
diff --git a/tools/hermes/tests/fixtures/is_valid_verification/hermes.toml b/tools/hermes/tests/fixtures/is_valid_verification/hermes.toml
index 4b37a866d8..6fbb325ff8 100644
--- a/tools/hermes/tests/fixtures/is_valid_verification/hermes.toml
+++ b/tools/hermes/tests/fixtures/is_valid_verification/hermes.toml
@@ -1,6 +1,6 @@
 description = """
 Purpose: Exercises end-to-end Lean verification integration evaluating `isValid` invariants.
-Behavior: Uses `--verify` to trigger Lean analysis on the extracted logic. Confirms that purposefully faulty initialization states correctly drive Lean to trip the `Decidable` invariant logic, reporting "failed to synthesize" through Hermes.
+Behavior: Confirms that purposefully faulty initialization states correctly drive Lean to trip the `Decidable` invariant logic, reporting "failed to synthesize" through Hermes.
 """
 
 [test]
diff --git a/tools/hermes/tests/fixtures/map_symlinked_file/hermes.toml b/tools/hermes/tests/fixtures/map_symlinked_file/hermes.toml
index 8328ee7ffc..bb2e935bee 100644
--- a/tools/hermes/tests/fixtures/map_symlinked_file/hermes.toml
+++ b/tools/hermes/tests/fixtures/map_symlinked_file/hermes.toml
@@ -3,6 +3,10 @@ Purpose: Validates diagnostics resolution pointing to canonicalized symlinks.
 Behavior: Provides Charon errors mapped to an original `untransformed.rs` target spanning behind a symlink. Ensures Hermes resolves and prints the logical/canonical code appropriately.
 """
 
+# FIXME(#3089): It looks like this test *originally* correctly exercised symlink
+# logic, but it doesn't anymore. We should fix this to ensure it actualy
+# uses symlinks.
+
 [test]
 stderr_file = "expected.stderr"
 args = ["verify", "--allow-sorry"]
diff --git a/tools/hermes/tests/fixtures/multiple_errors/hermes.toml b/tools/hermes/tests/fixtures/multiple_errors/hermes.toml
index 0666d29f6b..c5fd43c18c 100644
--- a/tools/hermes/tests/fixtures/multiple_errors/hermes.toml
+++ b/tools/hermes/tests/fixtures/multiple_errors/hermes.toml
@@ -1,7 +1,4 @@
-description = """
-Purpose: Checks aggregation for widespread compilation failures.
-Behavior: Embeds syntax issues in two independent files (`a.rs`, `b.rs`). Exercises the diagnostic collector to aggregate and uniformly render the batch of distinct parsing errors.
-"""
+description = "Tests that syntax errors across multiple files are all reported"
 
 [test]
 stderr_file = "expected.stderr"
diff --git a/tools/hermes/tests/fixtures/named_bounds_validation_failures/hermes.toml b/tools/hermes/tests/fixtures/named_bounds_validation_failures/hermes.toml
index c641c3a7cf..64ba649d22 100644
--- a/tools/hermes/tests/fixtures/named_bounds_validation_failures/hermes.toml
+++ b/tools/hermes/tests/fixtures/named_bounds_validation_failures/hermes.toml
@@ -4,6 +4,6 @@ Behavior: Introduces missing colons, invalid names, and Lean keywords as named b
 """
 
 [test]
+expected_status = "failure"
 stderr_file = "expected.stderr"
 args = ["verify", "--allow-sorry", "--unsound-allow-is-valid"]
-expected_status = "failure"
diff --git a/tools/hermes/tests/fixtures/named_bounds_validation_failures/source/src/lib.rs b/tools/hermes/tests/fixtures/named_bounds_validation_failures/source/src/lib.rs
index 12bbd8f1d9..acd5c6bef0 100644
--- a/tools/hermes/tests/fixtures/named_bounds_validation_failures/source/src/lib.rs
+++ b/tools/hermes/tests/fixtures/named_bounds_validation_failures/source/src/lib.rs
@@ -2,7 +2,6 @@
 /// We test both validation errors (rust-level parsing and validation)
 /// and verification errors (Lean-level theorem failures).
 
-
 /// 3. Mismatched proof name
 /// ```lean, hermes, spec
 /// ensures (h_ensures):
@@ -15,7 +14,6 @@ fn fail_mismatched_proof_name(x: u32) -> u32 {
     x
 }
 
-
 /// 9. Reserved name collision (requires)
 /// ```lean, hermes, spec
 /// requires (h_x_is_valid):
@@ -30,7 +28,6 @@ unsafe fn fail_reserved_name_collision_requires(x: u32) -> u32 {
     x
 }
 
-
 /// 10. Reserved name collision (ensures)
 /// ```lean, hermes, spec
 /// ensures (h_ret_is_valid):
@@ -43,7 +40,6 @@ fn fail_reserved_name_collision_ensures(x: u32) -> u32 {
     x
 }
 
-
 /// 26. Proof targets a requires clause instead of an ensures clause
 /// ```lean, hermes, spec
 /// requires (h_req):
diff --git a/tools/hermes/tests/fixtures/reject_safe_requires/hermes.stderr b/tools/hermes/tests/fixtures/reject_safe_requires/hermes.stderr
index c9d51f37e5..82065badd8 100644
--- a/tools/hermes/tests/fixtures/reject_safe_requires/hermes.stderr
+++ b/tools/hermes/tests/fixtures/reject_safe_requires/hermes.stderr
@@ -7,7 +7,7 @@
   │ `unsafe` functions.
    ╭─[[PROJECT_ROOT]/src/lib.rs:2:1]
  1 │ /// ```hermes
- 2 │ /// requires: true
+ 2 │ /// requires: True
    · ─────────┬────────
    ·          ╰── problematic block
  3 │ /// ```
@@ -40,4 +40,17 @@
  14 │ /// ```
     ╰────
 
-Error: Aborting due to 3 previous errors.
+
+[Hermes Error] hermes::doc_block
+
+  × Documentation block error: `requires` sections are only permitted on
+  │ `unsafe` functions.
+    ╭─[[PROJECT_ROOT]/src/lib.rs:18:1]
+ 17 │ /// ```hermes
+ 18 │ /// requires(h_true): True
+    · ─────────────┬────────────
+    ·              ╰── problematic block
+ 19 │ /// ```
+    ╰────
+
+Error: Aborting due to 4 previous errors.
diff --git a/tools/hermes/tests/fixtures/reject_safe_requires/hermes.toml b/tools/hermes/tests/fixtures/reject_safe_requires/hermes.toml
index 2f3d0ebe97..d7d394065c 100644
--- a/tools/hermes/tests/fixtures/reject_safe_requires/hermes.toml
+++ b/tools/hermes/tests/fixtures/reject_safe_requires/hermes.toml
@@ -1,7 +1,4 @@
-description = """
-Purpose: Verify that `requires` blocks are strictly rejected on safe functions.
-Behavior: Hermes parses the file, encounters `requires` on safe functions, and errors out pointing to the specific spans.
-"""
+description = "Verify that `requires` blocks are rejected on safe functions."
 
 [test]
 args = ["verify"]
diff --git a/tools/hermes/tests/fixtures/reject_safe_requires/source/src/lib.rs b/tools/hermes/tests/fixtures/reject_safe_requires/source/src/lib.rs
index 22090081ce..ebf9994f1f 100644
--- a/tools/hermes/tests/fixtures/reject_safe_requires/source/src/lib.rs
+++ b/tools/hermes/tests/fixtures/reject_safe_requires/source/src/lib.rs
@@ -1,5 +1,5 @@
 /// ```hermes
-/// requires: true
+/// requires: True
 /// ```
 pub fn safe_with_requires() {}
 
@@ -13,3 +13,8 @@ pub fn multiple_requires_safe(x: u32, y: u32) {}
 /// requires:
 /// ```
 pub fn empty_requires_safe() {}
+
+/// ```hermes
+/// requires(h_true): True
+/// ```
+pub fn named_requires_safe() {}
diff --git a/tools/hermes/tests/fixtures/type_features/expected.stderr b/tools/hermes/tests/fixtures/type_features/expected.stderr
index 2500d29c84..e3700cad00 100644
--- a/tools/hermes/tests/fixtures/type_features/expected.stderr
+++ b/tools/hermes/tests/fixtures/type_features/expected.stderr
@@ -79,42 +79,6 @@
  47 │     A(u32),
     ╰────
 
-  ⚠ union `MyUnion` is never used
-    ╭─[[PROJECT_ROOT]/src/lib.rs:51:7]
- 50 │ 
- 51 │ union MyUnion {
-    ·       ───┬───
-    ·          ╰── 
- 52 │     f1: u32,
-    ╰────
-
-  ⚠ struct `UnionWrapper` is never constructed
-    ╭─[[PROJECT_ROOT]/src/lib.rs:59:8]
- 58 │ /// ```
- 59 │ struct UnionWrapper(MyUnion);
-    ·        ──────┬─────
-    ·              ╰── 
-    ╰────
-
-Error: Aeneas failed for package 'type_features' with status: exit status: 2
-stderr:
-Applied prepasses:  [----------------------------------------------------] 0/1 ⠋Applied prepasses:  [####################################################] 1/1 ⠋Applied prepasses:  [####################################################] 1/1 ✔️
-Uncaught exception:
-  
-  (Failure
-    "unions are not supported\
-   \nSource: 'src/lib.rs', lines 51:0-54:1\
-   \nCompiler source: llbc/TypesAnalysis.ml, line 503")
-
-Raised at Aeneas__Errors.craise_opt_span in file "Errors.ml", line 120, characters 4-23
-Called from Aeneas__Errors.craise in file "Errors.ml" (inlined), line 126, characters 2-43
-Called from Aeneas__TypesAnalysis.analyze_type_decl in file "llbc/TypesAnalysis.ml", line 503, characters 19-74
-Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
-Called from Aeneas__TypesAnalysis.analyze_type_declaration_group.analyze in file "llbc/TypesAnalysis.ml", lines 554-556, characters 6-23
-Called from Aeneas__Interp.analyze_type_declarations.(fun) in file "interp/Interp.ml", line 31, characters 10-62
-Called from Stdlib__List.fold_left in file "list.ml", line 123, characters 24-34
-Called from Aeneas__Interp.compute_contexts in file "interp/Interp.ml", line 153, characters 19-66
-Called from Aeneas__Translate.translate_crate_to_pure in file "Translate.ml", line 290, characters 18-40
-Called from Aeneas__Translate.translate_crate in file "Translate.ml", line 2100, characters 31-71
-Called from Dune__exe__Main in file "Main.ml", lines 715-716, characters 8-37
-
+[External Error] generated/TypeFeaturesTypeFeatures<HASH>/TypeFeaturesTypeFeatures<HASH>.lean: type expected, got
+  (UsesAssoc Self : Type → Type)
+Error: Lean verification failed
diff --git a/tools/hermes/tests/fixtures/type_features/source/src/lib.rs b/tools/hermes/tests/fixtures/type_features/source/src/lib.rs
index d726bff9cd..57d3fdf3a0 100644
--- a/tools/hermes/tests/fixtures/type_features/source/src/lib.rs
+++ b/tools/hermes/tests/fixtures/type_features/source/src/lib.rs
@@ -1,11 +1,11 @@
 /// ```hermes
-/// isValid self := {N} > 0
+/// isValid self := N > 0
 /// ```
 struct ConstGen<const N: usize>;
 
 /// ```hermes
 /// isSafe :
-///   {N} > 0
+///   N > 0
 /// ```
 unsafe trait ConstTrait<const N: usize> {}
 
@@ -47,13 +47,3 @@ enum ValidatedEnum {
     A(u32),
     B { x: u32 },
 }
-
-union MyUnion {
-    f1: u32,
-    f2: f32,
-}
-
-/// ```hermes
-/// isValid self := True
-/// ```
-struct UnionWrapper(MyUnion);
diff --git a/tools/hermes/tests/fixtures/ui_build_script_noise/hermes.toml b/tools/hermes/tests/fixtures/ui_build_script_noise/hermes.toml
index 5974a9dd90..0e50ea9bf4 100644
--- a/tools/hermes/tests/fixtures/ui_build_script_noise/hermes.toml
+++ b/tools/hermes/tests/fixtures/ui_build_script_noise/hermes.toml
@@ -3,6 +3,9 @@ Purpose: Tests UI robustness handling invalid JSON interlacing from build script
 Behavior: Prints invalid JSON payloads before emitting a valid `compiler-artifact` blob. Ensures Hermes' diagnostic collector discards garbage outputs without panicking.
 """
 
+# FIXME(#3089): Hermes doesn't panic, but it also doesn't seem to interpret the
+# JSON payload, instead passing it to stderr verbatim.
+
 [test]
 stderr_file = "expected.stderr"
 args = ["verify", "--allow-sorry"]
diff --git a/tools/hermes/tests/fixtures/ui_silent_panic/hermes.toml b/tools/hermes/tests/fixtures/ui_silent_panic/hermes.toml
index b3b6b35037..c99d500be7 100644
--- a/tools/hermes/tests/fixtures/ui_silent_panic/hermes.toml
+++ b/tools/hermes/tests/fixtures/ui_silent_panic/hermes.toml
@@ -4,6 +4,6 @@ Behavior: Triggers a `panic!("Boom")` immediately in `build.rs`. Confirms Hermes
 """
 
 [test]
+expected_status = "failure"
 stderr_file = "expected.stderr"
 args = ["verify", "--allow-sorry"]
-expected_status = "failure"
diff --git a/tools/hermes/tests/fixtures/ui_silent_panic/source/src/lib.rs b/tools/hermes/tests/fixtures/ui_silent_panic/source/src/lib.rs
index 8afbc86ed9..ca243b427c 100644
--- a/tools/hermes/tests/fixtures/ui_silent_panic/source/src/lib.rs
+++ b/tools/hermes/tests/fixtures/ui_silent_panic/source/src/lib.rs
@@ -1,3 +1,3 @@
-/// ```lean, hermes
+/// ```hermes
 /// ```
 pub fn foo() {}
diff --git a/tools/hermes/tests/integration.rs b/tools/hermes/tests/integration.rs
index 8fc92ea0ea..15003e08ba 100644
--- a/tools/hermes/tests/integration.rs
+++ b/tools/hermes/tests/integration.rs
@@ -1371,8 +1371,8 @@ fn run_toolchain_versioning_test(path: &Path) -> datatest_stable::Result<()> {
     let metadata = cargo_toml
         .get("package")
         .and_then(|p| p.get("metadata"))
-        .and_then(|m| m.get("build-rs"))
-        .expect("Cargo.toml must have [package.metadata.build-rs]");
+        .and_then(|m| m.get("build_rs"))
+        .expect("Cargo.toml must have [package.metadata.build_rs]");
 
     let expected_rev = metadata.get("aeneas_rev").and_then(|v| v.as_str()).unwrap();
     let expected_toolchain = metadata.get("lean_toolchain").and_then(|v| v.as_str()).unwrap();
@@ -2012,8 +2012,8 @@ fn get_expected_charon_version() -> String {
     let metadata = cargo_toml
         .get("package")
         .and_then(|p| p.get("metadata"))
-        .and_then(|m| m.get("build-rs"))
-        .expect("Cargo.toml must have [package.metadata.build-rs]");
+        .and_then(|m| m.get("build_rs"))
+        .expect("Cargo.toml must have [package.metadata.build_rs]");
 
     metadata.get("charon_version").and_then(|v| v.as_str()).unwrap().to_string()
 }
diff --git a/tools/hermes/tools/roll-pinned-prebuilts.py b/tools/hermes/tools/roll-pinned-prebuilts.py
index 3e38c75eb3..92ceb8ca98 100755
--- a/tools/hermes/tools/roll-pinned-prebuilts.py
+++ b/tools/hermes/tools/roll-pinned-prebuilts.py
@@ -246,11 +246,11 @@ def update_cargo_toml(aeneas_meta, charon_meta, dry_run=False):
     try:
         metadata = doc["package"]["metadata"]
 
-        # Update the build-rs section, which defines the environment variables
+        # Update the build_rs section, which defines the environment variables
         # injected into the Hermes build process.
-        metadata["build-rs"]["aeneas_rev"] = aeneas_meta["commit"]
-        metadata["build-rs"]["lean_toolchain"] = aeneas_meta["lean_toolchain"]
-        metadata["build-rs"]["charon_version"] = charon_meta["version"]
+        metadata["build_rs"]["aeneas_rev"] = aeneas_meta["commit"]
+        metadata["build_rs"]["lean_toolchain"] = aeneas_meta["lean_toolchain"]
+        metadata["build_rs"]["charon_version"] = charon_meta["version"]
 
         # Update the hermes.dependencies section, which defines the download URLs
         # and checksums used by the 'cargo hermes setup' command.