diff --git a/Cargo.lock b/Cargo.lock
index 8dae72b6c89..83b8d509325 100644
--- a/Cargo.lock
+++ b/Cargo.lock
@@ -866,6 +866,19 @@ dependencies = [
  "serde_core",
 ]
 
+[[package]]
+name = "indicatif"
+version = "0.18.3"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "9375e112e4b463ec1b1c6c011953545c65a30164fbab5b581df32b3abf0dcb88"
+dependencies = [
+ "console",
+ "portable-atomic",
+ "unicode-width",
+ "unit-prefix",
+ "web-time",
+]
+
 [[package]]
 name = "indoc"
 version = "2.0.7"
@@ -1002,6 +1015,7 @@ dependencies = [
  "clap",
  "comfy-table",
  "console",
+ "indicatif",
  "kani_metadata",
  "once_cell",
  "pathdiff",
@@ -2377,6 +2391,12 @@ version = "0.2.2"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "b4ac048d71ede7ee76d585517add45da530660ef4390e49b098733c6e897f254"
 
+[[package]]
+name = "unit-prefix"
+version = "0.5.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "81e544489bf3d8ef66c953931f56617f423cd4b5494be343d9b9d3dda037b9a3"
+
 [[package]]
 name = "unsafe-libyaml"
 version = "0.2.11"
@@ -2480,6 +2500,16 @@ dependencies = [
  "unicode-ident",
 ]
 
+[[package]]
+name = "web-time"
+version = "1.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5a6580f308b1fad9207618087a65c04e7a10bc77e02c8e84e9b00dd4b12fa0bb"
+dependencies = [
+ "js-sys",
+ "wasm-bindgen",
+]
+
 [[package]]
 name = "which"
 version = "7.0.3"
diff --git a/kani-driver/Cargo.toml b/kani-driver/Cargo.toml
index f0e886c31d1..3ced7b50177 100644
--- a/kani-driver/Cargo.toml
+++ b/kani-driver/Cargo.toml
@@ -36,6 +36,7 @@ which = "8"
 time = {version = "0.3.47", features = ["formatting"]}
 tokio = { version = "1.40.0", features = ["io-util", "process", "rt", "time"] }
 chrono = { version = "0.4.41", default-features = false, features = [ "clock" ]}
+indicatif = "0.18"
 
 
 # A good set of suggested dependencies can be found in rustup:
diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs
index f7aef031f47..a00ae27f1b4 100644
--- a/kani-driver/src/args/mod.rs
+++ b/kani-driver/src/args/mod.rs
@@ -326,6 +326,12 @@ pub struct VerificationArgs {
     #[arg(long, hide_short_help = true)]
     pub output_into_files: bool,
 
+    /// Write verbose and terse log output to the specified file.
+    /// When enabled with an interactive terminal, progress indicator will be shown on terminal
+    /// while detailed logs are written to the file.
+    #[arg(long, value_name = "PATH")]
+    pub log_file: Option<PathBuf>,
+
     /// Print final LLBC for Lean backend. This requires the `-Z lean` option.
     #[arg(long, hide = true)]
     pub print_llbc: bool,
diff --git a/kani-driver/src/call_cbmc.rs b/kani-driver/src/call_cbmc.rs
index 3eeede9f68e..7c3891798dd 100644
--- a/kani-driver/src/call_cbmc.rs
+++ b/kani-driver/src/call_cbmc.rs
@@ -129,6 +129,7 @@ impl KaniSession {
                         self.args.extra_pointer_checks,
                         self.args.common_args.quiet,
                         &self.args.output_format,
+                        self.args.log_file.as_ref(),
                     )
                 }),
             )
@@ -140,6 +141,7 @@ impl KaniSession {
                     self.args.extra_pointer_checks,
                     self.args.common_args.quiet,
                     &self.args.output_format,
+                    self.args.log_file.as_ref(),
                 )
             })
             .await)
diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs
index a64562d5116..cf8f3a693d1 100644
--- a/kani-driver/src/cbmc_property_renderer.rs
+++ b/kani-driver/src/cbmc_property_renderer.rs
@@ -10,6 +10,9 @@ use once_cell::sync::Lazy;
 use regex::Regex;
 use rustc_demangle::demangle;
 use std::collections::HashMap;
+use std::fs::OpenOptions;
+use std::io::Write;
+use std::path::PathBuf;
 
 type CbmcAltDescriptions = HashMap<&'static str, Vec<(&'static str, Option<&'static str>)>>;
 
