diff --git a/README.md b/README.md
index 454eed6..009a45e 100644
--- a/README.md
+++ b/README.md
@@ -44,6 +44,27 @@ cargo dv verify --targets ostd --features irc11 -- \
   --verify-only-module sync::rcu
 ```
 
+### Line counting
+
+Line counting is a separate command from verification. Count a complete target
+using its latest Cargo/Verus dependency information:
+
+```bash
+cargo dv count --targets ostd
+```
+
+To count one Rust module (including file-based submodules), select exactly one
+target and pass the Verus module path:
+
+```bash
+cargo dv count --targets ostd --module sync::rwlock
+```
+
+The default output is a per-file summary. Add `--print-all` (or `-p`) to print
+every annotated source line. Whole-target counting requires dependency
+information from a previous `cargo dv verify` or `cargo dv build`; module
+counting resolves source files directly and does not require it.
+
 ## Bootstrapping Verus
 
 By default, `cargo dv bootstrap` builds the `main` branch of
diff --git a/src/count.rs b/src/count.rs
new file mode 100644
index 0000000..7b83de0
--- /dev/null
+++ b/src/count.rs
@@ -0,0 +1,410 @@
+use std::ffi::OsStr;
+use std::fs::{self, File, OpenOptions};
+use std::io::{BufRead, BufReader};
+use std::path::{Path, PathBuf};
+use std::process::Command;
+
+use crate::verus::{
+    self, get_target_dir, get_workspace_root, DynError, VerusTarget, VERIFICATION_RUST_TARGET,
+};
+
+fn dep_info_dirs(target_dir: &Path) -> Vec<PathBuf> {
+    [target_dir.join("verus-partial"), target_dir.to_path_buf()]
+        .into_iter()
+        .flat_map(|base| {
+            ["debug", "release"].into_iter().map(move |profile| {
+                base.join(VERIFICATION_RUST_TARGET)
+                    .join(profile)
+                    .join("deps")
+            })
+        })
+        .collect()
+}
+
+fn dep_info_source_root(
+    dep_info: &Path,
+    target: &VerusTarget,
+    workspace_root: &Path,
+) -> Option<PathBuf> {
+    let first_line = BufReader::new(File::open(dep_info).ok()?)
+        .lines()
+        .next()?
+        .ok()?;
+    let target_file = target.file.canonicalize().ok()?;
+
+    for root in [workspace_root, target.dir.as_path()] {
+        if first_line
+            .split_whitespace()
+            .skip(1)
+            .map(|dependency| dependency.trim_end_matches('\\'))
+            .map(Path::new)
+            .map(|dependency| {
+                if dependency.is_absolute() {
+                    dependency.to_path_buf()
+                } else {
+                    root.join(dependency)
+                }
+            })
+            .filter_map(|dependency| dependency.canonicalize().ok())
+            .any(|dependency| dependency == target_file)
+        {
+            return Some(root.to_path_buf());
+        }
+    }
+
+    None
+}
+
+fn find_dep_info(target: &VerusTarget) -> Option<(PathBuf, PathBuf)> {
+    let target_dir = get_target_dir();
+    let workspace_root = get_workspace_root();
+
+    dep_info_dirs(&target_dir)
+        .into_iter()
+        .filter_map(|dir| fs::read_dir(dir).ok())
+        .flatten()
+        .filter_map(|entry| entry.ok())
+        .map(|entry| entry.path())
+        .filter(|path| path.extension() == Some(OsStr::new("d")))
+        .filter_map(|path| {
+            let source_root = dep_info_source_root(&path, target, &workspace_root)?;
+            let modified = path.metadata().ok()?.modified().ok()?;
+            Some((modified, path, source_root))
+        })
+        .max_by_key(|(modified, _, _)| *modified)
+        .map(|(_, path, source_root)| (path, source_root))
+}
+
+struct TemporaryDepInfo {
+    path: PathBuf,
+}
+
+impl TemporaryDepInfo {
+    fn copy_into(source: &Path, root: &Path, crate_name: &str) -> Result<Self, DynError> {
+        for suffix in 0..100 {
+            let path = root.join(format!(
+                ".dv-line-count-{}-{}-{}.d",
+                crate_name,
+                std::process::id(),
+                suffix
+            ));
+            match OpenOptions::new().write(true).create_new(true).open(&path) {
+                Ok(mut destination) => {
+                    let temporary_dep_info = Self { path };
+                    let mut source = File::open(source)?;
+                    std::io::copy(&mut source, &mut destination)?;
+                    return Ok(temporary_dep_info);
+                }
+                Err(error) if error.kind() == std::io::ErrorKind::AlreadyExists => continue,
+                Err(error) => return Err(error.into()),
+            }
+        }
+
+        Err(format!(
+            "failed to create a temporary dep-info file in {}",
+            root.display()
+        )
+        .into())
+    }
+}
+
+impl Drop for TemporaryDepInfo {
+    fn drop(&mut self) {
+        if let Err(error) = fs::remove_file(&self.path) {
+            warn!(
+                "Failed to remove temporary dep-info file {}: {}",
+                self.path.display(),
+                error
+            );
+        }
+    }
+}
+
+fn line_count_command(print_all: bool) -> Command {
+    let mut command = Command::new("cargo");
+    command
+        .current_dir(verus::install::verus_dir().join("source/tools/line_count"))
+        .arg("run")
+        .arg("--release")
+        .arg("--");
+    if print_all {
+        command.arg("--print-all");
+    }
+    command
+}
+
+fn run_line_count(target: &VerusTarget, print_all: bool) -> Result<(), DynError> {
+    let (dep_info, source_root) = find_dep_info(target).ok_or_else(|| {
+        format!(
+            "could not find cargo-verus dep-info for target {} under {}; run `cargo dv verify --targets {}` first",
+            target.name,
+            get_target_dir().display(),
+            target.name
+        )
+    })?;
+    let temporary_dep_info = TemporaryDepInfo::copy_into(&dep_info, &source_root, &target.name)?;
+    println!("Counting lines for {}", target.name);
+    let status = line_count_command(print_all)
+        .arg("--deps")
+        .arg(&temporary_dep_info.path)
+        .status()?;
+    if !status.success() {
+        return Err(format!("line_count failed for target {}", target.name).into());
+    }
+
+    Ok(())
+}
+
+fn available_child_modules(source: &str) -> Vec<String> {
+    let Ok(file) = syn::parse_file(source) else {
+        return Vec::new();
+    };
+    let mut modules = file
+        .items
+        .into_iter()
+        .filter_map(|item| match item {
+            syn::Item::Mod(module) if module.content.is_none() => Some(module.ident.to_string()),
+            _ => None,
+        })
+        .collect::<Vec<_>>();
+    modules.sort();
+    modules.dedup();
+    modules
+}
+
+fn available_modules_message(source: &str, resolved: &[&str]) -> String {
+    let modules = available_child_modules(source);
+    if modules.is_empty() {
+        return String::new();
+    }
+
+    let prefix = if resolved.is_empty() {
+        String::new()
+    } else {
+        format!("{}::", resolved.join("::"))
+    };
+    format!(
+        "; available modules:\n{}",
+        modules
+            .iter()
+            .map(|module| format!("  {prefix}{module}"))
+            .collect::<Vec<_>>()
+            .join("\n")
+    )
+}
+
+fn module_source_paths(crate_root: &Path, module: &str) -> Result<Vec<PathBuf>, DynError> {
+    let segments = module
+        .split("::")
+        .map(|segment| segment.strip_prefix("r#").unwrap_or(segment))
+        .collect::<Vec<_>>();
+    if segments.is_empty()
+        || segments.iter().any(|segment| {
+            segment.is_empty()
+                || !segment
+                    .chars()
+                    .all(|ch| ch == '_' || ch.is_ascii_alphanumeric())
+        })
+    {
+        return Err(format!("invalid Rust module path `{module}`").into());
+    }
+
+    let mut current = crate_root.canonicalize()?;
+    for (index, segment) in segments.iter().enumerate() {
+        let parent = current
+            .parent()
+            .ok_or_else(|| format!("crate root {} has no parent", current.display()))?;
+        let source = fs::read_to_string(&current)?;
+        let path_pattern = regex::Regex::new(&format!(
+            r#"(?s)#\s*\[\s*path\s*=\s*"([^"]+)"\s*\](?:\s*#\s*\[[^\]]*\])*\s*(?:pub(?:\s*\([^)]*\))?\s+)?mod\s+{}\s*;"#,
+            regex::escape(segment)
+        ))?;
+        if let Some(path) = path_pattern
+            .captures(&source)
+            .and_then(|captures| captures.get(1))
+        {
+            let path = parent.join(path.as_str());
+            if !path.is_file() {
+                return Err(format!(
+                    "module `{module}` has #[path = {:?}], but {} is not a file",
+                    path.as_os_str(),
+                    path.display()
+                )
+                .into());
+            }
+            current = path.canonicalize()?;
+            continue;
+        }
+        let file_name = current
+            .file_name()
+            .and_then(OsStr::to_str)
+            .unwrap_or_default();
+        let base = if matches!(file_name, "lib.rs" | "main.rs" | "mod.rs") {
+            parent.to_path_buf()
+        } else {
+            parent.join(current.file_stem().unwrap_or_default())
+        };
+        let file_candidate = base.join(segment).with_extension("rs");
+        let mod_candidate = base.join(segment).join("mod.rs");
+        current = match (file_candidate.is_file(), mod_candidate.is_file()) {
+            (true, false) => file_candidate,
+            (false, true) => mod_candidate,
+            (false, false) => {
+                return Err(format!(
+                    "could not resolve module `{module}`: expected {} or {}{}",
+                    file_candidate.display(),
+                    mod_candidate.display(),
+                    available_modules_message(&source, &segments[..index])
+                )
+                .into());
+            }
+            (true, true) => {
+                return Err(format!(
+                    "module `{module}` is ambiguous: both {} and {} exist",
+                    file_candidate.display(),
+                    mod_candidate.display()
+                )
+                .into());
+            }
+        };
+    }
+
+    if current.file_name() == Some(OsStr::new("mod.rs")) {
+        return Ok(vec![current.parent().unwrap().to_path_buf()]);
+    }
+
+    let mut paths = vec![current.clone()];
+    let child_modules = current
+        .parent()
+        .unwrap()
+        .join(current.file_stem().unwrap_or_default());
+    if child_modules.is_dir() {
+        paths.push(child_modules);
+    }
+    Ok(paths)
+}
+
+fn run_module_line_count(
+    target: &VerusTarget,
+    module: &str,
+    print_all: bool,
+) -> Result<(), DynError> {
+    let module = module
+        .strip_prefix(&format!("{}::", target.name))
+        .unwrap_or(module);
+    let paths = module_source_paths(&target.file, module)?;
+
+    println!("Counting lines for {} module {}", target.name, module);
+    let status = line_count_command(print_all).args(&paths).status()?;
+    if !status.success() {
+        return Err(format!("line_count failed for {} module {}", target.name, module).into());
+    }
+    Ok(())
+}
+
+pub fn exec_count(
+    targets: &[VerusTarget],
+    module: Option<&str>,
+    print_all: bool,
+) -> Result<(), DynError> {
+    if module.is_some() && targets.len() != 1 {
+        return Err("--module requires exactly one --targets value".into());
+    }
+
+    let mut count_targets = if targets.is_empty() {
+        verus::verus_targets().into_values().collect::<Vec<_>>()
+    } else {
+        targets.to_vec()
+    };
+    count_targets.sort_by(|left, right| left.name.cmp(&right.name));
+
+    for target in &count_targets {
+        if let Some(module) = module {
+            run_module_line_count(target, module, print_all)?;
+        } else {
+            run_line_count(target, print_all)?;
+        }
+    }
+    Ok(())
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn resolves_a_leaf_module_to_its_source_file() {
+        let temp = tempfile::tempdir().unwrap();
+        let src = temp.path().join("src");
+        fs::create_dir_all(src.join("sync")).unwrap();
+        fs::write(src.join("lib.rs"), "mod sync;\n").unwrap();
+        fs::write(src.join("sync/mod.rs"), "mod rwlock;\n").unwrap();
+        fs::write(src.join("sync/rwlock.rs"), "struct RwLock;\n").unwrap();
+
+        let paths = module_source_paths(&src.join("lib.rs"), "sync::rwlock").unwrap();
+        assert_eq!(paths, [src.join("sync/rwlock.rs")]);
+    }
+
+    #[test]
+    fn resolves_a_parent_module_to_its_source_tree() {
+        let temp = tempfile::tempdir().unwrap();
+        let src = temp.path().join("src");
+        fs::create_dir_all(src.join("sync")).unwrap();
+        fs::write(src.join("lib.rs"), "mod sync;\n").unwrap();
+        fs::write(src.join("sync/mod.rs"), "mod rwlock;\n").unwrap();
+        fs::write(src.join("sync/rwlock.rs"), "struct RwLock;\n").unwrap();
+
+        let paths = module_source_paths(&src.join("lib.rs"), "sync").unwrap();
+        assert_eq!(paths, [src.join("sync")]);
+    }
+
+    #[test]
+    fn resolves_a_module_with_a_path_attribute() {
+        let temp = tempfile::tempdir().unwrap();
+        let src = temp.path().join("src");
+        fs::create_dir_all(src.join("arch/x86")).unwrap();
+        fs::write(
+            src.join("lib.rs"),
+            "#[path = \"arch/x86/mod.rs\"]\npub mod arch;\n",
+        )
+        .unwrap();
+        fs::write(src.join("arch/x86/mod.rs"), "mod irq;\n").unwrap();
+        fs::write(src.join("arch/x86/irq.rs"), "fn enable() {}\n").unwrap();
+
+        let paths = module_source_paths(&src.join("lib.rs"), "arch::irq").unwrap();
+        assert_eq!(paths, [src.join("arch/x86/irq.rs")]);
+    }
+
+    #[test]
+    fn unresolved_module_lists_available_module_paths() {
+        let temp = tempfile::tempdir().unwrap();
+        let src = temp.path().join("src");
+        fs::create_dir_all(src.join("sync")).unwrap();
+        fs::write(
+            src.join("lib.rs"),
+            "mod sync;\n// mod commented_out;\nmod task;\n",
+        )
+        .unwrap();
+        fs::write(src.join("sync/mod.rs"), "mod rwlock;\n").unwrap();
+
+        let error = module_source_paths(&src.join("lib.rs"), "sy")
+            .unwrap_err()
+            .to_string();
+        assert!(error.contains("available modules:\n  sync\n  task"));
+        assert!(!error.contains("commented_out"));
+    }
+
+    #[test]
+    fn unresolved_nested_module_lists_qualified_paths() {
+        let temp = tempfile::tempdir().unwrap();
+        let src = temp.path().join("src");
+        fs::create_dir_all(src.join("sync")).unwrap();
+        fs::write(src.join("lib.rs"), "mod sync;\n").unwrap();
+        fs::write(src.join("sync/mod.rs"), "mod mutex;\nmod rwlock;\n").unwrap();
+
+        let error = module_source_paths(&src.join("lib.rs"), "sync::rw")
+            .unwrap_err()
+            .to_string();
+        assert!(error.contains("available modules:\n  sync::mutex\n  sync::rwlock"));
+    }
+}
diff --git a/src/lib.rs b/src/lib.rs
index f55f3cb..7116530 100644
--- a/src/lib.rs
+++ b/src/lib.rs
@@ -6,6 +6,7 @@ pub mod files;
 pub mod console;
 pub mod commands;
 pub mod config;
+pub mod count;
 pub mod dep_tree;
 pub mod doc;
 pub mod format;
diff --git a/src/main.rs b/src/main.rs
index ffbc94b..33482d3 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -24,6 +24,13 @@ enum Commands {
     )]
     Verify(VerifyArgs),
 
+    #[command(
+        name = "count",
+        about = "Count Verus source lines by target or module",
+        alias = "cnt"
+    )]
+    Count(CountArgs),
+
     #[command(
         name = "doc",
         about = "Generate documentation for the verification targets"
@@ -187,15 +194,6 @@ struct VerifyArgs {
     )]
     focus: bool,
 
-    #[arg(
-        short = 'c',
-        long = "count-line",
-        help = "Count the number of lines of code",
-        default_value = "false",
-        action = ArgAction::SetTrue
-    )]
-    count_line: bool,
-
     #[command(flatten, next_help_heading = "Cargo feature options")]
     cargo_features: clap_cargo::Features,
 
@@ -209,6 +207,36 @@ struct VerifyArgs {
     verus_args: Vec<String>,
 }
 
+#[derive(Parser, Debug)]
+struct CountArgs {
+    #[arg(
+        short = 't',
+        long = "targets",
+        value_parser = verus::find_target,
+        help = "The targets to count",
+        num_args = 0..,
+        action = ArgAction::Append
+    )]
+    targets: Vec<VerusTarget>,
+
+    #[arg(
+        short = 'm',
+        long = "module",
+        value_name = "MODULE_PATH",
+        help = "Count only this module and its file-based submodules (for example, sync::rwlock)"
+    )]
+    module: Option<String>,
+
+    #[arg(
+        short = 'p',
+        long = "print-all",
+        help = "Print every annotated source line",
+        default_value = "false",
+        action = ArgAction::SetTrue
+    )]
+    print_all: bool,
+}
+
 #[derive(Parser, Debug)]
 struct DocArgs {
     #[arg(
@@ -447,13 +475,16 @@ fn verify(args: &VerifyArgs) -> Result<(), DynError> {
         disasm: false,
         cargo_args: cargo_feature_args(&args.cargo_features),
         verus_args: args.verus_args.clone(),
-        count_line: args.count_line,
         focus: args.focus,
     };
 
     verus::exec_verify(&targets, &options)
 }
 
+fn count(args: &CountArgs) -> Result<(), DynError> {
+    count::exec_count(&args.targets, args.module.as_deref(), args.print_all)
+}
+
 fn doc(args: &DocArgs) -> Result<(), DynError> {
     doc::exec_doc(
         &args.target,
@@ -490,7 +521,6 @@ fn build(args: &BuildArgs) -> Result<(), DynError> {
         disasm: args.disasm,
         cargo_args: cargo_feature_args(&args.cargo_features),
         verus_args: args.verus_args.clone(),
-        count_line: false,
         focus: false,
     };
 
@@ -565,6 +595,7 @@ fn main() {
     let cli = Cli::parse();
     if let Err(e) = match &cli.command {
         Commands::Verify(args) => verify(args),
+        Commands::Count(args) => count(args),
         Commands::Doc(args) => doc(args),
         Commands::Bootstrap(args) => bootstrap(args),
         Commands::Build(args) => build(args),
@@ -574,7 +605,7 @@ fn main() {
         Commands::Format(args) => format(args),
         Commands::Clean(args) => clean(args),
     } {
-        error!("Error when executing command `{:?}`: {}", cli.command, e);
+        error!("Error: {}", e);
     }
 }
 
@@ -620,6 +651,19 @@ mod tests {
         assert!(args.verus_args.is_empty());
     }
 
+    #[test]
+    fn count_accepts_a_module_and_print_all() {
+        let cli = Cli::try_parse_from(["dv", "count", "--module", "sync::rwlock", "--print-all"])
+            .unwrap();
+
+        let Commands::Count(args) = cli.command else {
+            panic!("expected count command");
+        };
+        assert!(args.targets.is_empty());
+        assert_eq!(args.module.as_deref(), Some("sync::rwlock"));
+        assert!(args.print_all);
+    }
+
     #[test]
     fn bootstrap_accepts_upstream_irc11_build_argument() {
         let cli = Cli::try_parse_from([
diff --git a/src/verus.rs b/src/verus.rs
index b979b7d..046bf2b 100644
--- a/src/verus.rs
+++ b/src/verus.rs
@@ -195,8 +195,6 @@ pub struct ExtraOptions {
     pub cargo_args: Vec<String>,
     /// pass-through options to the Verus verifier
     pub verus_args: Vec<String>,
-    /// count lines of code
-    pub count_line: bool,
     /// use cargo-verus focus instead of cargo-verus verify
     pub focus: bool,
 }
@@ -612,12 +610,6 @@ fn move_verus_log_files(crate_name: &str) {
 }
 
 pub fn exec_verify(targets: &[VerusTarget], options: &ExtraOptions) -> Result<(), DynError> {
-    if options.count_line {
-        eprintln!("Error: --count-line is currently unsupported with cargo-verus");
-        // TODO: Re-enable this path once cargo-verus can produce the dep-info expected by Verus' line_count tool.
-        return Err("--count-line is currently unsupported with cargo-verus".into());
-    }
-
     let z3 = get_z3();
     let run = |target: Option<&VerusTarget>| -> Result<(), DynError> {
         let ts_start = Instant::now();
@@ -643,9 +635,6 @@ pub fn exec_verify(targets: &[VerusTarget], options: &ExtraOptions) -> Result<()
             cmd.env("RUST_BACKTRACE", "full");
             verus_args.push("--trace".to_string());
         }
-        if options.count_line {
-            verus_args.push("--emit=dep-info".to_string());
-        }
         verus_args.push(format!("--multiple-errors={}", options.max_errors));
         verus_args.extend(options.verus_args.clone());
         push_verus_args(cmd, &verus_args);
@@ -690,28 +679,6 @@ pub fn exec_verify(targets: &[VerusTarget], options: &ExtraOptions) -> Result<()
             );
         }
 
-        if options.count_line {
-            let verus_root = install::verus_dir();
-            let line_count_dir = verus_root.join("source/tools/line_count");
-            let current_dir = std::env::current_dir()?;
-            let dependency_file = current_dir.join("lib.d");
-            std::env::set_current_dir(&line_count_dir)?;
-            let mut cargo_cmd = Command::new("cargo");
-            cargo_cmd
-                .arg("run")
-                .arg("--release")
-                .arg(&dependency_file)
-                .arg("-p");
-
-            println!(
-                "Counting lines for {}",
-                target.map(|t| t.name.as_str()).unwrap_or("workspace")
-            );
-            let line_count_result = cargo_cmd.status();
-            std::env::set_current_dir(current_dir)?;
-            line_count_result?;
-            fs::remove_file(&dependency_file)?;
-        }
         Ok(())
     };