diff --git a/src/commands.rs b/src/commands.rs
index de7966e..23460ca 100644
--- a/src/commands.rs
+++ b/src/commands.rs
@@ -269,22 +269,22 @@ impl CargoBuildExterns {
         full
     }
 
-    pub fn parse_from_build_log(package: &str, stdout: &str, stderr: &str) -> Self {
+    pub fn parse_from_build_log(crate_name: &str, stdout: &str, stderr: &str) -> Self {
         let mut cargo_build = CargoBuildExterns::new(true);
         cargo_build.parse_library(stdout);
-        cargo_build.parse_last_level(package, stderr);
+        cargo_build.parse_last_level(crate_name, stderr);
         cargo_build
     }
 
-    pub fn parse_last_level(&mut self, package: &str, stderr: &str) {
+    pub fn parse_last_level(&mut self, crate_name: &str, stderr: &str) {
         let rustc_regex =
             Regex::new(r"^\s+Running\s+`.*rustc\s+.*--crate-name\s+(\S+)\s+.*$").unwrap();
         let extern_regex = Regex::new(r"--extern\s+([^=\s]+)=([^\s]+)").unwrap();
 
         for line in stderr.lines() {
             if let Some(caps) = rustc_regex.captures(line) {
-                let crate_name = caps.get(1).unwrap().as_str();
-                if crate_name != package {
+                let line_crate = caps.get(1).unwrap().as_str();
+                if line_crate != crate_name {
                     continue;
                 }
             }
@@ -352,6 +352,7 @@ impl CargoBuildExterns {
 /// But the package itself is not required to be built.
 pub fn cargo_build_resolve_deps(
     package: &str,
+    crate_name: &str,
     env: &HashMap<String, String>,
     release: bool,
 ) -> CargoBuildExterns {
@@ -377,7 +378,7 @@ pub fn cargo_build_resolve_deps(
         .arg(crate::verus::VERIFICATION_RUST_TARGET);
 
     let res = run_build_log_capture(&mut cmd);
-    CargoBuildExterns::parse_from_build_log(package, res.stdout.as_str(), res.stderr.as_str())
+    CargoBuildExterns::parse_from_build_log(crate_name, res.stdout.as_str(), res.stderr.as_str())
 }
 
 pub fn cargo_build(package: &str, env: &HashMap<String, String>, release: bool) {
diff --git a/src/count.rs b/src/count.rs
index 7b83de0..e7c6109 100644
--- a/src/count.rs
+++ b/src/count.rs
@@ -290,7 +290,8 @@ fn run_module_line_count(
     print_all: bool,
 ) -> Result<(), DynError> {
     let module = module
-        .strip_prefix(&format!("{}::", target.name))
+        .strip_prefix(&format!("{}::", target.crate_name))
+        .or_else(|| module.strip_prefix(&format!("{}::", target.name)))
         .unwrap_or(module);
     let paths = module_source_paths(&target.file, module)?;
 
diff --git a/src/doc.rs b/src/doc.rs
index 6f57231..40149db 100644
--- a/src/doc.rs
+++ b/src/doc.rs
@@ -137,11 +137,14 @@ fn generate_single_target_doc(
     // Add dependencies that this target actually needs
     let deps = verus::get_local_dependency(target);
     for (_name, dep_target) in deps.iter() {
-        if dep_target.name != target.name {
-            if let Some(rlib_path) = find_local_dependency_rlib(&target_dir, &dep_target.name) {
-                let extern_name = dep_target.name.replace('-', "_");
-                cmd.arg("--extern")
-                    .arg(format!("{}={}", extern_name, rlib_path.display()));
+        if dep_target.crate_name != target.crate_name {
+            if let Some(rlib_path) = find_local_dependency_rlib(&target_dir, &dep_target.crate_name)
+            {
+                cmd.arg("--extern").arg(format!(
+                    "{}={}",
+                    dep_target.crate_name,
+                    rlib_path.display()
+                ));
             } else {
                 return Err(format!(
                     "Missing built dependency '{}' for target '{}'.\n\nPlease run:\n  cargo dv build",
@@ -217,7 +220,7 @@ fn generate_single_target_doc(
 
     // Set crate type and name
     cmd.arg("--crate-type=lib")
-        .arg(format!("--crate-name={}", target.name.replace('-', "_")));
+        .arg(format!("--crate-name={}", target.crate_name));
 
     if json_output {
         cmd.arg("--output-format").arg("json");
diff --git a/src/pre_commit.rs b/src/pre_commit.rs
index 35afeec..ca106df 100644
--- a/src/pre_commit.rs
+++ b/src/pre_commit.rs
@@ -21,7 +21,9 @@ fn main() {
     let mut found_errors = false;
     for (vt, t) in targets.iter() {
         let verus_target = t.root_file();
-        let package = members.get(vt).unwrap_or_else(|| {
+        // `targets` is keyed by crate identifier; metadata packages are keyed
+        // by the manifest package name.
+        let package = members.get(&t.name).unwrap_or_else(|| {
             fatal!("Unable to find target {} in metadata", vt);
         });
 
@@ -36,7 +38,7 @@ fn main() {
         if verus_target == cargo_target {
             warn!("Target [{}] has cargo target source path `{}` which is the same as the Verus target.\n\
                    Consider change `path=...` in `{}` to `path=src/.dummy.rs` to avoid build errors.",
-                   vt, cargo_target, package.manifest_path);
+                   t.name, cargo_target, package.manifest_path);
             found_errors = true;
         }
     }
diff --git a/src/verus.rs b/src/verus.rs
index 8bc9f41..80c03f1 100644
--- a/src/verus.rs
+++ b/src/verus.rs
@@ -159,8 +159,11 @@ pub struct VerusDependency {
 
 #[derive(Clone, Debug, PartialEq, Eq, Hash)]
 pub struct VerusTarget {
-    /// name of the package
+    /// name of the package, as declared in `Cargo.toml` (e.g. `id-alloc`)
     pub name: String,
+    /// crate identifier of the package (e.g. `id_alloc`); differs from `name`
+    /// for packages with hyphens
+    pub crate_name: String,
     /// version of the package
     pub version: String,
     /// directory of the package
@@ -250,7 +253,7 @@ impl VerusTarget {
 
     pub fn library_proof(&self) -> PathBuf {
         get_target_dir()
-            .join(format!("{}.verusdata", self.name))
+            .join(format!("{}.verusdata", self.crate_name))
             .to_path_buf()
     }
 
@@ -258,7 +261,7 @@ impl VerusTarget {
         let lib = format!(
             "{}{}.{}",
             self.library_prefix(),
-            self.name,
+            self.crate_name,
             self.library_suffix()
         );
         get_target_dir().join(lib).to_path_buf()
@@ -357,7 +360,8 @@ pub fn verus_targets() -> HashMap<String, VerusTarget> {
 
         // check if the package has a target
         if let Some(target) = package.targets.first() {
-            let name = package.name.as_str().replace('-', "_");
+            let name = package.name.as_str().to_string();
+            let crate_name = name.replace('-', "_");
             let version = package.version.to_string();
             let dir = Path::new(&package.manifest_path)
                 .parent()
@@ -386,9 +390,10 @@ pub fn verus_targets() -> HashMap<String, VerusTarget> {
             let features = extract_features(package, ws_features.as_slice());
 
             targets.insert(
-                name.clone(),
+                crate_name.clone(),
                 VerusTarget {
                     name,
+                    crate_name,
                     version,
                     dir,
                     file,
@@ -410,8 +415,11 @@ pub fn verus_targets() -> HashMap<String, VerusTarget> {
 pub fn find_target(t: &str) -> Result<VerusTarget, String> {
     let all = verus_targets();
     let s = files::dir_as_package(t);
+    // Target names are keyed by crate identifier (`-` -> `_`); accept both
+    // spellings so users can pass the package name as well.
+    let key = s.replace('-', "_");
 
-    let target = all.get(&s).cloned().unwrap_or_else(|| {
+    let target = all.get(&key).cloned().unwrap_or_else(|| {
         error!(
             "Cannot find target {}\n\n  Targets available:\n{}",
             t,
@@ -435,12 +443,13 @@ fn get_local_dependency_direct(target: &VerusTarget) -> IndexMap<String, VerusTa
             // Not a local path dependency
             continue;
         }
-        if !all.contains_key(dep.name.as_str()) {
+        let dep_key = dep.name.replace('-', "_");
+        if !all.contains_key(&dep_key) {
             // Not in current workspace
             continue;
         }
-        let dep_target = all.get(dep.name.as_str()).unwrap();
-        deps.insert(dep.name.clone(), dep_target.clone());
+        let dep_target = all.get(&dep_key).unwrap();
+        deps.insert(dep_key, dep_target.clone());
     }
 
     deps
@@ -456,7 +465,7 @@ pub fn get_local_dependency(target: &VerusTarget) -> IndexMap<String, VerusTarge
         visited: &mut std::collections::HashSet<String>,
         _is_root: bool,
     ) {
-        let target_name = target.name.replace('-', "_");
+        let target_name = target.crate_name.clone();
 
         // Prevent infinite recursion
         if visited.contains(&target_name) {
@@ -469,9 +478,8 @@ pub fn get_local_dependency(target: &VerusTarget) -> IndexMap<String, VerusTarge
 
         // Add direct dependencies to result (unless it's the root target)
         for (dep_name, dep_target) in direct_deps.iter() {
-            let dep_key = dep_name.replace('-', "_");
-            if !result.contains_key(&dep_key) {
-                result.insert(dep_key, dep_target.clone());
+            if !result.contains_key(dep_name) {
+                result.insert(dep_name.clone(), dep_target.clone());
             }
             // Recursively collect dependencies of this dependency
             collect_deps_recursively(dep_target, result, visited, false);
@@ -489,7 +497,7 @@ pub fn get_remote_dependency(target: &VerusTarget, release: bool) -> IndexMap<St
 
     let local_verus = verus_targets()
         .values()
-        .map(|t| t.name.replace('-', "_"))
+        .map(|t| t.crate_name.clone())
         .collect::<HashSet<_>>();
 
     for (name, path) in externs.iter() {
@@ -546,7 +554,12 @@ pub fn resolve_deps(target: &VerusTarget, release: bool) -> CargoBuildExterns {
     let dummy_rs = target.dir.join("src").join(".dummy.rs");
     files::touch(&dummy_rs.to_string_lossy());
 
-    let mut externs = commands::cargo_build_resolve_deps(&target.name, &HashMap::new(), release);
+    let mut externs = commands::cargo_build_resolve_deps(
+        &target.name,
+        &target.crate_name,
+        &HashMap::new(),
+        release,
+    );
 
     if externs.deps_ready {
         reorder_deps(target, &mut externs);
@@ -682,7 +695,7 @@ pub fn exec_verify(targets: &[VerusTarget], options: &ExtraOptions) -> Result<()
 
             if options.log && target.is_some() {
                 let target = target.unwrap();
-                move_verus_log_files(&target.name);
+                move_verus_log_files(&target.crate_name);
             }
         } else {
             error!(