@@ -165,12 +168,14 @@ impl ParserItem {
 /// filter and transform it into the format we expect.
 ///
 /// This will output "messages" live as they stream in if `output_format` is
-/// set to `regular` but will otherwise not print.
+/// set to `regular` but will otherwise not print. When a log file path is provided, output is
+/// redirected to the log file instead.
 pub fn kani_cbmc_output_filter(
     item: ParserItem,
     extra_ptr_checks: bool,
     quiet: bool,
     output_format: &OutputFormat,
+    log_file: Option<&PathBuf>,
 ) -> Option<ParserItem> {
     // Some items (e.g., messages) are skipped.
     // We could also process them and decide to skip later.
@@ -183,7 +188,17 @@ pub fn kani_cbmc_output_filter(
     if !quiet {
         let formatted_item = format_item(&processed_item, output_format);
         if let Some(fmt_item) = formatted_item {
-            println!("{fmt_item}");
+            if let Some(log_path) = log_file {
+                if let Err(e) = write_to_log_file(log_path, &fmt_item) {
+                    eprintln!(
+                        "Failed to write CBMC output to log file {}: {}",
+                        log_path.display(),
+                        e
+                    );
+                }
+            } else {
+                println!("{fmt_item}");
+            }
         }
     }
     // TODO: Record processed items and dump them into a JSON file
@@ -191,6 +206,12 @@ pub fn kani_cbmc_output_filter(
     Some(processed_item)
 }
 
+/// Helper function to write output to log file
+fn write_to_log_file(log_file_path: &PathBuf, content: &str) -> std::io::Result<()> {
+    let mut file = OpenOptions::new().create(true).append(true).open(log_file_path)?;
+    writeln!(file, "{}", content)
+}
+
 /// Processes a `ParserItem`. In general, all items are returned as they are,
 /// except for:
 ///  * Error messages, which may be edited.
diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs
index 708a4064cd7..f097aa78a48 100644
--- a/kani-driver/src/harness_runner.rs
+++ b/kani-driver/src/harness_runner.rs
@@ -5,11 +5,12 @@ use anyhow::{Error, Result, bail};
 use kani_metadata::{ArtifactType, HarnessKind, HarnessMetadata};
 use rayon::prelude::*;
 use std::fs::File;
-use std::io::Write;
+use std::io::{IsTerminal, Write};
 use std::path::Path;
 
 use crate::args::{NumThreads, OutputFormat};
 use crate::call_cbmc::{VerificationResult, VerificationStatus};
+use crate::progress_indicator::ProgressIndicator;
 use crate::project::Project;
 use crate::session::{BUG_REPORT_URL, KaniSession};
 
@@ -56,6 +57,15 @@ impl<'pr> HarnessRunner<'_, 'pr> {
         harnesses: &'pr [&HarnessMetadata],
     ) -> Result<Vec<HarnessResult<'pr>>> {
         let sorted_harnesses = crate::metadata::sort_harnesses_by_loc(harnesses);
+
+        // Determine if we should show progress indicator
+        let show_progress = self.sess.args.log_file.is_some()
+            && !self.sess.args.common_args.quiet
+            && std::io::stdout().is_terminal();
+
+        // Create progress indicator
+        let progress_indicator = ProgressIndicator::new(sorted_harnesses.len(), show_progress);
+
         let pool = {
             let mut builder = rayon::ThreadPoolBuilder::new();
             match self.sess.args.jobs() {
@@ -86,6 +96,15 @@ impl<'pr> HarnessRunner<'_, 'pr> {
                     }
 
                     let result = self.sess.check_harness(goto_file, harness)?;
+
+                    // Update progress indicator if active
+                    if progress_indicator.is_active() {
+                        let succeeded = result.status == VerificationStatus::Success;
+                        let timed_out =
+                            matches!(&result.results, Err(crate::call_cbmc::ExitStatus::Timeout));
+                        progress_indicator.update_with_result(succeeded, timed_out);
+                    }
+
                     if self.sess.args.fail_fast && result.status == VerificationStatus::Failure {
                         Err(Error::new(FailFastHarnessInfo {
                             index_to_failing_harness: idx,
@@ -97,6 +116,10 @@ impl<'pr> HarnessRunner<'_, 'pr> {
                 })
                 .collect::<Result<Vec<_>>>()
         });
+
+        // Finish progress indicator
+        progress_indicator.finish();
+
         match results {
             Ok(results) => Ok(results),
             Err(err) => {
@@ -127,14 +150,40 @@ impl KaniSession {
             }
 
             let output = result.render(&self.args.output_format, harness.attributes.should_panic);
-            if rayon::current_num_threads() > 1 {
-                println!("Thread {thread_index}: {output}");
+
+            // If log file is specified, write to log file instead of stdout
+            if let Some(ref log_file_path) = self.args.log_file {
+                self.write_to_log_file(log_file_path, &output, thread_index);
             } else {
-                println!("{output}");
+                // Normal stdout output
+                if rayon::current_num_threads() > 1 {
+                    println!("Thread {thread_index}: {output}");
+                } else {
+                    println!("{output}");
+                }
             }
         }
     }
 
+    fn write_to_log_file(&self, log_file_path: &PathBuf, output: &str, thread_index: usize) {
+        use std::fs::OpenOptions;
+
+        let result = OpenOptions::new().create(true).append(true).open(log_file_path).and_then(
+            |mut file| {
+                let formatted_output = if rayon::current_num_threads() > 1 {
+                    format!("Thread {thread_index}: {output}\n")
+                } else {
+                    format!("{output}\n")
+                };
+                file.write_all(formatted_output.as_bytes())
+            },
+        );
+
+        if let Err(e) = result {
+            eprintln!("Failed to write to log file {}: {}", log_file_path.display(), e);
+        }
+    }
+
     fn should_print_output(&self) -> bool {
         !self.args.common_args.quiet && self.args.output_format != OutputFormat::Old
     }
@@ -201,7 +250,12 @@ impl KaniSession {
                 msg = format!("Thread {thread_index}: {msg}");
             }
 
-            println!("{msg}");
+            // Write to log file if specified, otherwise to stdout
+            if let Some(ref log_file_path) = self.args.log_file {
+                self.write_to_log_file(log_file_path, &msg, thread_index);
+            } else {
+                println!("{msg}");
+            }
         }
 
         let mut result = self.with_timer(|| self.run_cbmc(binary, harness), "run_cbmc")?;
diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs
index 21b74e8672c..3f602ab1f27 100644
--- a/kani-driver/src/main.rs
+++ b/kani-driver/src/main.rs
@@ -35,6 +35,7 @@ mod coverage;
 mod harness_runner;
 mod list;
 mod metadata;
+mod progress_indicator;
 mod project;
 mod session;
 mod util;
diff --git a/kani-driver/src/progress_indicator.rs b/kani-driver/src/progress_indicator.rs
new file mode 100644
index 00000000000..3c0b4ba5e00
--- /dev/null
+++ b/kani-driver/src/progress_indicator.rs
@@ -0,0 +1,146 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Progress indicator for verification harness execution
+
+use indicatif::{ProgressBar, ProgressStyle};
+use std::sync::Arc;
+use std::sync::atomic::{AtomicUsize, Ordering};
+
+/// Tracks statistics for harness verification progress
+#[derive(Debug, Clone)]
+pub struct VerificationStats {
+    pub total: usize,
+    pub completed: Arc<AtomicUsize>,
+    pub succeeded: Arc<AtomicUsize>,
+    pub failed: Arc<AtomicUsize>,
+    pub timed_out: Arc<AtomicUsize>,
+}
+
+impl VerificationStats {
+    pub fn new(total: usize) -> Self {
+        Self {
+            total,
+            completed: Arc::new(AtomicUsize::new(0)),
+            succeeded: Arc::new(AtomicUsize::new(0)),
+            failed: Arc::new(AtomicUsize::new(0)),
+            timed_out: Arc::new(AtomicUsize::new(0)),
+        }
+    }
+
+    pub fn increment_completed(&self) {
+        self.completed.fetch_add(1, Ordering::SeqCst);
+    }
+
+    pub fn increment_succeeded(&self) {
+        self.succeeded.fetch_add(1, Ordering::SeqCst);
+    }
+
+    pub fn increment_failed(&self) {
+        self.failed.fetch_add(1, Ordering::SeqCst);
+    }
+
+    pub fn increment_timed_out(&self) {
+        self.timed_out.fetch_add(1, Ordering::SeqCst);
+    }
+
+    pub fn get_completed(&self) -> usize {
+        self.completed.load(Ordering::SeqCst)
+    }
+
+    pub fn get_succeeded(&self) -> usize {
+        self.succeeded.load(Ordering::SeqCst)
+    }
+
+    pub fn get_failed(&self) -> usize {
+        self.failed.load(Ordering::SeqCst)
+    }
+
+    pub fn get_timed_out(&self) -> usize {
+        self.timed_out.load(Ordering::SeqCst)
+    }
+}
+
+/// Progress indicator for verification harness execution
+pub struct ProgressIndicator {
+    progress_bar: Option<ProgressBar>,
+    stats: VerificationStats,
+}
+
+impl ProgressIndicator {
+    /// Create a new progress indicator if running in an interactive terminal and log file is enabled
+    pub fn new(total_harnesses: usize, show_progress: bool) -> Self {
+        let stats = VerificationStats::new(total_harnesses);
+
+        if show_progress {
+            let progress_bar = ProgressBar::new(total_harnesses as u64);
+
+            progress_bar.set_style(
+                ProgressStyle::with_template(
+                    "{spinner:.green} [{elapsed_precise}] [{bar:40.cyan/blue}] {pos}/{len} ({eta})\n{msg}"
+                )
+                .unwrap()
+                .progress_chars("#>-"),
+            );
+
+            progress_bar.set_message("Verifying harnesses...");
+
+            Self { progress_bar: Some(progress_bar), stats }
+        } else {
+            Self { progress_bar: None, stats }
+        }
+    }
+
+    /// Update progress with the result of a harness verification
+    pub fn update_with_result(&self, succeeded: bool, timed_out: bool) {
+        self.stats.increment_completed();
+
+        if timed_out {
+            self.stats.increment_timed_out();
+        } else if succeeded {
+            self.stats.increment_succeeded();
+        } else {
+            self.stats.increment_failed();
+        }
+
+        if let Some(ref pb) = self.progress_bar {
+            pb.inc(1);
+            let completed = self.stats.get_completed();
+            let succeeded = self.stats.get_succeeded();
+            let failed = self.stats.get_failed();
+            let timed_out = self.stats.get_timed_out();
+
+            pb.set_message(format!(
+                "Completed: {}/{} | Succeeded: {} | Failed: {} | Timed out: {}",
+                completed, self.stats.total, succeeded, failed, timed_out
+            ));
+        }
+    }
+
+    /// Finish the progress indicator
+    pub fn finish(&self) {
+        if let Some(ref pb) = self.progress_bar {
+            let succeeded = self.stats.get_succeeded();
+            let failed = self.stats.get_failed();
+            let timed_out = self.stats.get_timed_out();
+
+            pb.finish_with_message(format!(
+                "Verification complete | Succeeded: {} | Failed: {} | Timed out: {}",
+                succeeded, failed, timed_out
+            ));
+        }
+    }
+
+    /// Check if progress indicator is active
+    pub fn is_active(&self) -> bool {
+        self.progress_bar.is_some()
+    }
+
+    /// Get the statistics
+    ///
+    /// This method provides access to the underlying verification statistics,
+    /// which may be useful for testing, monitoring, or external reporting purposes.
+    #[allow(dead_code)]
+    pub fn stats(&self) -> &VerificationStats {
+        &self.stats
+    }
+}
diff --git a/tests/ui/log-file-output/expected b/tests/ui/log-file-output/expected
new file mode 100644
index 00000000000..6a72096f329
--- /dev/null
+++ b/tests/ui/log-file-output/expected
@@ -0,0 +1,3 @@
+Kani Rust Verifier \
+Manual Harness Summary:\
+Complete - 2 successfully verified harnesses, 0 failures, 2 total.
diff --git a/tests/ui/log-file-output/main.rs b/tests/ui/log-file-output/main.rs
new file mode 100644
index 00000000000..8c17f6a471f
--- /dev/null
+++ b/tests/ui/log-file-output/main.rs
@@ -0,0 +1,21 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// kani-flags: --log-file verification.log
+//
+// This test checks that the --log-file option works correctly
+// and writes verification output to the specified file
+
+#[kani::proof]
+fn test_simple_verification() {
+    let x: u32 = kani::any();
+    if x < 100 {
+        assert!(x < 100);
+    }
+}
+
+#[kani::proof]
+fn test_another_harness() {
+    let y: i32 = kani::any();
+    assert!(y == y);
+}