diff --git a/tools/hermes/src/charon.rs b/tools/hermes/src/charon.rs
index 4e507bba34..77ca2ef10d 100644
--- a/tools/hermes/src/charon.rs
+++ b/tools/hermes/src/charon.rs
@@ -39,6 +39,13 @@ pub fn run_charon(args: &Args, roots: &Roots, packages: &[HermesArtifact]) -> Re
         let mut start_from = artifact.start_from.clone();
         start_from.sort();
 
+        // NOTE: This is an optimization that is relevant because, when we
+        // encounter items which we can't name (which carry Hermes annotations),
+        // we add their parent module to the list of entrypoints. If there are
+        // multiple items in the same module, this can lead to duplication in
+        // the list of entrypoints.
+        start_from.dedup();
+
         let start_from_str = start_from.join(",");
         // OS command-line length limits (Windows is ~32k; Linux `ARG_MAX` is
         // usually larger, but variable)
diff --git a/tools/hermes/src/parse.rs b/tools/hermes/src/parse.rs
index ce374e1895..300f9aae5b 100644
--- a/tools/hermes/src/parse.rs
+++ b/tools/hermes/src/parse.rs
@@ -7,10 +7,9 @@ use std::{
 use log::{debug, trace};
 use miette::{NamedSource, SourceSpan};
 use proc_macro2::Span;
-use quote::quote;
 use syn::{
     spanned::Spanned as _, visit::Visit, Attribute, Error, Expr, ImplItemFn, ItemEnum, ItemFn,
-    ItemImpl, ItemMod, ItemStruct, ItemTrait, ItemUnion, Lit, Meta,
+    ItemImpl, ItemMod, ItemStruct, ItemTrait, ItemUnion, Lit, Meta, TraitItemFn,
 };
 
 use crate::errors::HermesError;
@@ -44,6 +43,7 @@ pub enum ParsedItem {
     Trait(ItemTrait),
     Impl(ItemImpl),
     ImplItemFn(ImplItemFn),
+    TraitItemFn(TraitItemFn),
 }
 
 impl ParsedItem {
@@ -55,6 +55,7 @@ impl ParsedItem {
             Self::Union(item) => Some(item.ident.to_string()),
             Self::Trait(item) => Some(item.ident.to_string()),
             Self::ImplItemFn(item) => Some(item.sig.ident.to_string()),
+            Self::TraitItemFn(item) => Some(item.sig.ident.to_string()),
             Self::Impl(_) => None,
         }
     }
@@ -69,6 +70,7 @@ impl ParsedItem {
             Self::Trait(item) => &item.attrs,
             Self::Impl(item) => &item.attrs,
             Self::ImplItemFn(item) => &item.attrs,
+            Self::TraitItemFn(item) => &item.attrs,
         }
     }
 }
@@ -89,6 +91,8 @@ pub struct UnloadedModule {
     /// The value of `#[path = "..."]` if present.
     pub path_attr: Option<String>,
     pub span: proc_macro2::Span,
+    /// True if this module was declared inside a block.
+    pub inside_block: bool,
 }
 
 /// Parses the given Rust source code and invokes the callback `f` for each item
@@ -103,29 +107,35 @@ where
     F: FnMut(&str, Result<ParsedLeanItem, HermesError>),
 {
     let mut unloaded_modules = Vec::new();
-    scan_compilation_unit_internal(source, None, f, |m| unloaded_modules.push(m));
+    scan_compilation_unit_internal(source, None, false, f, |m| unloaded_modules.push(m));
     unloaded_modules
 }
 
 /// Like [`scan_compilation_unit`], but reads the source code from a file path.
 ///
 /// Parsing errors and generated items will be associated with this file path.
+///
+/// Set `inside_block = true` if this file was discovered via a `mod foo;` item
+/// inside of a block.
 pub fn read_file_and_scan_compilation_unit<F>(
     path: &Path,
+    inside_block: bool,
     f: F,
 ) -> Result<(String, Vec<UnloadedModule>), io::Error>
 where
     F: FnMut(&str, Result<ParsedLeanItem, HermesError>),
 {
-    log::trace!("read_file_and_scan_compilation_unit({:?})", path);
+    log::trace!("read_file_and_scan_compilation_unit({:?}, inside_block={})", path, inside_block);
     let source = fs::read_to_string(path)?;
-    let unloaded_modules = scan_compilation_unit(&source, f);
+    let mut unloaded_modules = Vec::new();
+    scan_compilation_unit_internal(&source, None, inside_block, f, |m| unloaded_modules.push(m));
     Ok((source, unloaded_modules))
 }
 
 fn scan_compilation_unit_internal<I, M>(
     source: &str,
     source_file: Option<PathBuf>,
+    inside_block: bool,
     mut item_cb: I,
     mod_cb: M,
 ) where
@@ -141,10 +151,6 @@ fn scan_compilation_unit_internal<I, M>(
 
         f
     };
-    let _x = source_file
-        .as_ref()
-        .map(|p| p.display().to_string())
-        .unwrap_or_else(|| "<input>".to_string());
     let named_source = miette::NamedSource::new(file_name, source.to_string());
     let file = match syn::parse_file(source) {
         Ok(file) => {
@@ -168,7 +174,7 @@ fn scan_compilation_unit_internal<I, M>(
     trace!("Initializing HermesVisitor to traverse AST");
     let mut visitor = HermesVisitor {
         current_path: Vec::new(),
-        inside_block: false,
+        inside_block,
         item_cb,
         mod_cb,
         source_file,
@@ -195,8 +201,7 @@ where
     I: FnMut(&str, Result<ParsedLeanItem, HermesError>),
     M: FnMut(UnloadedModule),
 {
-    fn check_and_add(&mut self, item: ParsedItem, span: Span) {
-        // NEW: Check nesting
+    fn process_item(&mut self, item: ParsedItem, span: Span) {
         if self.inside_block {
             // Only check attributes if we are in a body to see if we need to
             // error. We want to avoid erroring on un-annotated local items.
@@ -268,6 +273,7 @@ where
                 name: mod_name.clone(),
                 path_attr: extract_path_attr(&node.attrs),
                 span: node.span(),
+                inside_block: self.inside_block,
             });
         }
 
@@ -290,32 +296,32 @@ where
 
     fn visit_item_fn(&mut self, node: &'ast ItemFn) {
         trace!("Visiting Fn {}", node.sig.ident);
-        self.check_and_add(ParsedItem::Fn(node.clone()), node.span());
+        self.process_item(ParsedItem::Fn(node.clone()), node.span());
         syn::visit::visit_item_fn(self, node);
     }
 
     fn visit_item_struct(&mut self, node: &'ast ItemStruct) {
         trace!("Visiting Struct {}", node.ident);
-        self.check_and_add(ParsedItem::Struct(node.clone()), node.span());
+        self.process_item(ParsedItem::Struct(node.clone()), node.span());
         syn::visit::visit_item_struct(self, node);
     }
 
     fn visit_item_enum(&mut self, node: &'ast ItemEnum) {
         trace!("Visiting Enum {}", node.ident);
-        self.check_and_add(ParsedItem::Enum(node.clone()), node.span());
+        self.process_item(ParsedItem::Enum(node.clone()), node.span());
         syn::visit::visit_item_enum(self, node);
     }
 
     fn visit_item_union(&mut self, node: &'ast ItemUnion) {
         trace!("Visiting Union {}", node.ident);
-        self.check_and_add(ParsedItem::Union(node.clone()), node.span());
+        self.process_item(ParsedItem::Union(node.clone()), node.span());
         syn::visit::visit_item_union(self, node);
     }
 
     fn visit_item_trait(&mut self, node: &'ast ItemTrait) {
         let name = node.ident.to_string();
         trace!("Visiting Trait {}", name);
-        self.check_and_add(ParsedItem::Trait(node.clone()), node.span());
+        self.process_item(ParsedItem::Trait(node.clone()), node.span());
 
         self.current_path.push(name);
         syn::visit::visit_item_trait(self, node);
@@ -331,27 +337,21 @@ where
 
     fn visit_item_impl(&mut self, node: &'ast ItemImpl) {
         trace!("Visiting Impl");
-        self.check_and_add(ParsedItem::Impl(node.clone()), node.span());
-
-        // If this is a trait impl, we use UFCS syntax (`<Type as Trait>`). If
-        // this is an inherent impl, we use the `Type: Type` syntax.
-        let self_ty = &node.self_ty;
-        let segment = if let Some((_, path, _)) = &node.trait_ {
-            quote! { <#self_ty as #path> }
-        } else {
-            quote! { #self_ty }
-        };
-
-        self.current_path.push(segment.to_string());
+        self.process_item(ParsedItem::Impl(node.clone()), node.span());
         syn::visit::visit_item_impl(self, node);
-        self.current_path.pop();
     }
 
     fn visit_impl_item_fn(&mut self, node: &'ast ImplItemFn) {
         trace!("Visiting ImplItemFn {}", node.sig.ident);
-        self.check_and_add(ParsedItem::ImplItemFn(node.clone()), node.span());
+        self.process_item(ParsedItem::ImplItemFn(node.clone()), node.span());
         syn::visit::visit_impl_item_fn(self, node);
     }
+
+    fn visit_trait_item_fn(&mut self, node: &'ast TraitItemFn) {
+        trace!("Visiting TraitItemFn {}", node.sig.ident);
+        self.process_item(ParsedItem::TraitItemFn(node.clone()), node.span());
+        syn::visit::visit_trait_item_fn(self, node);
+    }
 }
 
 /// Helper to extract exactly one Lean block from a slice of attributes.
@@ -605,6 +605,7 @@ mod tests {
         scan_compilation_unit_internal(
             code,
             Some(Path::new("src/foo.rs").to_path_buf()),
+            false,
             |source: &str, res| items.push((source.to_string(), res)),
             |_| {},
         );
@@ -689,12 +690,14 @@ mod c {
         scan_compilation_unit_internal(
             code1,
             Some(path.to_path_buf()),
+            false,
             |_src, res| items.push(res),
             |_| {},
         );
         scan_compilation_unit_internal(
             code2,
             Some(path.to_path_buf()),
+            false,
             |_src, res| items.push(res),
             |_| {},
         );
diff --git a/tools/hermes/src/resolve.rs b/tools/hermes/src/resolve.rs
index 49a0004b7d..77df8e32b7 100644
--- a/tools/hermes/src/resolve.rs
+++ b/tools/hermes/src/resolve.rs
@@ -102,6 +102,7 @@ impl TryFrom<&TargetKind> for HermesTargetKind {
 pub struct HermesTargetName {
     pub package_name: PackageName,
     pub target_name: String,
+    pub kind: HermesTargetKind,
 }
 
 #[derive(Debug)]
@@ -171,6 +172,7 @@ pub fn resolve_roots(args: &Args) -> Result<Roots> {
                 name: HermesTargetName {
                     package_name: package.name.clone(),
                     target_name: target.name.clone(),
+                    kind,
                 },
                 kind,
                 src_path: target.src_path.as_std_path().to_owned(),
diff --git a/tools/hermes/src/scanner.rs b/tools/hermes/src/scanner.rs
index 9e1c130891..f14191de67 100644
--- a/tools/hermes/src/scanner.rs
+++ b/tools/hermes/src/scanner.rs
@@ -7,7 +7,6 @@ use std::{
 };
 
 use anyhow::Result;
-use dashmap::DashSet;
 
 use crate::{
     parse,
@@ -39,7 +38,8 @@ impl HermesArtifact {
         // which would hash identically if we just hashed their concatenation.
         let h0 = hash(&self.manifest_path);
         let h1 = hash(&self.name.target_name);
-        let h = hash(&[h0, h1]);
+        let h2 = hash(&self.target_kind);
+        let h = hash(&[h0, h1, h2]);
         format!("{}-{}-{:08x}.llbc", self.name.package_name, self.name.target_name, h)
     }
 }
@@ -49,7 +49,6 @@ impl HermesArtifact {
 pub fn scan_workspace(roots: &Roots) -> Result<Vec<HermesArtifact>> {
     log::trace!("scan_workspace({:?})", roots);
 
-    let visited_paths = DashSet::new();
     let (err_tx, err_rx) = mpsc::channel();
     // Items are `((PackageName, TargetName), ItemPath)`.
     let (path_tx, path_rx) = mpsc::channel::<(HermesTargetName, String)>();
@@ -69,7 +68,6 @@ pub fn scan_workspace(roots: &Roots) -> Result<Vec<HermesArtifact>> {
 
     rayon::scope(|s| {
         for target in &roots.roots {
-            let visited = &visited_paths;
             let (err_tx, path_tx) = (err_tx.clone(), path_tx.clone());
             let roots_ref = roots;
 
@@ -84,11 +82,12 @@ pub fn scan_workspace(roots: &Roots) -> Result<Vec<HermesArtifact>> {
                     s,
                     &target.src_path,
                     roots_ref,
-                    visited,
                     err_tx,
                     path_tx,
                     initial_prefix,
                     target.name.clone(),
+                    false, // Initial call is top-level, so not inside block
+                    Vec::new(),
                 )
             });
         }
@@ -131,15 +130,21 @@ pub fn scan_workspace(roots: &Roots) -> Result<Vec<HermesArtifact>> {
         .collect())
 }
 
+// NOTE: It might be tempting to try to deduplicate files to avoid re-processing
+// a file that is reachable via multiple paths. However, this is incorrect, as
+// this only happens if the file is named in multiple `#[path]` attributes, in
+// which case it logically constitutes a distinct module each time it is
+// referenced.
 fn process_file_recursive<'a>(
     scope: &rayon::Scope<'a>,
     src_path: &Path,
     config: &'a Roots,
-    visited: &'a DashSet<PathBuf>,
     err_tx: Sender<anyhow::Error>,
     path_tx: Sender<(HermesTargetName, String)>,
-    module_prefix: Vec<String>,
+    current_prefix: Vec<String>,
     name: HermesTargetName,
+    inside_block: bool,
+    ancestors: Vec<PathBuf>,
 ) {
     log::trace!("process_file_recursive(src_path: {:?})", src_path);
 
@@ -157,40 +162,57 @@ fn process_file_recursive<'a>(
         }
     };
 
-    if !visited.insert(src_path.clone()) {
+    // Cycle detection: prevent infinite recursion on symlinks or recursive mod
+    // declarations, while still allowing identical files to be mounted in
+    // different branches of the tree. A cycle would represent an invalid crate
+    // anyway (i.e., an invalid set of `#[path]` attributes).
+    if ancestors.contains(&src_path) {
         return;
     }
+    let mut current_ancestors = ancestors.clone();
+    current_ancestors.push(src_path.clone());
 
-    // Walk the AST, collecting new modules to process.
-    let (_source_code, unloaded_modules) =
-        match parse::read_file_and_scan_compilation_unit(&src_path, |_src, item_result| {
-            match item_result {
-                Ok(parsed_item) => {
-                    if let Some(item_name) = parsed_item.item.name() {
-                        // Calculate the full path to this item.
-                        let mut full_path = module_prefix.clone();
-                        full_path.extend(parsed_item.module_path);
-                        full_path.push(item_name);
-
-                        let _ = path_tx.send((name.clone(), full_path.join("::")));
+    let result = parse::read_file_and_scan_compilation_unit(
+        &src_path,
+        inside_block,
+        |_src, res| match res {
+            Ok(item) => {
+                let mut full_path = current_prefix.clone();
+                full_path.extend(item.module_path);
+
+                use parse::ParsedItem::*;
+                match &item.item {
+                    // Unreliable syntaxes: we have no way of reliably naming
+                    // these in Charon's `--start-from` argument, so we fall
+                    // back to naming the parent module.
+                    Impl(_) | ImplItemFn(_) | TraitItemFn(_) => {
+                        let start_from = full_path.join("::");
+                        path_tx.send((name.clone(), start_from)).unwrap();
+                    }
+                    // Reliable syntaxes: target the specific item.
+                    _ => {
+                        if let Some(item_name) = item.item.name() {
+                            full_path.push(item_name);
+                            let start_from = full_path.join("::");
+                            log::debug!("Found entry point: {}", start_from);
+                            path_tx.send((name.clone(), start_from)).unwrap();
+                        }
                     }
-                }
-                Err(e) => {
-                    // A parsing error means we either:
-                    // 1. Lost the module graph, causing missing files later.
-                    // 2. Lost a specification, causing unsound verification.
-                    // We must abort the build.
-                    let _ = err_tx.send(anyhow::anyhow!(e));
                 }
             }
-        }) {
-            Ok(res) => res,
             Err(e) => {
-                let _ = err_tx
-                    .send(anyhow::anyhow!(e).context(format!("Failed to parse {:?}", src_path)));
-                return;
+                let _ = err_tx.send(e.into());
             }
-        };
+        },
+    );
+
+    let (_, unloaded_modules) = match result {
+        Ok(res) => res,
+        Err(e) => {
+            let _ = err_tx.send(e.into());
+            return;
+        }
+    };
 
     // Determine the directory to search for child modules in.
     // - For `mod.rs`, `lib.rs`, `main.rs`, children are in the parent directory.
@@ -213,13 +235,24 @@ fn process_file_recursive<'a>(
             // Spawn new tasks for discovered modules.
             let (err_tx, path_tx) = (err_tx.clone(), path_tx.clone());
 
-            let mut new_prefix = module_prefix.clone();
+            let mut new_prefix = current_prefix.clone();
             new_prefix.push(module.name);
 
             let name = name.clone();
+            // TODO: Can we do something more efficient than cloning here? Maybe
+            // a linked list?
+            let ancestors = current_ancestors.clone();
             scope.spawn(move |s| {
                 process_file_recursive(
-                    s, &mod_path, config, visited, err_tx, path_tx, new_prefix, name,
+                    s,
+                    &mod_path,
+                    config,
+                    err_tx,
+                    path_tx,
+                    new_prefix,
+                    name,
+                    module.inside_block,
+                    ancestors,
                 )
             })
         } else {
@@ -271,3 +304,49 @@ fn resolve_module_path(
 
     None
 }
+
+#[cfg(test)]
+mod tests {
+    use std::path::PathBuf;
+
+    use cargo_metadata::PackageName;
+
+    use super::*;
+    use crate::resolve::{HermesTargetKind, HermesTargetName};
+
+    #[test]
+    fn test_llbc_file_name_collision() {
+        let name_lib = HermesTargetName {
+            package_name: PackageName::new("pkg".to_string()),
+            target_name: "name".to_string(),
+            kind: HermesTargetKind::Lib,
+        };
+
+        let artifact_lib = HermesArtifact {
+            name: name_lib,
+            target_kind: HermesTargetKind::Lib,
+            manifest_path: PathBuf::from("Cargo.toml"),
+            start_from: vec![],
+        };
+
+        let name_bin = HermesTargetName {
+            package_name: PackageName::new("pkg".to_string()),
+            target_name: "name".to_string(),
+            kind: HermesTargetKind::Bin,
+        };
+
+        let artifact_bin = HermesArtifact {
+            name: name_bin,
+            target_kind: HermesTargetKind::Bin,
+            manifest_path: PathBuf::from("Cargo.toml"),
+            start_from: vec![],
+        };
+
+        // Verify that the file names are distinct, and that they're distinct
+        // *because of the trailing hash* (ie, that they have identical
+        // prefixes).
+        assert_ne!(artifact_lib.llbc_file_name(), artifact_bin.llbc_file_name());
+        assert!(artifact_lib.llbc_file_name().starts_with("pkg-name-"));
+        assert!(artifact_bin.llbc_file_name().starts_with("pkg-name-"));
+    }
+}
diff --git a/tools/hermes/src/ui_test_shim.rs b/tools/hermes/src/ui_test_shim.rs
index e118463701..b7c5866732 100644
--- a/tools/hermes/src/ui_test_shim.rs
+++ b/tools/hermes/src/ui_test_shim.rs
@@ -41,7 +41,7 @@ pub fn run() {
     let mut has_errors = false;
 
     // Ignore the returned source and module list; we only care about errors.
-    let _ = parse::read_file_and_scan_compilation_unit(&file_path, |source, res| {
+    let _ = parse::read_file_and_scan_compilation_unit(&file_path, false, |source, res| {
         if let Err(e) = res {
             has_errors = true;
             emit_rustc_json(&e, source, file_path.to_str().unwrap());
diff --git a/tools/hermes/tests/fixtures/complex_impl/expected_config.toml b/tools/hermes/tests/fixtures/complex_impl/expected_config.toml
index 538a595208..636f0e7f9f 100644
--- a/tools/hermes/tests/fixtures/complex_impl/expected_config.toml
+++ b/tools/hermes/tests/fixtures/complex_impl/expected_config.toml
@@ -1,3 +1,3 @@
 [[command]]
-args = ["--start-from", "crate::< * const Foo as T1 >::m1,crate::< [Foo ; 5] as T3 >::m3,crate::< [Foo] as T2 >::m2"]
+args = ["--start-from", "crate"]
 should_not_exist = false
diff --git a/tools/hermes/tests/fixtures/complex_impl/expected_status.txt b/tools/hermes/tests/fixtures/complex_impl/expected_status.txt
index 7a4059ef83..2e9ba477f8 100644
--- a/tools/hermes/tests/fixtures/complex_impl/expected_status.txt
+++ b/tools/hermes/tests/fixtures/complex_impl/expected_status.txt
@@ -1 +1 @@
-failure
+success
diff --git a/tools/hermes/tests/fixtures/const_block_blind_spot/expected_status.txt b/tools/hermes/tests/fixtures/const_block_blind_spot/expected_status.txt
new file mode 100644
index 0000000000..7a4059ef83
--- /dev/null
+++ b/tools/hermes/tests/fixtures/const_block_blind_spot/expected_status.txt
@@ -0,0 +1 @@
+failure
diff --git a/tools/hermes/tests/fixtures/const_block_blind_spot/expected_stderr.txt b/tools/hermes/tests/fixtures/const_block_blind_spot/expected_stderr.txt
new file mode 100644
index 0000000000..175e9828ff
--- /dev/null
+++ b/tools/hermes/tests/fixtures/const_block_blind_spot/expected_stderr.txt
@@ -0,0 +1,5 @@
+
+=== Hermes Verification Failed ===
+
+[Hermes Error] Nested item error: Hermes cannot verify items defined inside function bodies or other blocks.
+Error: Aborting due to 1 previous errors.
diff --git a/tools/hermes/tests/fixtures/const_block_blind_spot/hermes.toml b/tools/hermes/tests/fixtures/const_block_blind_spot/hermes.toml
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/tools/hermes/tests/fixtures/const_block_blind_spot/source/Cargo.toml b/tools/hermes/tests/fixtures/const_block_blind_spot/source/Cargo.toml
new file mode 100644
index 0000000000..0caa4ab49b
--- /dev/null
+++ b/tools/hermes/tests/fixtures/const_block_blind_spot/source/Cargo.toml
@@ -0,0 +1,4 @@
+[package]
+name = "const_blind_spot"
+version = "0.1.0"
+edition = "2021"
diff --git a/tools/hermes/tests/fixtures/const_block_blind_spot/source/src/lib.rs b/tools/hermes/tests/fixtures/const_block_blind_spot/source/src/lib.rs
new file mode 100644
index 0000000000..501de67d0d
--- /dev/null
+++ b/tools/hermes/tests/fixtures/const_block_blind_spot/source/src/lib.rs
@@ -0,0 +1,6 @@
+const _: () = {
+    /// ```lean
+    /// theorem hidden_impl : True := trivial
+    /// ```
+    pub fn hidden_impl() {}
+};
diff --git a/tools/hermes/tests/fixtures/cyclic_paths/expected_stderr.txt b/tools/hermes/tests/fixtures/cyclic_paths/expected_stderr.txt
new file mode 100644
index 0000000000..dd12fdf10b
--- /dev/null
+++ b/tools/hermes/tests/fixtures/cyclic_paths/expected_stderr.txt
@@ -0,0 +1,11 @@
+
+  × circular modules: src/lib.rs -> src/lib.rs
+   ╭─[[PROJECT_ROOT]/src/lib.rs:2:1]
+ 1 │ #[path = "lib.rs"]
+ 2 │ mod self_loop;
+   · ───────┬──────
+   ·        ╰── 
+ 3 │ 
+   ╰────
+
+Error: Diagnostic error in charon
diff --git a/tools/hermes/tests/fixtures/cyclic_paths/source/Cargo.toml b/tools/hermes/tests/fixtures/cyclic_paths/source/Cargo.toml
index c9d084f63a..26d0e1bd5f 100644
--- a/tools/hermes/tests/fixtures/cyclic_paths/source/Cargo.toml
+++ b/tools/hermes/tests/fixtures/cyclic_paths/source/Cargo.toml
@@ -2,5 +2,3 @@
 name = "cyclic_paths"
 version = "0.1.0"
 edition = "2021"
-
-[dependencies]
diff --git a/tools/hermes/tests/fixtures/cyclic_paths/source/src/lib.rs b/tools/hermes/tests/fixtures/cyclic_paths/source/src/lib.rs
index 03f8974b07..bffe02d000 100644
--- a/tools/hermes/tests/fixtures/cyclic_paths/source/src/lib.rs
+++ b/tools/hermes/tests/fixtures/cyclic_paths/source/src/lib.rs
@@ -1,5 +1,3 @@
-// This simulates a symlink loop by pointing a module declaration back at itself.
-// Without canonicalization, this causes a stack overflow.
 #[path = "lib.rs"]
 mod self_loop;
 
diff --git a/tools/hermes/tests/fixtures/double_mounted_mod/expected_config.toml b/tools/hermes/tests/fixtures/double_mounted_mod/expected_config.toml
new file mode 100644
index 0000000000..b9b5a16082
--- /dev/null
+++ b/tools/hermes/tests/fixtures/double_mounted_mod/expected_config.toml
@@ -0,0 +1,4 @@
+[[command]]
+# Assert that ONLY crate::a::s::proof is passed, and crate::b::s::proof is omitted
+args = ["--start-from", "crate::s1::proof,crate::s2::proof"]
+should_not_exist = false
diff --git a/tools/hermes/tests/fixtures/double_mounted_mod/expected_status.txt b/tools/hermes/tests/fixtures/double_mounted_mod/expected_status.txt
new file mode 100644
index 0000000000..2e9ba477f8
--- /dev/null
+++ b/tools/hermes/tests/fixtures/double_mounted_mod/expected_status.txt
@@ -0,0 +1 @@
+success
diff --git a/tools/hermes/tests/fixtures/double_mounted_mod/hermes.toml b/tools/hermes/tests/fixtures/double_mounted_mod/hermes.toml
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/tools/hermes/tests/fixtures/double_mounted_mod/source/Cargo.toml b/tools/hermes/tests/fixtures/double_mounted_mod/source/Cargo.toml
new file mode 100644
index 0000000000..9fd156bcb4
--- /dev/null
+++ b/tools/hermes/tests/fixtures/double_mounted_mod/source/Cargo.toml
@@ -0,0 +1,4 @@
+[package]
+name = "double_mounted"
+version = "0.1.0"
+edition = "2021"
diff --git a/tools/hermes/tests/fixtures/double_mounted_mod/source/src/lib.rs b/tools/hermes/tests/fixtures/double_mounted_mod/source/src/lib.rs
new file mode 100644
index 0000000000..8c668e6274
--- /dev/null
+++ b/tools/hermes/tests/fixtures/double_mounted_mod/source/src/lib.rs
@@ -0,0 +1,5 @@
+#[path = "shared.rs"]
+pub mod s1;
+
+#[path = "shared.rs"]
+pub mod s2;
diff --git a/tools/hermes/tests/fixtures/double_mounted_mod/source/src/shared.rs b/tools/hermes/tests/fixtures/double_mounted_mod/source/src/shared.rs
new file mode 100644
index 0000000000..38ef0edbd7
--- /dev/null
+++ b/tools/hermes/tests/fixtures/double_mounted_mod/source/src/shared.rs
@@ -0,0 +1,4 @@
+/// ```lean
+/// theorem proof : True := trivial
+/// ```
+pub fn proof() {}
diff --git a/tools/hermes/tests/fixtures/impl_fallback_dedup/expected_config.toml b/tools/hermes/tests/fixtures/impl_fallback_dedup/expected_config.toml
new file mode 100644
index 0000000000..34504b4d93
--- /dev/null
+++ b/tools/hermes/tests/fixtures/impl_fallback_dedup/expected_config.toml
@@ -0,0 +1,6 @@
+[[command]]
+# Assert that the start-from arg contains `crate::my_module` EXACTLY ONCE, 
+# proving that all inner items successfully fell back to the module,
+# and that `dedup()` successfully prevented string explosion.
+args = ["--start-from", "crate::my_module,crate::my_module::Bar"]
+should_not_exist = false
diff --git a/tools/hermes/tests/fixtures/impl_fallback_dedup/expected_status.txt b/tools/hermes/tests/fixtures/impl_fallback_dedup/expected_status.txt
new file mode 100644
index 0000000000..2e9ba477f8
--- /dev/null
+++ b/tools/hermes/tests/fixtures/impl_fallback_dedup/expected_status.txt
@@ -0,0 +1 @@
+success
diff --git a/tools/hermes/tests/fixtures/impl_fallback_dedup/hermes.toml b/tools/hermes/tests/fixtures/impl_fallback_dedup/hermes.toml
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/tools/hermes/tests/fixtures/impl_fallback_dedup/source/Cargo.toml b/tools/hermes/tests/fixtures/impl_fallback_dedup/source/Cargo.toml
new file mode 100644
index 0000000000..a95040c4f1
--- /dev/null
+++ b/tools/hermes/tests/fixtures/impl_fallback_dedup/source/Cargo.toml
@@ -0,0 +1,4 @@
+[package]
+name = "impl_fallback_dedup"
+version = "0.1.0"
+edition = "2021"
diff --git a/tools/hermes/tests/fixtures/impl_fallback_dedup/source/src/lib.rs b/tools/hermes/tests/fixtures/impl_fallback_dedup/source/src/lib.rs
new file mode 100644
index 0000000000..a901f8a162
--- /dev/null
+++ b/tools/hermes/tests/fixtures/impl_fallback_dedup/source/src/lib.rs
@@ -0,0 +1,22 @@
+pub mod my_module {
+    pub struct Foo;
+
+    impl Foo {
+        /// ```lean
+        /// theorem meth_one : True := trivial
+        /// ```
+        pub fn method_one() {}
+
+        /// ```lean
+        /// theorem meth_two : True := trivial
+        /// ```
+        pub fn method_two() {}
+    }
+
+    pub trait Bar {
+        /// ```lean
+        /// theorem trait_meth : True := trivial
+        /// ```
+        fn trait_method();
+    }
+}
diff --git a/tools/hermes/tests/fixtures/impl_path/expected_config.toml b/tools/hermes/tests/fixtures/impl_path/expected_config.toml
index d1048f47b6..4c54f4e040 100644
--- a/tools/hermes/tests/fixtures/impl_path/expected_config.toml
+++ b/tools/hermes/tests/fixtures/impl_path/expected_config.toml
@@ -1,4 +1,4 @@
 [[command]]
-# We assert that the path includes the Type Name "Foo"
-args = ["--start-from", "crate::Foo::bar"]
+# We target the module now due to fallback strategy
+args = ["--start-from", "crate"]
 should_not_exist = false
diff --git a/tools/hermes/tests/fixtures/macro_blind_spot/expected_status.txt b/tools/hermes/tests/fixtures/macro_blind_spot/expected_status.txt
new file mode 100644
index 0000000000..7a4059ef83
--- /dev/null
+++ b/tools/hermes/tests/fixtures/macro_blind_spot/expected_status.txt
@@ -0,0 +1 @@
+failure
diff --git a/tools/hermes/tests/fixtures/macro_blind_spot/expected_stderr.txt b/tools/hermes/tests/fixtures/macro_blind_spot/expected_stderr.txt
new file mode 100644
index 0000000000..faf13968de
--- /dev/null
+++ b/tools/hermes/tests/fixtures/macro_blind_spot/expected_stderr.txt
@@ -0,0 +1 @@
+No Hermes annotations
diff --git a/tools/hermes/tests/fixtures/macro_blind_spot/hermes.toml b/tools/hermes/tests/fixtures/macro_blind_spot/hermes.toml
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/tools/hermes/tests/fixtures/macro_blind_spot/source/Cargo.toml b/tools/hermes/tests/fixtures/macro_blind_spot/source/Cargo.toml
new file mode 100644
index 0000000000..f94e741790
--- /dev/null
+++ b/tools/hermes/tests/fixtures/macro_blind_spot/source/Cargo.toml
@@ -0,0 +1,4 @@
+[package]
+name = "macro_blind_spot"
+version = "0.1.0"
+edition = "2021"
diff --git a/tools/hermes/tests/fixtures/macro_blind_spot/source/src/lib.rs b/tools/hermes/tests/fixtures/macro_blind_spot/source/src/lib.rs
new file mode 100644
index 0000000000..86307a7a9e
--- /dev/null
+++ b/tools/hermes/tests/fixtures/macro_blind_spot/source/src/lib.rs
@@ -0,0 +1,9 @@
+macro_rules! make_proof {
+    () => {
+        /// ```lean
+        /// theorem hidden_proof : True := trivial
+        /// ```
+        pub fn hidden_proof() {}
+    }
+}
+make_proof!();
diff --git a/tools/hermes/tests/fixtures/nested_item_error/expected_stderr.txt b/tools/hermes/tests/fixtures/nested_item_error/expected_stderr.txt
index 32a0afc1c1..175e9828ff 100644
--- a/tools/hermes/tests/fixtures/nested_item_error/expected_stderr.txt
+++ b/tools/hermes/tests/fixtures/nested_item_error/expected_stderr.txt
@@ -1 +1,5 @@
-Nested item error
+
+=== Hermes Verification Failed ===
+
+[Hermes Error] Nested item error: Hermes cannot verify items defined inside function bodies or other blocks.
+Error: Aborting due to 1 previous errors.
diff --git a/tools/hermes/tests/fixtures/nested_out_of_line_mod/expected_status.txt b/tools/hermes/tests/fixtures/nested_out_of_line_mod/expected_status.txt
new file mode 100644
index 0000000000..7a4059ef83
--- /dev/null
+++ b/tools/hermes/tests/fixtures/nested_out_of_line_mod/expected_status.txt
@@ -0,0 +1 @@
+failure
diff --git a/tools/hermes/tests/fixtures/nested_out_of_line_mod/expected_stderr.txt b/tools/hermes/tests/fixtures/nested_out_of_line_mod/expected_stderr.txt
new file mode 100644
index 0000000000..175e9828ff
--- /dev/null
+++ b/tools/hermes/tests/fixtures/nested_out_of_line_mod/expected_stderr.txt
@@ -0,0 +1,5 @@
+
+=== Hermes Verification Failed ===
+
+[Hermes Error] Nested item error: Hermes cannot verify items defined inside function bodies or other blocks.
+Error: Aborting due to 1 previous errors.
diff --git a/tools/hermes/tests/fixtures/nested_out_of_line_mod/hermes.toml b/tools/hermes/tests/fixtures/nested_out_of_line_mod/hermes.toml
new file mode 100644
index 0000000000..e69de29bb2
diff --git a/tools/hermes/tests/fixtures/nested_out_of_line_mod/source/Cargo.toml b/tools/hermes/tests/fixtures/nested_out_of_line_mod/source/Cargo.toml
new file mode 100644
index 0000000000..acee787a64
--- /dev/null
+++ b/tools/hermes/tests/fixtures/nested_out_of_line_mod/source/Cargo.toml
@@ -0,0 +1,4 @@
+[package]
+name = "nested_out_of_line"
+version = "0.1.0"
+edition = "2021"
diff --git a/tools/hermes/tests/fixtures/nested_out_of_line_mod/source/src/hidden.rs b/tools/hermes/tests/fixtures/nested_out_of_line_mod/source/src/hidden.rs
new file mode 100644
index 0000000000..532cea8d15
--- /dev/null
+++ b/tools/hermes/tests/fixtures/nested_out_of_line_mod/source/src/hidden.rs
@@ -0,0 +1,4 @@
+/// ```lean
+/// theorem secret_proof : False := sorry
+/// ```
+pub fn secret_proof() {} 
diff --git a/tools/hermes/tests/fixtures/nested_out_of_line_mod/source/src/lib.rs b/tools/hermes/tests/fixtures/nested_out_of_line_mod/source/src/lib.rs
new file mode 100644
index 0000000000..ddd90f05a3
--- /dev/null
+++ b/tools/hermes/tests/fixtures/nested_out_of_line_mod/source/src/lib.rs
@@ -0,0 +1,11 @@
+pub fn outer_logic() {
+    // This module declaration is hidden inside a function.
+    // Hermes must NOT load `hidden.rs`.
+    #[path = "hidden.rs"]
+    mod hidden;
+}
+
+/// ```lean
+/// theorem valid_proof : True := trivial
+/// ```
+pub fn valid_proof() {} // Included so the crate has at least one valid proof to succeed.