diff --git a/docs/src/SUMMARY.md b/docs/src/SUMMARY.md
index d534cf1f7f22..11d5318a0e2c 100644
--- a/docs/src/SUMMARY.md
+++ b/docs/src/SUMMARY.md
@@ -18,6 +18,7 @@
 - [Reference](./reference.md)
   - [Attributes](./reference/attributes.md)
   - [Experimental features](./reference/experimental/experimental-features.md)
+    - [Automatic Harness Generation](./reference/experimental/autoharness.md)
     - [Coverage](./reference/experimental/coverage.md)
     - [Stubbing](./reference/experimental/stubbing.md)
     - [Contracts](./reference/experimental/contracts.md)
diff --git a/docs/src/reference/experimental/autoharness.md b/docs/src/reference/experimental/autoharness.md
new file mode 100644
index 000000000000..022d6471ea0e
--- /dev/null
+++ b/docs/src/reference/experimental/autoharness.md
@@ -0,0 +1,84 @@
+# Automatic Harness Generation
+
+Recall the harness for `estimate_size` that we wrote in [First Steps](../../tutorial-first-steps.md):
+```rust
+{{#include ../../tutorial/first-steps-v1/src/lib.rs:kani}}
+```
+
+This harness first declares a local variable `x` using `kani::any()`, then calls `estimate_size` with argument `x`.
+Many proof harnesses follow this predictable format—to verify a function `foo`, we create arbitrary values for each of `foo`'s arguments, then call `foo` on those arguments.
+
+The `autoharness` subcommand leverages this observation to automatically generate and run harnesses.
+Kani scans the crate for functions whose arguments all implement the `kani::Arbitrary` trait, generates harnesses for them, then runs them.
+These harnesses are internal to Kani--i.e., Kani does not make any changes to your source code.
+
+## Usage
+Run either:
+```
+# cargo kani autoharness -Z unstable-options
+```
+or
+```
+# kani autoharness -Z unstable-options <FILE>
+```
+
+If Kani detects that all of a function `foo`'s arguments implement `kani::Arbitrary`, it will generate and run a `#[kani::proof]` harness, which prints:
+
+```
+Autoharness: Checking function foo against all possible inputs...
+<VERIFICATION RESULTS>
+```
+
+However, if Kani detects that `foo` has a [contract](./contracts.md), it will instead generate a `#[kani::proof_for_contract]` harness and verify the contract:
+```
+Autoharness: Checking function foo's contract against all possible inputs...
+<VERIFICATION RESULTS>
+```
+
+Kani generates and runs these harnesses internally—the user only sees the verification results.
+
+The `autoharness` subcommand has options `--include-function` and `--exclude-function` to include and exclude particular functions.
+These flags look for partial matches against the fully qualified name of a function.
+
+For example, if a module `my_module` has many functions, but we are only interested in `my_module::foo` and `my_module::bar`, we can run:
+```
+cargo run autoharness -Z unstable-options --include-function foo include-function bar
+```
+To exclude `my_module` entirely, run:
+```
+cargo run autoharness -Z unstable-options --exclude-function my_module
+```
+
+## Example
+Using the `estimate_size` example from [First Steps](../../tutorial-first-steps.md) again:
+```rust
+{{#include ../../tutorial/first-steps-v1/src/lib.rs:code}}
+```
+
+We get:
+
+```
+# cargo kani autoharness -Z unstable-options
+Autoharness: Checking function estimate_size against all possible inputs...
+RESULTS:
+Check 3: estimate_size.assertion.1
+         - Status: FAILURE
+         - Description: "Oh no, a failing corner case!"
+[...]
+
+Verification failed for - estimate_size
+Complete - 0 successfully verified functions, 1 failures, 1 total.
+```
+
+## Request for comments
+This feature is experimental and is therefore subject to change.
+If you have ideas for improving the user experience of this feature,
+please add them to [this GitHub issue](https://github.com/model-checking/kani/issues/3832).
+
+## Limitations
+Kani will only generate an automatic harness for a function if it can determine that all of the function's arguments implement Arbitrary.
+It does not attempt to derive/implement Arbitrary for any types, even if those types could implement Arbitrary.
+
+If a function contains a loop with a loop contract, Kani will detect the presence of a loop contract and verify that contract.
+If, however, the loop does not have a contract, then there is currently no way to specify an unwinding bound for the function, meaning that Kani may hang as it tries to unwind the loop.
+We recommend using the `--exclude-function` option to exclude any functions that have this issue (or `--harness-timeout` to bail after attempting verification for some amount of time).
\ No newline at end of file
diff --git a/kani-compiler/src/args.rs b/kani-compiler/src/args.rs
index 99254a08423a..e524b6e5ba2a 100644
--- a/kani-compiler/src/args.rs
+++ b/kani-compiler/src/args.rs
@@ -30,6 +30,9 @@ pub enum ReachabilityType {
     PubFns,
     /// Start the cross-crate reachability analysis from all *test* (i.e. `#[test]`) harnesses in the local crate.
     Tests,
+    /// Start the cross-crate reachability analysis from all functions in the local crate.
+    /// Currently, this mode is only used for automatic harness generation.
+    AllFns,
 }
 
 /// Command line arguments that this instance of the compiler run was called
@@ -88,6 +91,12 @@ pub struct Arguments {
     /// Print the final LLBC file to stdout.
     #[clap(long)]
     pub print_llbc: bool,
+    /// If we are running the autoharness subcommand, the functions to autoharness
+    #[arg(long = "autoharness-include-function", num_args(1))]
+    pub autoharness_included_functions: Vec<String>,
+    /// If we are running the autoharness subcommand, the functions to exclude from autoverification
+    #[arg(long = "autoharness-exclude-function", num_args(1))]
+    pub autoharness_excluded_functions: Vec<String>,
 }
 
 #[derive(Debug, Clone, Copy, AsRefStr, EnumString, VariantNames, PartialEq, Eq)]
diff --git a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs
index e87bed0ea388..f577d2886e6c 100644
--- a/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs
+++ b/kani-compiler/src/codegen_aeneas_llbc/compiler_interface.rs
@@ -253,7 +253,7 @@ impl CodegenBackend for LlbcCodegenBackend {
                     units.store_modifies(&modifies_instances);
                     units.write_metadata(&queries, tcx);
                 }
-                ReachabilityType::Tests => todo!(),
+                ReachabilityType::Tests | ReachabilityType::AllFns => todo!(),
                 ReachabilityType::None => {}
                 ReachabilityType::PubFns => {
                     let unit = CodegenUnit::default();
diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
index a0ae5ae99eff..80137db06a6e 100644
--- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
+++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs
@@ -264,7 +264,7 @@ impl CodegenBackend for GotocCodegenBackend {
             let reachability = queries.args().reachability_analysis;
             let mut results = GotoCodegenResults::new(tcx, reachability);
             match reachability {
-                ReachabilityType::Harnesses => {
+                ReachabilityType::AllFns | ReachabilityType::Harnesses => {
                     let mut units = CodegenUnits::new(&queries, tcx);
                     let mut modifies_instances = vec![];
                     let mut loop_contracts_instances = vec![];
@@ -375,7 +375,9 @@ impl CodegenBackend for GotocCodegenBackend {
                 // Print compilation report.
                 results.print_report(tcx);
 
-                if reachability != ReachabilityType::Harnesses {
+                if reachability != ReachabilityType::Harnesses
+                    && reachability != ReachabilityType::AllFns
+                {
                     // In a workspace, cargo seems to be using the same file prefix to build a crate that is
                     // a package lib and also a dependency of another package.
                     // To avoid overriding the metadata for its verification, we skip this step when
diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs
index 072528f9a765..1fc659ea2f80 100644
--- a/kani-compiler/src/kani_middle/codegen_units.rs
+++ b/kani-compiler/src/kani_middle/codegen_units.rs
@@ -8,8 +8,11 @@
 //! according to their stub configuration.
 
 use crate::args::ReachabilityType;
-use crate::kani_middle::attributes::is_proof_harness;
-use crate::kani_middle::metadata::{gen_contracts_metadata, gen_proof_metadata};
+use crate::kani_middle::attributes::{KaniAttributes, is_proof_harness};
+use crate::kani_middle::kani_functions::{KaniIntrinsic, KaniModel};
+use crate::kani_middle::metadata::{
+    gen_automatic_proof_metadata, gen_contracts_metadata, gen_proof_metadata,
+};
 use crate::kani_middle::reachability::filter_crate_items;
 use crate::kani_middle::resolve::expect_resolve_fn;
 use crate::kani_middle::stubbing::{check_compatibility, harness_stub_map};
@@ -20,8 +23,8 @@ use rustc_middle::ty::TyCtxt;
 use rustc_session::config::OutputType;
 use rustc_smir::rustc_internal;
 use stable_mir::CrateDef;
-use stable_mir::mir::mono::Instance;
-use stable_mir::ty::{FnDef, IndexedVal, RigidTy, TyKind};
+use stable_mir::mir::{TerminatorKind, mono::Instance};
+use stable_mir::ty::{FnDef, GenericArgKind, GenericArgs, IndexedVal, RigidTy, TyKind};
 use std::collections::{BTreeMap, BTreeSet, HashMap, HashSet};
 use std::fs::File;
 use std::io::BufWriter;
@@ -57,26 +60,66 @@ pub struct CodegenUnit {
 impl CodegenUnits {
     pub fn new(queries: &QueryDb, tcx: TyCtxt) -> Self {
         let crate_info = CrateInfo { name: stable_mir::local_crate().name.as_str().into() };
-        if queries.args().reachability_analysis == ReachabilityType::Harnesses {
-            let base_filepath = tcx.output_filenames(()).path(OutputType::Object);
-            let base_filename = base_filepath.as_path();
-            let harnesses = filter_crate_items(tcx, |_, instance| is_proof_harness(tcx, instance));
-            let all_harnesses = harnesses
-                .into_iter()
-                .map(|harness| {
-                    let metadata = gen_proof_metadata(tcx, harness, &base_filename);
-                    (harness, metadata)
-                })
-                .collect::<HashMap<_, _>>();
+        let base_filepath = tcx.output_filenames(()).path(OutputType::Object);
+        let base_filename = base_filepath.as_path();
+        let args = queries.args();
+        match args.reachability_analysis {
+            ReachabilityType::Harnesses => {
+                let all_harnesses = get_all_manual_harnesses(tcx, base_filename);
+                // Even if no_stubs is empty we still need to store rustc metadata.
+                let units = group_by_stubs(tcx, &all_harnesses);
+                validate_units(tcx, &units);
+                debug!(?units, "CodegenUnits::new");
+                CodegenUnits { units, harness_info: all_harnesses, crate_info }
+            }
+            ReachabilityType::AllFns => {
+                let mut all_harnesses = get_all_manual_harnesses(tcx, base_filename);
+                let mut units = group_by_stubs(tcx, &all_harnesses);
+                validate_units(tcx, &units);
 
-            // Even if no_stubs is empty we still need to store rustc metadata.
-            let units = group_by_stubs(tcx, &all_harnesses);
-            validate_units(tcx, &units);
-            debug!(?units, "CodegenUnits::new");
-            CodegenUnits { units, harness_info: all_harnesses, crate_info }
-        } else {
-            // Leave other reachability type handling as is for now.
-            CodegenUnits { units: vec![], harness_info: HashMap::default(), crate_info }
+                let kani_fns = queries.kani_functions();
+                let kani_harness_intrinsic =
+                    kani_fns.get(&KaniIntrinsic::AutomaticHarness.into()).unwrap();
+                let kani_any_inst = kani_fns.get(&KaniModel::Any.into()).unwrap();
+
+                let verifiable_fns = filter_crate_items(tcx, |_, instance: Instance| -> bool {
+                    // If the user specified functions to include or exclude, only allow instances matching those filters.
+                    let user_included = if !args.autoharness_included_functions.is_empty() {
+                        fn_list_contains_instance(&instance, &args.autoharness_included_functions)
+                    } else if !args.autoharness_excluded_functions.is_empty() {
+                        !fn_list_contains_instance(&instance, &args.autoharness_excluded_functions)
+                    } else {
+                        true
+                    };
+                    user_included
+                        && is_eligible_for_automatic_harness(tcx, instance, *kani_any_inst)
+                });
+                let automatic_harnesses = get_all_automatic_harnesses(
+                    tcx,
+                    verifiable_fns,
+                    *kani_harness_intrinsic,
+                    base_filename,
+                );
+                // We generate one contract harness per function under contract, so each harness is in its own unit,
+                // and these harnesses have no stubs.
+                units.extend(
+                    automatic_harnesses
+                        .keys()
+                        .map(|harness| CodegenUnit {
+                            harnesses: vec![*harness],
+                            stubs: HashMap::default(),
+                        })
+                        .collect::<Vec<_>>(),
+                );
+                all_harnesses.extend(automatic_harnesses);
+                // No need to validate the units again because validation only checks stubs, and we haven't added any stubs.
+                debug!(?units, "CodegenUnits::new");
+                CodegenUnits { units, harness_info: all_harnesses, crate_info }
+            }
+            _ => {
+                // Leave other reachability type handling as is for now.
+                CodegenUnits { units: vec![], harness_info: HashMap::default(), crate_info }
+            }
         }
     }
 
@@ -94,7 +137,15 @@ impl CodegenUnits {
     /// We flag that the harness contains usage of loop contracts.
     pub fn store_loop_contracts(&mut self, harnesses: &[Harness]) {
         for harness in harnesses {
-            self.harness_info.get_mut(harness).unwrap().has_loop_contracts = true;
+            let metadata = self.harness_info.get_mut(harness).unwrap();
+            metadata.has_loop_contracts = true;
+            // If we're generating this harness automatically and we encounter a loop contract,
+            // ensure that the HarnessKind is updated to be a contract harness
+            // targeting the function to verify.
+            if metadata.is_automatically_generated {
+                metadata.attributes.kind =
+                    HarnessKind::ProofForContract { target_fn: metadata.pretty_name.clone() }
+            }
         }
     }
 
@@ -252,3 +303,89 @@ fn apply_transitivity(tcx: TyCtxt, harness: Harness, stubs: Stubs) -> Stubs {
     }
     new_stubs
 }
+
+/// Fetch all manual harnesses (i.e., functions provided by the user) and generate their metadata
+fn get_all_manual_harnesses(
+    tcx: TyCtxt,
+    base_filename: &Path,
+) -> HashMap<Harness, HarnessMetadata> {
+    let harnesses = filter_crate_items(tcx, |_, instance| is_proof_harness(tcx, instance));
+    harnesses
+        .into_iter()
+        .map(|harness| {
+            let metadata = gen_proof_metadata(tcx, harness, &base_filename);
+            (harness, metadata)
+        })
+        .collect::<HashMap<_, _>>()
+}
+
+/// For each function eligible for automatic verification,
+/// generate a harness Instance for it, then generate its metadata.
+/// Note that the body of each harness instance is still the dummy body of `kani_harness_intrinsic`;
+/// the AutomaticHarnessPass will later transform the bodies of these instances to actually verify the function.
+fn get_all_automatic_harnesses(
+    tcx: TyCtxt,
+    verifiable_fns: Vec<Instance>,
+    kani_harness_intrinsic: FnDef,
+    base_filename: &Path,
+) -> HashMap<Harness, HarnessMetadata> {
+    verifiable_fns
+        .into_iter()
+        .map(|fn_to_verify| {
+            // Set the generic arguments of the harness to be the function it is verifying
+            // so that later, in AutomaticHarnessPass, we can retrieve the function to verify
+            // and generate the harness body accordingly.
+            let harness = Instance::resolve(
+                kani_harness_intrinsic,
+                &GenericArgs(vec![GenericArgKind::Type(fn_to_verify.ty())]),
+            )
+            .unwrap();
+            let metadata = gen_automatic_proof_metadata(tcx, &base_filename, &fn_to_verify);
+            (harness, metadata)
+        })
+        .collect::<HashMap<_, _>>()
+}
+
+/// Determine whether `instance` is eligible for automatic verification.
+fn is_eligible_for_automatic_harness(tcx: TyCtxt, instance: Instance, any_inst: FnDef) -> bool {
+    // `instance` is ineligble if it is a harness or has an nonexistent/empty body
+    if is_proof_harness(tcx, instance) || !instance.has_body() {
+        return false;
+    }
+    let body = instance.body().unwrap();
+
+    // `instance` is ineligble if it is an associated item of a Kani trait implementation,
+    // or part of Kani contract instrumentation.
+    // FIXME -- find a less hardcoded way of checking the former condition (perhaps upstream PR to StableMIR).
+    if instance.name().contains("kani::Arbitrary")
+        || instance.name().contains("kani::Invariant")
+        || KaniAttributes::for_instance(tcx, instance)
+            .fn_marker()
+            .is_some_and(|m| m.as_str() == "kani_contract_mode")
+    {
+        return false;
+    }
+
+    // Each non-generic argument of `instance`` must implement Arbitrary.
+    body.arg_locals().iter().all(|arg| {
+        let kani_any_body =
+            Instance::resolve(any_inst, &GenericArgs(vec![GenericArgKind::Type(arg.ty)]))
+                .unwrap()
+                .body()
+                .unwrap();
+        if let TerminatorKind::Call { func, .. } = &kani_any_body.blocks[0].terminator.kind {
+            if let Some((def, args)) = func.ty(body.arg_locals()).unwrap().kind().fn_def() {
+                return Instance::resolve(def, &args).is_ok();
+            }
+        }
+        false
+    })
+}
+
+/// Return whether the name of `instance` is included in `fn_list`.
+/// If `exact = true`, then `instance`'s exact, fully-qualified name must be in `fn_list`; otherwise, `fn_list`
+/// can have a substring of `instance`'s name.
+fn fn_list_contains_instance(instance: &Instance, fn_list: &[String]) -> bool {
+    let pretty_name = instance.name();
+    fn_list.contains(&pretty_name) || fn_list.iter().any(|fn_name| pretty_name.contains(fn_name))
+}
diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs
index 8d1ab5ef939d..3182ced8fa61 100644
--- a/kani-compiler/src/kani_middle/kani_functions.rs
+++ b/kani-compiler/src/kani_middle/kani_functions.rs
@@ -48,6 +48,8 @@ pub enum KaniIntrinsic {
     CheckedAlignOf,
     #[strum(serialize = "CheckedSizeOfIntrinsic")]
     CheckedSizeOf,
+    #[strum(serialize = "AutomaticHarnessIntrinsic")]
+    AutomaticHarness,
     #[strum(serialize = "IsInitializedIntrinsic")]
     IsInitialized,
     #[strum(serialize = "ValidValueIntrinsic")]
diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs
index 67d32b0079c4..449548f27045 100644
--- a/kani-compiler/src/kani_middle/metadata.rs
+++ b/kani-compiler/src/kani_middle/metadata.rs
@@ -39,6 +39,7 @@ pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) ->
         goto_file: Some(model_file),
         contract: Default::default(),
         has_loop_contracts: false,
+        is_automatically_generated: false,
     }
 }
 
@@ -84,6 +85,48 @@ pub fn gen_contracts_metadata(tcx: TyCtxt) -> Vec<ContractedFunction> {
     fn_to_data.into_values().collect()
 }
 
+/// Generate metadata for automatically generated harnesses.
+/// For now, we just use the data from the function we are verifying; since we only generate one automatic harness per function,
+/// the metdata from that function uniquely identifies the harness.
+/// In future iterations of this feature, we will likely have multiple harnesses for a single function (e.g., for generic functions),
+/// in which case HarnessMetadata will need to change further to differentiate between those harnesses.
+pub fn gen_automatic_proof_metadata(
+    tcx: TyCtxt,
+    base_name: &Path,
+    fn_to_verify: &Instance,
+) -> HarnessMetadata {
+    let def = fn_to_verify.def;
+    let pretty_name = fn_to_verify.name();
+    let mangled_name = fn_to_verify.mangled_name();
+
+    // Leave the concrete playback instrumentation for now, but this feature does not actually support concrete playback.
+    let loc = SourceLocation::new(fn_to_verify.body().unwrap().span);
+    let file_stem = format!("{}_{mangled_name}", base_name.file_stem().unwrap().to_str().unwrap());
+    let model_file = base_name.with_file_name(file_stem).with_extension(ArtifactType::SymTabGoto);
+
+    let kani_attributes = KaniAttributes::for_instance(tcx, *fn_to_verify);
+    let harness_kind = if kani_attributes.has_contract() {
+        HarnessKind::ProofForContract { target_fn: pretty_name.clone() }
+    } else {
+        HarnessKind::Proof
+    };
+
+    HarnessMetadata {
+        pretty_name,
+        mangled_name,
+        crate_name: def.krate().name,
+        original_file: loc.filename,
+        original_start_line: loc.start_line,
+        original_end_line: loc.end_line,
+        attributes: HarnessAttributes::new(harness_kind),
+        // TODO: This no longer needs to be an Option.
+        goto_file: Some(model_file),
+        contract: Default::default(),
+        has_loop_contracts: false,
+        is_automatically_generated: true,
+    }
+}
+
 /// Create the harness metadata for a test description.
 #[allow(dead_code)]
 pub fn gen_test_metadata(
@@ -110,5 +153,6 @@ pub fn gen_test_metadata(
         goto_file: Some(model_file),
         contract: Default::default(),
         has_loop_contracts: false,
+        is_automatically_generated: false,
     }
 }
diff --git a/kani-compiler/src/kani_middle/transform/automatic.rs b/kani-compiler/src/kani_middle/transform/automatic.rs
new file mode 100644
index 000000000000..705a8ac26a88
--- /dev/null
+++ b/kani-compiler/src/kani_middle/transform/automatic.rs
@@ -0,0 +1,129 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+//! This module transforms the body of an automatic harness to verify a function.
+//! Upon entry to this module, a harness has the dummy body of the automatic_harness Kani intrinsic.
+//! We obtain the function its meant to verify by inspecting its generic arguments,
+//! then transform its body to be a harness for that function.
+
+use crate::args::ReachabilityType;
+use crate::kani_middle::codegen_units::CodegenUnit;
+use crate::kani_middle::kani_functions::{KaniIntrinsic, KaniModel};
+use crate::kani_middle::transform::body::{InsertPosition, MutableBody, SourceInstruction};
+use crate::kani_middle::transform::{TransformPass, TransformationType};
+use crate::kani_queries::QueryDb;
+use rustc_middle::ty::TyCtxt;
+use stable_mir::mir::mono::Instance;
+use stable_mir::mir::{Body, Operand, Place, TerminatorKind};
+use stable_mir::ty::{FnDef, GenericArgKind, GenericArgs};
+use tracing::debug;
+
+#[derive(Debug)]
+pub struct AutomaticHarnessPass {
+    /// The FnDef of KaniModel::Any
+    kani_any: FnDef,
+    /// All of the automatic harness Instances that we generated in the CodegenUnits constructor
+    automatic_harnesses: Vec<Instance>,
+}
+
+impl AutomaticHarnessPass {
+    // FIXME: this is a bit clunky.
+    // Historically, in codegen_crate, we reset the BodyTransformation cache on a per-unit basis,
+    // so the BodyTransformation constructor only accepts a CodegenUnit and thus this constructor can only accept a unit.
+    // Later, we changed codegen to reset the cache on a per-harness basis (for uninitialized memory instrumentation).
+    // So BodyTransformation should really be changed to reflect that, so that this constructor can just save the one automatic harness it should transform
+    // and not all of the possibilities.
+    pub fn new(unit: &CodegenUnit, query_db: &QueryDb) -> Self {
+        let kani_fns = query_db.kani_functions();
+        let harness_intrinsic = *kani_fns.get(&KaniIntrinsic::AutomaticHarness.into()).unwrap();
+        let kani_any = *kani_fns.get(&KaniModel::Any.into()).unwrap();
+        let automatic_harnesses = unit
+            .harnesses
+            .iter()
+            .cloned()
+            .filter(|harness| {
+                let (def, _) = harness.ty().kind().fn_def().unwrap();
+                def == harness_intrinsic
+            })
+            .collect::<Vec<_>>();
+        Self { kani_any, automatic_harnesses }
+    }
+}
+
+impl TransformPass for AutomaticHarnessPass {
+    fn transformation_type() -> TransformationType
+    where
+        Self: Sized,
+    {
+        TransformationType::Stubbing
+    }
+
+    fn is_enabled(&self, query_db: &QueryDb) -> bool
+    where
+        Self: Sized,
+    {
+        matches!(query_db.args().reachability_analysis, ReachabilityType::AllFns)
+    }
+
+    fn transform(&mut self, _tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) {
+        debug!(function=?instance.name(), "AutomaticHarnessPass::transform");
+
+        if !self.automatic_harnesses.contains(&instance) {
+            return (false, body);
+        }
+
+        // Retrieve the generic arguments of the harness, which is the type of the function it is verifying,
+        // and then resolve `fn_to_verify`.
+        let kind = instance.args().0[0].expect_ty().kind();
+        let (def, args) = kind.fn_def().unwrap();
+        let fn_to_verify = Instance::resolve(def, &args).unwrap();
+        let fn_to_verify_body = fn_to_verify.body().unwrap();
+
+        let mut harness_body = MutableBody::from(body);
+        harness_body.clear_body(TerminatorKind::Return);
+        let mut source = SourceInstruction::Terminator { bb: 0 };
+
+        let mut arg_locals = vec![];
+
+        // For each argument of `fn_to_verify`, create a nondeterministic value of its type
+        // by generating a kani::any() call and saving the result in `arg_local`.
+        for local_decl in fn_to_verify_body.arg_locals().iter() {
+            let arg_local = harness_body.new_local(
+                local_decl.ty,
+                source.span(harness_body.blocks()),
+                local_decl.mutability,
+            );
+            let kani_any_inst = Instance::resolve(
+                self.kani_any,
+                &GenericArgs(vec![GenericArgKind::Type(local_decl.ty)]),
+            )
+            .unwrap();
+            harness_body.insert_call(
+                &kani_any_inst,
+                &mut source,
+                InsertPosition::Before,
+                vec![],
+                Place::from(arg_local),
+            );
+            arg_locals.push(arg_local);
+        }
+
+        let func_to_verify_ret = fn_to_verify_body.ret_local();
+        let ret_place = Place::from(harness_body.new_local(
+            func_to_verify_ret.ty,
+            source.span(harness_body.blocks()),
+            func_to_verify_ret.mutability,
+        ));
+
+        // Call `fn_to_verify` on the nondeterministic arguments generated above.
+        harness_body.insert_call(
+            &fn_to_verify,
+            &mut source,
+            InsertPosition::Before,
+            arg_locals.iter().map(|lcl| Operand::Copy(Place::from(*lcl))).collect::<Vec<_>>(),
+            ret_place,
+        );
+
+        (true, harness_body.into())
+    }
+}
diff --git a/kani-compiler/src/kani_middle/transform/contracts.rs b/kani-compiler/src/kani_middle/transform/contracts.rs
index fea8a8a1bc3c..bd613b3d6663 100644
--- a/kani-compiler/src/kani_middle/transform/contracts.rs
+++ b/kani-compiler/src/kani_middle/transform/contracts.rs
@@ -1,6 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //! This module contains code related to the MIR-to-MIR pass to enable contracts.
+use crate::args::ReachabilityType;
 use crate::kani_middle::attributes::KaniAttributes;
 use crate::kani_middle::codegen_units::CodegenUnit;
 use crate::kani_middle::kani_functions::{KaniIntrinsic, KaniModel};
@@ -341,13 +342,34 @@ impl FunctionWithContractPass {
     /// verifying.
     pub fn new(tcx: TyCtxt, queries: &QueryDb, unit: &CodegenUnit) -> FunctionWithContractPass {
         if let Some(harness) = unit.harnesses.first() {
-            let attrs = KaniAttributes::for_instance(tcx, *harness);
-            let check_fn = attrs.interpret_for_contract_attribute().map(|(_, def_id, _)| def_id);
-            let replace_fns: HashSet<_> = attrs
-                .interpret_stub_verified_attribute()
-                .iter()
-                .map(|(_, def_id, _)| *def_id)
-                .collect();
+            let (check_fn, replace_fns) = {
+                let harness_generic_args = harness.args().0;
+                // Manual harnesses have no arguments, so if there are generic arguments,
+                // we know this is an automatic harness
+                if matches!(queries.args().reachability_analysis, ReachabilityType::AllFns)
+                    && !harness_generic_args.is_empty()
+                {
+                    let kind = harness.args().0[0].expect_ty().kind();
+                    let (def, args) = kind.fn_def().unwrap();
+                    let fn_to_verify = Instance::resolve(def, &args).unwrap();
+                    // For automatic harnesses, the target is the function to verify,
+                    // and stubs are empty.
+                    (
+                        Some(rustc_internal::internal(tcx, fn_to_verify.def.def_id())),
+                        HashSet::default(),
+                    )
+                } else {
+                    let attrs = KaniAttributes::for_instance(tcx, *harness);
+                    let check_fn =
+                        attrs.interpret_for_contract_attribute().map(|(_, def_id, _)| def_id);
+                    let replace_fns: HashSet<_> = attrs
+                        .interpret_stub_verified_attribute()
+                        .iter()
+                        .map(|(_, def_id, _)| *def_id)
+                        .collect();
+                    (check_fn, replace_fns)
+                }
+            };
             let run_contract_fn =
                 queries.kani_functions().get(&KaniModel::RunContract.into()).copied();
             assert!(run_contract_fn.is_some(), "Failed to find Kani run contract function");
diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs
index 206c0160a80d..d18b4b059063 100644
--- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs
+++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs
@@ -74,8 +74,10 @@ impl TransformPass for IntrinsicGeneratorPass {
                 KaniIntrinsic::CheckedSizeOf => (true, self.checked_size_of(body, instance)),
                 KaniIntrinsic::IsInitialized => (true, self.is_initialized_body(body)),
                 KaniIntrinsic::ValidValue => (true, self.valid_value_body(body)),
-                // This is handled in contracts pass for now.
-                KaniIntrinsic::WriteAny | KaniIntrinsic::AnyModifies => (false, body),
+                // The former two are handled in contracts pass for now, while the latter is handled in the the automatic harness pass.
+                KaniIntrinsic::WriteAny
+                | KaniIntrinsic::AnyModifies
+                | KaniIntrinsic::AutomaticHarness => (false, body),
             }
         } else {
             (false, body)
diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs
index 8001b1f1d359..49e36461081c 100644
--- a/kani-compiler/src/kani_middle/transform/mod.rs
+++ b/kani-compiler/src/kani_middle/transform/mod.rs
@@ -26,6 +26,7 @@ use crate::kani_middle::transform::kani_intrinsics::IntrinsicGeneratorPass;
 use crate::kani_middle::transform::loop_contracts::LoopContractPass;
 use crate::kani_middle::transform::stubs::{ExternFnStubPass, FnStubPass};
 use crate::kani_queries::QueryDb;
+use automatic::AutomaticHarnessPass;
 use dump_mir_pass::DumpMirPass;
 use rustc_middle::ty::TyCtxt;
 use stable_mir::mir::Body;
@@ -36,6 +37,7 @@ use std::fmt::Debug;
 use crate::kani_middle::transform::rustc_intrinsics::RustcIntrinsicsPass;
 pub use internal_mir::RustcInternalMir;
 
+mod automatic;
 pub(crate) mod body;
 mod check_uninit;
 mod check_values;
@@ -71,6 +73,8 @@ impl BodyTransformation {
             cache: Default::default(),
         };
         let check_type = CheckType::new_assert_assume(queries);
+        // This has to come first, since creating harnesses affects later stubbing and contract passes.
+        transformer.add_pass(queries, AutomaticHarnessPass::new(unit, queries));
         transformer.add_pass(queries, FnStubPass::new(&unit.stubs));
         transformer.add_pass(queries, ExternFnStubPass::new(&unit.stubs));
         transformer.add_pass(queries, FunctionWithContractPass::new(tcx, queries, &unit));
diff --git a/kani-driver/src/args/autoharness_args.rs b/kani-driver/src/args/autoharness_args.rs
new file mode 100644
index 000000000000..d7a69070bf41
--- /dev/null
+++ b/kani-driver/src/args/autoharness_args.rs
@@ -0,0 +1,136 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Implements the subcommand handling of the autoharness subcommand
+
+use std::path::PathBuf;
+
+use crate::args::{ValidateArgs, VerificationArgs};
+use clap::{Error, Parser, error::ErrorKind};
+use kani_metadata::UnstableFeature;
+
+#[derive(Debug, Parser)]
+pub struct CommonAutoharnessArgs {
+    /// If specified, only autoharness functions that match this filter. This option can be provided
+    /// multiple times, which will verify all functions matching any of the filters.
+    /// Note that this filter will match against partial names, i.e., providing the name of a module will include all functions from that module.
+    /// Also note that if the function specified is unable to be automatically verified, this flag will have no effect.
+    #[arg(
+        long = "include-function",
+        num_args(1),
+        value_name = "FUNCTION",
+        conflicts_with = "exclude_function"
+    )]
+    pub include_function: Vec<String>,
+
+    /// If specified, only autoharness functions that do not match this filter. This option can be provided
+    /// multiple times, which will verify all functions that do not match any of the filters.
+    /// Note that this filter will match against partial names, i.e., providing the name of a module will exclude all functions from that module.
+    #[arg(long = "exclude-function", num_args(1), value_name = "FUNCTION")]
+    pub exclude_function: Vec<String>,
+    // TODO: It would be nice if we could borrow --exact here from VerificationArgs to differentiate between partial/exact matches,
+    // like --harnesses does. Sharing arguments with VerificationArgs doesn't work with our current structure, though.
+}
+
+/// Automatically verify functions in a crate.
+#[derive(Debug, Parser)]
+pub struct CargoAutoharnessArgs {
+    #[command(flatten)]
+    pub common_autoharness_args: CommonAutoharnessArgs,
+
+    #[command(flatten)]
+    pub verify_opts: VerificationArgs,
+}
+
+/// Automatically verify functions in a file.
+#[derive(Debug, Parser)]
+pub struct StandaloneAutoharnessArgs {
+    /// Rust crate's top file location.
+    #[arg(required = true)]
+    pub input: PathBuf,
+
+    #[arg(long, hide = true)]
+    pub crate_name: Option<String>,
+
+    #[command(flatten)]
+    pub common_autoharness_args: CommonAutoharnessArgs,
+
+    #[command(flatten)]
+    pub verify_opts: VerificationArgs,
+}
+
+impl ValidateArgs for CargoAutoharnessArgs {
+    fn validate(&self) -> Result<(), Error> {
+        self.verify_opts.validate()?;
+        if !self
+            .verify_opts
+            .common_args
+            .unstable_features
+            .contains(UnstableFeature::UnstableOptions)
+        {
+            return Err(Error::raw(
+                ErrorKind::MissingRequiredArgument,
+                format!(
+                    "The `autoharness` subcommand is unstable and requires -Z {}",
+                    UnstableFeature::UnstableOptions
+                ),
+            ));
+        }
+
+        if self
+            .verify_opts
+            .common_args
+            .unstable_features
+            .contains(UnstableFeature::ConcretePlayback)
+        {
+            return Err(Error::raw(
+                ErrorKind::ArgumentConflict,
+                "The autoharness subcommand does not support concrete playback",
+            ));
+        }
+
+        Ok(())
+    }
+}
+
+impl ValidateArgs for StandaloneAutoharnessArgs {
+    fn validate(&self) -> Result<(), Error> {
+        self.verify_opts.validate()?;
+        if !self
+            .verify_opts
+            .common_args
+            .unstable_features
+            .contains(UnstableFeature::UnstableOptions)
+        {
+            return Err(Error::raw(
+                ErrorKind::MissingRequiredArgument,
+                format!(
+                    "The `autoharness` subcommand is unstable and requires -Z {}",
+                    UnstableFeature::UnstableOptions
+                ),
+            ));
+        }
+        if !self.input.is_file() {
+            return Err(Error::raw(
+                ErrorKind::InvalidValue,
+                format!(
+                    "Invalid argument: Input invalid. `{}` is not a regular file.",
+                    self.input.display()
+                ),
+            ));
+        }
+
+        if self
+            .verify_opts
+            .common_args
+            .unstable_features
+            .contains(UnstableFeature::ConcretePlayback)
+        {
+            return Err(Error::raw(
+                ErrorKind::ArgumentConflict,
+                "The autoharness subcommand does not support concrete playback",
+            ));
+        }
+
+        Ok(())
+    }
+}
diff --git a/kani-driver/src/args/mod.rs b/kani-driver/src/args/mod.rs
index b8b1ba60a50a..26e9927cf67c 100644
--- a/kani-driver/src/args/mod.rs
+++ b/kani-driver/src/args/mod.rs
@@ -3,6 +3,7 @@
 //! Module that define Kani's command line interface. This includes all subcommands.
 
 pub mod assess_args;
+pub mod autoharness_args;
 pub mod cargo;
 pub mod common;
 pub mod list_args;
@@ -145,6 +146,8 @@ pub enum StandaloneSubcommand {
     VerifyStd(Box<std_args::VerifyStdArgs>),
     /// List contracts and harnesses.
     List(Box<list_args::StandaloneListArgs>),
+    /// Scan the input file for functions eligible for automatic (i.e., harness-free) verification and verify them.
+    Autoharness(Box<autoharness_args::StandaloneAutoharnessArgs>),
 }
 
 #[derive(Debug, clap::Parser)]
@@ -173,6 +176,9 @@ pub enum CargoKaniSubcommand {
 
     /// List contracts and harnesses.
     List(Box<list_args::CargoListArgs>),
+
+    /// Scan the crate for functions eligible for automatic (i.e., harness-free) verification and verify them.
+    Autoharness(Box<autoharness_args::CargoAutoharnessArgs>),
 }
 
 // Common arguments for invoking Kani for verification purpose. This gets put into KaniContext,
@@ -487,6 +493,7 @@ impl ValidateArgs for StandaloneArgs {
         match &self.command {
             Some(StandaloneSubcommand::VerifyStd(args)) => args.validate()?,
             Some(StandaloneSubcommand::List(args)) => args.validate()?,
+            Some(StandaloneSubcommand::Autoharness(args)) => args.validate()?,
             // TODO: Invoke PlaybackArgs::validate()
             None | Some(StandaloneSubcommand::Playback(..)) => {}
         };
@@ -532,6 +539,7 @@ impl ValidateArgs for CargoKaniSubcommand {
         match self {
             // Assess doesn't implement validation yet.
             CargoKaniSubcommand::Assess(_) => Ok(()),
+            CargoKaniSubcommand::Autoharness(autoharness) => autoharness.validate(),
             CargoKaniSubcommand::Playback(playback) => playback.validate(),
             CargoKaniSubcommand::List(list) => list.validate(),
         }
diff --git a/kani-driver/src/assess/mod.rs b/kani-driver/src/assess/mod.rs
index ec91918ac8b5..02b3da0974f8 100644
--- a/kani-driver/src/assess/mod.rs
+++ b/kani-driver/src/assess/mod.rs
@@ -53,7 +53,7 @@ fn assess_project(mut session: KaniSession) -> Result<AssessMetadata> {
         session.args.jobs = Some(None); // -j, num_cpu
     }
 
-    let project = project::cargo_project(&session, true)?;
+    let project = project::cargo_project(&mut session, true)?;
     let cargo_metadata = project.cargo_metadata.as_ref().expect("built with cargo");
 
     let packages_metadata =
diff --git a/kani-driver/src/autoharness/mod.rs b/kani-driver/src/autoharness/mod.rs
new file mode 100644
index 000000000000..69c49580cd77
--- /dev/null
+++ b/kani-driver/src/autoharness/mod.rs
@@ -0,0 +1,73 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+use crate::call_cbmc::VerificationStatus;
+use crate::call_single_file::to_rustc_arg;
+use crate::harness_runner::HarnessResult;
+use crate::session::KaniSession;
+use anyhow::Result;
+
+impl KaniSession {
+    /// Enable autoharness mode.
+    pub fn enable_autoharness(&mut self) {
+        self.auto_harness = true;
+    }
+
+    /// Add the compiler arguments specific to the `autoharness` subcommand.
+    pub fn add_auto_harness_args(&mut self, included: Vec<String>, excluded: Vec<String>) {
+        for func in included {
+            self.pkg_args
+                .push(to_rustc_arg(vec![format!("--autoharness-include-function {}", func)]));
+        }
+        for func in excluded {
+            self.pkg_args
+                .push(to_rustc_arg(vec![format!("--autoharness-exclude-function {}", func)]));
+        }
+    }
+
+    /// Prints the results from running the `autoharness` subcommand.
+    pub fn print_autoharness_summary(&self, automatic: Vec<&HarnessResult<'_>>) -> Result<()> {
+        let (successes, failures): (Vec<_>, Vec<_>) =
+            automatic.into_iter().partition(|r| r.result.status == VerificationStatus::Success);
+
+        let succeeding = successes.len();
+        let failing = failures.len();
+        let total = succeeding + failing;
+
+        // TODO: it would be nice if we had access to which functions the user included/excluded here
+        // so that we could print a comparison for them of any of the included functions that we skipped.
+        println!("Autoharness Summary:");
+        println!(
+            "Note that Kani will only generate an automatic harness for a function if it determines that each of its arguments implement the Arbitrary trait."
+        );
+        println!(
+            "Examine the summary closely to determine which functions were automatically verified."
+        );
+
+        // Since autoverification skips over some functions, print the successes to make it easier to see what we verified in one place.
+        for success in successes {
+            println!("Verification succeeded for - {}", success.harness.pretty_name);
+        }
+
+        for failure in failures {
+            println!("Verification failed for - {}", failure.harness.pretty_name);
+        }
+
+        if total > 0 {
+            println!(
+                "Complete - {succeeding} successfully verified functions, {failing} failures, {total} total."
+            );
+        } else {
+            println!(
+                "No functions were eligible for automatic verification. Functions can only be automatically verified if each of their arguments implement kani::Arbitrary."
+            );
+            println!(
+                "If you specified --include-function or --exclude-function, make sure that your filters were not overly restrictive."
+            );
+        }
+
+        // Manual harness summary may come afterward, so separate them with a new line.
+        println!();
+        Ok(())
+    }
+}
diff --git a/kani-driver/src/call_cargo.rs b/kani-driver/src/call_cargo.rs
index 0bc716115989..4c39b03183b6 100644
--- a/kani-driver/src/call_cargo.rs
+++ b/kani-driver/src/call_cargo.rs
@@ -126,7 +126,7 @@ crate-type = ["lib"]
     }
 
     /// Calls `cargo_build` to generate `*.symtab.json` files in `target_dir`
-    pub fn cargo_build(&self, keep_going: bool) -> Result<CargoOutputs> {
+    pub fn cargo_build(&mut self, keep_going: bool) -> Result<CargoOutputs> {
         let build_target = env!("TARGET"); // see build.rs
         let metadata = self.cargo_metadata(build_target)?;
         let target_dir = self
@@ -183,13 +183,12 @@ crate-type = ["lib"]
         }
 
         // Arguments that will only be passed to the target package.
-        let mut pkg_args: Vec<String> = vec![];
-        pkg_args.extend(["--".to_string(), self.reachability_arg()]);
+        self.pkg_args.push(self.reachability_arg());
         if let Some(backend_arg) = self.backend_arg() {
-            pkg_args.push(backend_arg);
+            self.pkg_args.push(backend_arg);
         }
         if self.args.no_assert_contracts {
-            pkg_args.push("--no-assert-contracts".into());
+            self.pkg_args.push("--no-assert-contracts".into());
         }
 
         let mut found_target = false;
@@ -202,7 +201,7 @@ crate-type = ["lib"]
                 cmd.args(&cargo_args)
                     .args(vec!["-p", &package.id.to_string()])
                     .args(verification_target.to_args())
-                    .args(&pkg_args)
+                    .args(&self.pkg_args)
                     .env("RUSTC", &self.kani_compiler)
                     // Use CARGO_ENCODED_RUSTFLAGS instead of RUSTFLAGS is preferred. See
                     // https://doc.rust-lang.org/cargo/reference/environment-variables.html
diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs
index 96b2e732f5ba..56e3f4c09ed2 100644
--- a/kani-driver/src/harness_runner.rs
+++ b/kani-driver/src/harness_runner.rs
@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 use anyhow::{Error, Result, bail};
-use kani_metadata::{ArtifactType, HarnessMetadata};
+use kani_metadata::{ArtifactType, HarnessKind, HarnessMetadata};
 use rayon::prelude::*;
 use std::fs::File;
 use std::io::Write;
@@ -11,7 +11,7 @@ use std::path::Path;
 use crate::args::OutputFormat;
 use crate::call_cbmc::{VerificationResult, VerificationStatus};
 use crate::project::Project;
-use crate::session::KaniSession;
+use crate::session::{BUG_REPORT_URL, KaniSession};
 
 use std::env::current_dir;
 use std::path::PathBuf;
@@ -202,11 +202,28 @@ impl KaniSession {
     ) -> Result<VerificationResult> {
         let thread_index = rayon::current_thread_index().unwrap_or_default();
         if !self.args.common_args.quiet {
-            if rayon::current_num_threads() > 1 {
-                println!("Thread {thread_index}: Checking harness {}...", harness.pretty_name);
+            // If the harness is automatically generated, pretty_name refers to the function under verification.
+            let mut msg = if harness.is_automatically_generated {
+                if matches!(harness.attributes.kind, HarnessKind::Proof) {
+                    format!(
+                        "Autoharness: Checking function {} against all possible inputs...",
+                        harness.pretty_name
+                    )
+                } else {
+                    format!(
+                        "Autoharness: Checking function {}'s contract against all possible inputs...",
+                        harness.pretty_name
+                    )
+                }
             } else {
-                println!("Checking harness {}...", harness.pretty_name);
+                format!("Checking harness {}...", harness.pretty_name)
+            };
+
+            if rayon::current_num_threads() > 1 {
+                msg = format!("Thread {thread_index}: {msg}");
             }
+
+            println!("{msg}");
         }
 
         let mut result = self.with_timer(|| self.run_cbmc(binary, harness), "run_cbmc")?;
@@ -222,54 +239,65 @@ impl KaniSession {
     /// Note: Takes `self` "by ownership". This function wants to be able to drop before
     /// exiting with an error code, if needed.
     pub(crate) fn print_final_summary(self, results: &[HarnessResult<'_>]) -> Result<()> {
+        if self.args.common_args.quiet {
+            return Ok(());
+        }
+
+        let (automatic, manual): (Vec<_>, Vec<_>) =
+            results.iter().partition(|r| r.harness.is_automatically_generated);
+
+        if self.auto_harness {
+            self.print_autoharness_summary(automatic)?;
+        }
+
         let (successes, failures): (Vec<_>, Vec<_>) =
-            results.iter().partition(|r| r.result.status == VerificationStatus::Success);
+            manual.into_iter().partition(|r| r.result.status == VerificationStatus::Success);
 
         let succeeding = successes.len();
         let failing = failures.len();
         let total = succeeding + failing;
 
-        if self.args.concrete_playback.is_some()
-            && !self.args.common_args.quiet
-            && results.iter().all(|r| !r.result.generated_concrete_test)
-        {
-            println!(
-                "INFO: The concrete playback feature never generated unit tests because there were no failing harnesses."
-            )
+        if self.args.concrete_playback.is_some() {
+            if failures.is_empty() {
+                println!(
+                    "INFO: The concrete playback feature never generated unit tests because there were no failing harnesses."
+                )
+            } else if failures.iter().all(|r| !r.result.generated_concrete_test) {
+                eprintln!(
+                    "The concrete playback feature did not generate unit tests, but there were failing harnesses. Please file a bug report at {BUG_REPORT_URL}"
+                )
+            }
         }
 
         // We currently omit a summary if there was just 1 harness
-        if !self.args.common_args.quiet {
-            if failing > 0 {
-                println!("Summary:");
-            }
-            for failure in failures.iter() {
-                println!("Verification failed for - {}", failure.harness.pretty_name);
-            }
+        if failing > 0 {
+            println!("Manual Harness Summary:");
+        }
+        for failure in failures.iter() {
+            println!("Verification failed for - {}", failure.harness.pretty_name);
+        }
 
-            if total > 0 {
-                println!(
-                    "Complete - {succeeding} successfully verified harnesses, {failing} failures, {total} total."
-                );
-            } else {
-                match self.args.harnesses.as_slice() {
-                    [] =>
-                    // TODO: This could use a better message, possibly with links to Kani documentation.
-                    // New users may encounter this and could use a pointer to how to write proof harnesses.
-                    {
-                        println!(
-                            "No proof harnesses (functions with #[kani::proof]) were found to verify."
-                        )
-                    }
-                    [harness] => {
-                        bail!("no harnesses matched the harness filter: `{harness}`")
-                    }
-                    harnesses => bail!(
-                        "no harnesses matched the harness filters: `{}`",
-                        harnesses.join("`, `")
-                    ),
-                };
-            }
+        if total > 0 {
+            println!(
+                "Complete - {succeeding} successfully verified harnesses, {failing} failures, {total} total."
+            );
+        } else {
+            match self.args.harnesses.as_slice() {
+                [] =>
+                // TODO: This could use a better message, possibly with links to Kani documentation.
+                // New users may encounter this and could use a pointer to how to write proof harnesses.
+                {
+                    println!(
+                        "No proof harnesses (functions with #[kani::proof]) were found to verify."
+                    )
+                }
+                [harness] => {
+                    bail!("no harnesses matched the harness filter: `{harness}`")
+                }
+                harnesses => {
+                    bail!("no harnesses matched the harness filters: `{}`", harnesses.join("`, `"))
+                }
+            };
         }
 
         if self.args.coverage {
diff --git a/kani-driver/src/list/collect_metadata.rs b/kani-driver/src/list/collect_metadata.rs
index a7901e997ab1..588cab0b63af 100644
--- a/kani-driver/src/list/collect_metadata.rs
+++ b/kani-driver/src/list/collect_metadata.rs
@@ -78,12 +78,12 @@ fn process_metadata(metadata: Vec<KaniMetadata>) -> ListMetadata {
 pub fn list_cargo(args: CargoListArgs, mut verify_opts: VerificationArgs) -> Result<()> {
     let quiet = args.common_args.quiet;
     verify_opts.common_args = args.common_args;
-    let session = KaniSession::new(verify_opts)?;
+    let mut session = KaniSession::new(verify_opts)?;
     if !quiet {
         print_kani_version(InvocationType::CargoKani(vec![]));
     }
 
-    let project = cargo_project(&session, false)?;
+    let project = cargo_project(&mut session, false)?;
     let list_metadata = process_metadata(project.metadata);
 
     output_list_results(list_metadata, args.format, quiet)
diff --git a/kani-driver/src/main.rs b/kani-driver/src/main.rs
index 07405a30a307..9b82c8467e26 100644
--- a/kani-driver/src/main.rs
+++ b/kani-driver/src/main.rs
@@ -22,6 +22,7 @@ use tracing::debug;
 mod args;
 mod args_toml;
 mod assess;
+mod autoharness;
 mod call_cargo;
 mod call_cbmc;
 mod call_goto_cc;
@@ -72,28 +73,37 @@ fn cargokani_main(input_args: Vec<OsString>) -> Result<()> {
         return list_cargo(*list_args, args.verify_opts);
     }
 
-    let session = session::KaniSession::new(args.verify_opts)?;
-
-    if !session.args.common_args.quiet {
-        print_kani_version(InvocationType::CargoKani(input_args));
-    }
-
-    match args.command {
-        Some(CargoKaniSubcommand::Assess(args)) => {
-            return assess::run_assess(session, *args);
+    let mut session = match args.command {
+        Some(CargoKaniSubcommand::Assess(assess_args)) => {
+            let sess = session::KaniSession::new(args.verify_opts)?;
+            return assess::run_assess(sess, *assess_args);
+        }
+        Some(CargoKaniSubcommand::Autoharness(args)) => {
+            let mut sess = session::KaniSession::new(args.verify_opts)?;
+            sess.enable_autoharness();
+            sess.add_auto_harness_args(
+                args.common_autoharness_args.include_function,
+                args.common_autoharness_args.exclude_function,
+            );
+
+            sess
         }
         Some(CargoKaniSubcommand::Playback(args)) => {
             return playback_cargo(*args);
         }
         Some(CargoKaniSubcommand::List(_)) => unreachable!(),
-        None => {}
+        None => session::KaniSession::new(args.verify_opts)?,
+    };
+
+    if !session.args.common_args.quiet {
+        print_kani_version(InvocationType::CargoKani(input_args));
     }
 
     if session.args.assess {
         return assess::run_assess(session, assess::AssessArgs::default());
     }
 
-    let project = project::cargo_project(&session, false)?;
+    let project = project::cargo_project(&mut session, false)?;
     if session.args.only_codegen { Ok(()) } else { verify_project(project, session) }
 }
 
@@ -103,6 +113,21 @@ fn standalone_main() -> Result<()> {
     check_is_valid(&args);
 
     let (session, project) = match args.command {
+        Some(StandaloneSubcommand::Autoharness(args)) => {
+            let mut session = KaniSession::new(args.verify_opts)?;
+            session.enable_autoharness();
+            session.add_auto_harness_args(
+                args.common_autoharness_args.include_function,
+                args.common_autoharness_args.exclude_function,
+            );
+
+            if !session.args.common_args.quiet {
+                print_kani_version(InvocationType::Standalone);
+            }
+
+            let project = project::standalone_project(&args.input, args.crate_name, &session)?;
+            (session, project)
+        }
         Some(StandaloneSubcommand::Playback(args)) => return playback_standalone(*args),
         Some(StandaloneSubcommand::List(list_args)) => {
             return list_standalone(*list_args, args.verify_opts);
diff --git a/kani-driver/src/metadata.rs b/kani-driver/src/metadata.rs
index 94a5393408d3..d112591c6532 100644
--- a/kani-driver/src/metadata.rs
+++ b/kani-driver/src/metadata.rs
@@ -176,6 +176,10 @@ fn find_proof_harnesses<'a>(
     debug!(?targets, "find_proof_harness");
     let mut result = vec![];
     for md in all_harnesses.iter() {
+        // --harnesses should not select automatic harnesses
+        if md.is_automatically_generated {
+            continue;
+        }
         if exact_filter {
             // Check for exact match only
             if targets.contains(&md.pretty_name) {
@@ -224,6 +228,7 @@ pub mod tests {
             goto_file: model_file,
             contract: Default::default(),
             has_loop_contracts: false,
+            is_automatically_generated: false,
         }
     }
 
diff --git a/kani-driver/src/project.rs b/kani-driver/src/project.rs
index da04cc0517ba..2a1aad2c1eff 100644
--- a/kani-driver/src/project.rs
+++ b/kani-driver/src/project.rs
@@ -175,7 +175,7 @@ impl Artifact {
 /// Generate a project using `cargo`.
 /// Accept a boolean to build as many targets as possible. The number of failures in that case can
 /// be collected from the project.
-pub fn cargo_project(session: &KaniSession, keep_going: bool) -> Result<Project> {
+pub fn cargo_project(session: &mut KaniSession, keep_going: bool) -> Result<Project> {
     let outputs = session.cargo_build(keep_going)?;
     let outdir = outputs.outdir.canonicalize()?;
     // For the MIR Linker we know there is only one metadata per crate. Use that in our favor.
diff --git a/kani-driver/src/session.rs b/kani-driver/src/session.rs
index 187a17ae6981..6645db06e45e 100644
--- a/kani-driver/src/session.rs
+++ b/kani-driver/src/session.rs
@@ -17,6 +17,9 @@ use tokio::process::Command as TokioCommand;
 use tracing::level_filters::LevelFilter;
 use tracing_subscriber::{EnvFilter, Registry, layer::SubscriberExt};
 
+pub const BUG_REPORT_URL: &str =
+    "https://github.com/model-checking/kani/issues/new?labels=bug&template=bug_report.md";
+
 /// Environment variable used to control this session log tracing.
 /// This is the same variable used to control `kani-compiler` logs. Note that you can still control
 /// the driver logs separately, by using the logger directives to  select the kani-driver crate.
@@ -28,6 +31,12 @@ pub struct KaniSession {
     /// The common command-line arguments
     pub args: VerificationArgs,
 
+    /// Automatically verify functions in the crate, in addition to running manual harnesses.
+    pub auto_harness: bool,
+
+    /// The arguments that will be passed to the target package, i.e. kani_compiler.
+    pub pkg_args: Vec<String>,
+
     /// Include all publicly-visible symbols in the generated goto binary, not just those reachable from
     /// a proof harness. Useful when attempting to verify things that were not annotated with kani
     /// proof attributes.
@@ -62,6 +71,8 @@ impl KaniSession {
 
         Ok(KaniSession {
             args,
+            auto_harness: false,
+            pkg_args: vec!["--".to_string()],
             codegen_tests: false,
             kani_compiler: install.kani_compiler()?,
             kani_lib_c: install.kani_lib_c()?,
@@ -88,13 +99,20 @@ impl KaniSession {
     /// Determine which symbols Kani should codegen (i.e. by slicing away symbols
     /// that are considered unreachable.)
     pub fn reachability_mode(&self) -> ReachabilityMode {
-        if self.codegen_tests { ReachabilityMode::Tests } else { ReachabilityMode::ProofHarnesses }
+        if self.codegen_tests {
+            ReachabilityMode::Tests
+        } else if self.auto_harness {
+            ReachabilityMode::AllFns
+        } else {
+            ReachabilityMode::ProofHarnesses
+        }
     }
 }
 
 #[derive(Debug, Copy, Clone, Display)]
 #[strum(serialize_all = "snake_case")]
 pub enum ReachabilityMode {
+    AllFns,
     #[strum(to_string = "harnesses")]
     ProofHarnesses,
     Tests,
diff --git a/kani_metadata/src/harness.rs b/kani_metadata/src/harness.rs
index 6932b15dc1a7..227fe8df09d4 100644
--- a/kani_metadata/src/harness.rs
+++ b/kani_metadata/src/harness.rs
@@ -38,6 +38,8 @@ pub struct HarnessMetadata {
     pub contract: Option<AssignsContract>,
     /// If the harness contains some usage of loop contracts.
     pub has_loop_contracts: bool,
+    /// If the harness was automatically generated or manually written.
+    pub is_automatically_generated: bool,
 }
 
 /// The attributes added by the user to control how a harness is executed.
diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs
index 37a05821bd33..d3940160a91a 100644
--- a/library/kani_core/src/lib.rs
+++ b/library/kani_core/src/lib.rs
@@ -434,6 +434,12 @@ macro_rules! kani_intrinsics {
                 }
             }
 
+            /// Used to hold the bodies of automatically generated harnesses.
+            #[kanitool::fn_marker = "AutomaticHarnessIntrinsic"]
+            pub fn automatic_harness() {
+                super::kani_intrinsic()
+            }
+
             /// A way to break the ownerhip rules. Only used by contracts where we can
             /// guarantee it is done safely.
             #[inline(never)]
diff --git a/tests/script-based-pre/cargo_autoharness_contracts/Cargo.toml b/tests/script-based-pre/cargo_autoharness_contracts/Cargo.toml
new file mode 100644
index 000000000000..10a47f48262b
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_contracts/Cargo.toml
@@ -0,0 +1,10 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "cargo_autoharness_contracts"
+version = "0.1.0"
+edition = "2024"
+
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }
diff --git a/tests/script-based-pre/cargo_autoharness_contracts/config.yml b/tests/script-based-pre/cargo_autoharness_contracts/config.yml
new file mode 100644
index 000000000000..38bf8ee6c38c
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_contracts/config.yml
@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: contracts.sh
+expected: contracts.expected
diff --git a/tests/script-based-pre/cargo_autoharness_contracts/contracts.expected b/tests/script-based-pre/cargo_autoharness_contracts/contracts.expected
new file mode 100644
index 000000000000..1e25913b6765
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_contracts/contracts.expected
@@ -0,0 +1,28 @@
+Autoharness: Checking function should_fail::max's contract against all possible inputs...
+assertion\
+	 - Status: FAILURE\
+	 - Description: "|result : &u32| *result == x"
+
+Autoharness: Checking function should_pass::has_loop_contract's contract against all possible inputs...
+should_pass::has_loop_contract.assertion\
+	 - Status: SUCCESS\
+	 - Description: "assertion failed: x == 2"
+
+Autoharness: Checking function should_pass::has_recursion_gcd's contract against all possible inputs...
+assertion\
+	 - Status: SUCCESS\
+	 - Description: "|result : &u8| *result != 0 && x % *result == 0 && y % *result == 0"
+
+Autoharness: Checking function should_pass::div's contract against all possible inputs...
+
+Autoharness: Checking function should_pass::unchecked_mul's contract against all possible inputs...
+arithmetic_overflow\
+	 - Status: SUCCESS\
+	 - Description: "attempt to compute `unchecked_mul` which would overflow"
+
+Verification succeeded for - should_pass::unchecked_mul
+Verification succeeded for - should_pass::has_loop_contract
+Verification succeeded for - should_pass::has_recursion_gcd
+Verification succeeded for - should_pass::div
+Verification failed for - should_fail::max
+Complete - 4 successfully verified functions, 1 failures, 5 total.
diff --git a/tests/script-based-pre/cargo_autoharness_contracts/contracts.sh b/tests/script-based-pre/cargo_autoharness_contracts/contracts.sh
new file mode 100755
index 000000000000..caad53eb8ac4
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_contracts/contracts.sh
@@ -0,0 +1,9 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+cargo kani autoharness -Z unstable-options -Z function-contracts -Z loop-contracts
+# We expect verification to fail, so the above command will produce an exit status of 1
+# However, we don't want the test to fail because of that exit status; we only want it to fail if the expected file doesn't match
+# So, exit with a status code of 0 explicitly.
+exit 0;
diff --git a/tests/script-based-pre/cargo_autoharness_contracts/src/lib.rs b/tests/script-based-pre/cargo_autoharness_contracts/src/lib.rs
new file mode 100644
index 000000000000..c9f9dd3fd1b0
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_contracts/src/lib.rs
@@ -0,0 +1,56 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Test that the autoharness subcommand correctly verifies contracts,
+// i.e., that it detects the presence of a contract and generates a contract
+// harness instead of a standard harness.
+
+#![feature(stmt_expr_attributes)]
+#![feature(proc_macro_hygiene)]
+
+mod should_pass {
+    #[kani::requires(divisor != 0)]
+    fn div(dividend: u32, divisor: u32) -> u32 {
+        dividend / divisor
+    }
+
+    #[kani::requires(x != 0 && y != 0)]
+    #[kani::ensures(|result : &u8| *result != 0 && x % *result == 0 && y % *result == 0)]
+    #[kani::recursion]
+    fn has_recursion_gcd(x: u8, y: u8) -> u8 {
+        let mut max = x;
+        let mut min = y;
+        if min > max {
+            let val = max;
+            max = min;
+            min = val;
+        }
+
+        let res = max % min;
+        if res == 0 { min } else { has_recursion_gcd(min, res) }
+    }
+
+    fn has_loop_contract() {
+        let mut x: u8 = kani::any_where(|i| *i >= 2);
+
+        #[kani::loop_invariant(x >= 2)]
+        while x > 2 {
+            x = x - 1;
+        }
+
+        assert!(x == 2);
+    }
+
+    // Test that we can autoharness functions for unsafe functions with contracts
+    #[kani::requires(!left.overflowing_mul(rhs).1)]
+    unsafe fn unchecked_mul(left: u8, rhs: u8) -> u8 {
+        left.unchecked_mul(rhs)
+    }
+}
+
+mod should_fail {
+    #[kani::ensures(|result : &u32| *result == x)]
+    fn max(x: u32, y: u32) -> u32 {
+        if x > y { x } else { y }
+    }
+}
diff --git a/tests/script-based-pre/cargo_autoharness_exclude/Cargo.toml b/tests/script-based-pre/cargo_autoharness_exclude/Cargo.toml
new file mode 100644
index 000000000000..cceaa1bb7651
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_exclude/Cargo.toml
@@ -0,0 +1,10 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "cargo_autoharness_include"
+version = "0.1.0"
+edition = "2024"
+
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }
diff --git a/tests/script-based-pre/cargo_autoharness_exclude/config.yml b/tests/script-based-pre/cargo_autoharness_exclude/config.yml
new file mode 100644
index 000000000000..d3c26a0301f4
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_exclude/config.yml
@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: exclude.sh
+expected: exclude.expected
diff --git a/tests/script-based-pre/cargo_autoharness_exclude/exclude.expected b/tests/script-based-pre/cargo_autoharness_exclude/exclude.expected
new file mode 100644
index 000000000000..91d9eb4c399a
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_exclude/exclude.expected
@@ -0,0 +1,4 @@
+Autoharness: Checking function include::simple against all possible inputs...
+VERIFICATION:- SUCCESSFUL
+Verification succeeded for - include::simple
+Complete - 1 successfully verified functions, 0 failures, 1 total.
\ No newline at end of file
diff --git a/tests/script-based-pre/cargo_autoharness_exclude/exclude.sh b/tests/script-based-pre/cargo_autoharness_exclude/exclude.sh
new file mode 100755
index 000000000000..492325dc5c81
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_exclude/exclude.sh
@@ -0,0 +1,5 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+cargo kani autoharness -Z unstable-options --exclude-function exclude
diff --git a/tests/script-based-pre/cargo_autoharness_exclude/src/lib.rs b/tests/script-based-pre/cargo_autoharness_exclude/src/lib.rs
new file mode 100644
index 000000000000..7757239126c0
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_exclude/src/lib.rs
@@ -0,0 +1,23 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Test that the automatic harness generation feature selects functions correctly
+// when --exclude-function is provided.
+
+mod include {
+    fn simple(x: u8, _y: u16) -> u8 {
+        x
+    }
+
+    // Doesn't implement Arbitrary, so still should not be included.
+    fn generic<T>(x: u32, _y: T) -> u32 {
+        x
+    }
+}
+
+// These functions are eligible for autoverification, but are excluded.
+mod excluded {
+    fn simple(x: u8, _y: u16) -> u8 {
+        x
+    }
+}
diff --git a/tests/script-based-pre/cargo_autoharness_filter/Cargo.toml b/tests/script-based-pre/cargo_autoharness_filter/Cargo.toml
new file mode 100644
index 000000000000..41f0d6133106
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_filter/Cargo.toml
@@ -0,0 +1,10 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "cargo_autoharness_filter"
+version = "0.1.0"
+edition = "2024"
+
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }
diff --git a/tests/script-based-pre/cargo_autoharness_filter/config.yml b/tests/script-based-pre/cargo_autoharness_filter/config.yml
new file mode 100644
index 000000000000..90ee1970e96c
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_filter/config.yml
@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: filter.sh
+expected: filter.expected
diff --git a/tests/script-based-pre/cargo_autoharness_filter/filter.expected b/tests/script-based-pre/cargo_autoharness_filter/filter.expected
new file mode 100644
index 000000000000..9db37edf8232
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_filter/filter.expected
@@ -0,0 +1,43 @@
+Autoharness: Checking function yes_harness::f_tuple against all possible inputs...
+Autoharness: Checking function yes_harness::f_maybe_uninit against all possible inputs...
+Autoharness: Checking function yes_harness::f_result against all possible inputs...
+Autoharness: Checking function yes_harness::f_option against all possible inputs...
+Autoharness: Checking function yes_harness::f_array against all possible inputs...
+Autoharness: Checking function yes_harness::f_nonzero_isize against all possible inputs...
+Autoharness: Checking function yes_harness::f_nonzero_i128 against all possible inputs...
+Autoharness: Checking function yes_harness::f_nonzero_i64 against all possible inputs...
+Autoharness: Checking function yes_harness::f_nonzero_i32 against all possible inputs...
+Autoharness: Checking function yes_harness::f_nonzero_i16 against all possible inputs...
+Autoharness: Checking function yes_harness::f_nonzero_i8 against all possible inputs...
+Autoharness: Checking function yes_harness::f_nonzero_usize against all possible inputs...
+Autoharness: Checking function yes_harness::f_nonzero_u128 against all possible inputs...
+Autoharness: Checking function yes_harness::f_nonzero_u64 against all possible inputs...
+Autoharness: Checking function yes_harness::f_nonzero_u32 against all possible inputs...
+Autoharness: Checking function yes_harness::f_nonzero_u16 against all possible inputs...
+Autoharness: Checking function yes_harness::f_nonzero_u8 against all possible inputs...
+Autoharness: Checking function yes_harness::f_f128 against all possible inputs...
+Autoharness: Checking function yes_harness::f_f16 against all possible inputs...
+Autoharness: Checking function yes_harness::f_f64 against all possible inputs...
+Autoharness: Checking function yes_harness::f_f32 against all possible inputs...
+Autoharness: Checking function yes_harness::f_char against all possible inputs...
+Autoharness: Checking function yes_harness::f_bool against all possible inputs...
+Autoharness: Checking function yes_harness::f_isize against all possible inputs...
+Autoharness: Checking function yes_harness::f_i128 against all possible inputs...
+Autoharness: Checking function yes_harness::f_i64 against all possible inputs...
+Autoharness: Checking function yes_harness::f_i32 against all possible inputs...
+Autoharness: Checking function yes_harness::f_i16 against all possible inputs...
+Autoharness: Checking function yes_harness::f_i8 against all possible inputs...
+Autoharness: Checking function yes_harness::f_usize against all possible inputs...
+Autoharness: Checking function yes_harness::f_u128 against all possible inputs...
+Autoharness: Checking function yes_harness::f_u64 against all possible inputs...
+Autoharness: Checking function yes_harness::f_u32 against all possible inputs...
+Autoharness: Checking function yes_harness::f_u16 against all possible inputs...
+Autoharness: Checking function yes_harness::f_u8 against all possible inputs...
+Autoharness: Checking function yes_harness::f_unsupported_return_type against all possible inputs...
+Autoharness: Checking function yes_harness::f_multiple_args against all possible inputs...
+Autoharness: Checking function yes_harness::f_derives_arbitrary against all possible inputs...
+Autoharness: Checking function yes_harness::f_manually_implements_arbitrary against all possible inputs...
+Autoharness: Checking function yes_harness::f_phantom_data against all possible inputs...
+Autoharness: Checking function yes_harness::f_phantom_pinned against all possible inputs...
+Autoharness: Checking function yes_harness::empty_body against all possible inputs...
+Complete - 42 successfully verified functions, 0 failures, 42 total.
\ No newline at end of file
diff --git a/tests/script-based-pre/cargo_autoharness_filter/filter.sh b/tests/script-based-pre/cargo_autoharness_filter/filter.sh
new file mode 100755
index 000000000000..cec2f2e2a10b
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_filter/filter.sh
@@ -0,0 +1,5 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+cargo kani autoharness -Z unstable-options
diff --git a/tests/script-based-pre/cargo_autoharness_filter/src/lib.rs b/tests/script-based-pre/cargo_autoharness_filter/src/lib.rs
new file mode 100644
index 000000000000..bb278c73a2e7
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_filter/src/lib.rs
@@ -0,0 +1,210 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Test that the automatic harness generation feature filters functions correctly,
+// i.e., that it generates harnesses for a function iff:
+//   - It is not itself a harness
+//   - All of its arguments implement Arbitrary, either trivially or through a user-provided implementation
+// The bodies of these functions are purposefully left as simple as possible;
+// the point is not to test the generated harnesses themselves,
+// but only that we generate the harnesses in the first place.
+
+#![feature(f16)]
+#![feature(f128)]
+
+extern crate kani;
+use kani::Arbitrary;
+
+#[derive(Arbitrary)]
+struct DerivesArbitrary {
+    x: u8,
+    y: u32,
+}
+
+struct ManuallyImplementsArbitrary {
+    x: u8,
+    y: u32,
+}
+
+impl Arbitrary for ManuallyImplementsArbitrary {
+    fn any() -> Self {
+        Self { x: kani::any(), y: kani::any() }
+    }
+}
+
+struct DoesntImplementArbitrary {
+    x: u8,
+    y: u32,
+}
+
+mod yes_harness {
+    use crate::{DerivesArbitrary, ManuallyImplementsArbitrary};
+    use std::marker::{PhantomData, PhantomPinned};
+    use std::mem::MaybeUninit;
+    use std::num::NonZero;
+
+    // Kani-provided Arbitrary implementations
+    fn f_u8(x: u8) -> u8 {
+        x
+    }
+    fn f_u16(x: u16) -> u16 {
+        x
+    }
+    fn f_u32(x: u32) -> u32 {
+        x
+    }
+    fn f_u64(x: u64) -> u64 {
+        x
+    }
+    fn f_u128(x: u128) -> u128 {
+        x
+    }
+    fn f_usize(x: usize) -> usize {
+        x
+    }
+    fn f_i8(x: i8) -> i8 {
+        x
+    }
+    fn f_i16(x: i16) -> i16 {
+        x
+    }
+    fn f_i32(x: i32) -> i32 {
+        x
+    }
+    fn f_i64(x: i64) -> i64 {
+        x
+    }
+    fn f_i128(x: i128) -> i128 {
+        x
+    }
+    fn f_isize(x: isize) -> isize {
+        x
+    }
+    fn f_bool(x: bool) -> bool {
+        x
+    }
+    fn f_char(x: char) -> char {
+        x
+    }
+    fn f_f32(x: f32) -> f32 {
+        x
+    }
+    fn f_f64(x: f64) -> f64 {
+        x
+    }
+    fn f_f16(x: f16) -> f16 {
+        x
+    }
+    fn f_f128(x: f128) -> f128 {
+        x
+    }
+    fn f_nonzero_u8(x: NonZero<u8>) -> NonZero<u8> {
+        x
+    }
+    fn f_nonzero_u16(x: NonZero<u16>) -> NonZero<u16> {
+        x
+    }
+    fn f_nonzero_u32(x: NonZero<u32>) -> NonZero<u32> {
+        x
+    }
+    fn f_nonzero_u64(x: NonZero<u64>) -> NonZero<u64> {
+        x
+    }
+    fn f_nonzero_u128(x: NonZero<u128>) -> NonZero<u128> {
+        x
+    }
+    fn f_nonzero_usize(x: NonZero<usize>) -> NonZero<usize> {
+        x
+    }
+    fn f_nonzero_i8(x: NonZero<i8>) -> NonZero<i8> {
+        x
+    }
+    fn f_nonzero_i16(x: NonZero<i16>) -> NonZero<i16> {
+        x
+    }
+    fn f_nonzero_i32(x: NonZero<i32>) -> NonZero<i32> {
+        x
+    }
+    fn f_nonzero_i64(x: NonZero<i64>) -> NonZero<i64> {
+        x
+    }
+    fn f_nonzero_i128(x: NonZero<i128>) -> NonZero<i128> {
+        x
+    }
+    fn f_nonzero_isize(x: NonZero<isize>) -> NonZero<isize> {
+        x
+    }
+    fn f_array(x: [u8; 4]) -> [u8; 4] {
+        x
+    }
+    fn f_option(x: Option<u8>) -> Option<u8> {
+        x
+    }
+    fn f_result(x: Result<u8, u16>) -> Result<u8, u16> {
+        x
+    }
+    fn f_maybe_uninit(x: MaybeUninit<u8>) -> MaybeUninit<u8> {
+        x
+    }
+    fn f_tuple(x: (u8, u16, u32)) -> (u8, u16, u32) {
+        x
+    }
+
+    // The return type doesn't implement Arbitrary, but that shouldn't matter
+    fn f_unsupported_return_type(x: u8) -> Vec<u8> {
+        vec![x]
+    }
+
+    // Multiple arguments of different types, all of which implement Arbitrary
+    fn f_multiple_args(x: u8, y: u16, z: u32) -> (u8, u16, u32) {
+        (x, y, z)
+    }
+
+    // User-defined types that implement Arbitrary
+    fn f_derives_arbitrary(x: DerivesArbitrary) -> DerivesArbitrary {
+        x
+    }
+    fn f_manually_implements_arbitrary(
+        x: ManuallyImplementsArbitrary,
+    ) -> ManuallyImplementsArbitrary {
+        x
+    }
+
+    fn f_phantom_data(x: PhantomData<u8>) -> PhantomData<u8> {
+        x
+    }
+
+    fn f_phantom_pinned(x: PhantomPinned) -> PhantomPinned {
+        x
+    }
+
+    fn empty_body(_x: u8, _y: u16) {}
+}
+
+mod no_harness {
+    use crate::{DerivesArbitrary, DoesntImplementArbitrary};
+    fn unsupported_generic<T>(x: u32, _y: T) -> u32 {
+        x
+    }
+    fn unsupported_ref(x: u32, _y: &i32) -> u32 {
+        x
+    }
+    fn unsupported_const_pointer(x: u32, _y: *const i32) -> u32 {
+        x
+    }
+    fn unsupported_mut_pointer(x: u32, _y: *mut i32) -> u32 {
+        x
+    }
+    fn unsupported_vec(x: u32, _y: Vec<u8>) -> u32 {
+        x
+    }
+    fn unsupported_slice(x: u32, _y: &[u8]) -> u32 {
+        x
+    }
+    fn doesnt_implement_arbitrary(
+        x: DoesntImplementArbitrary,
+        _y: DerivesArbitrary,
+    ) -> DoesntImplementArbitrary {
+        x
+    }
+}
diff --git a/tests/script-based-pre/cargo_autoharness_harnesses_fail/Cargo.toml b/tests/script-based-pre/cargo_autoharness_harnesses_fail/Cargo.toml
new file mode 100644
index 000000000000..948b9e1666a4
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_harnesses_fail/Cargo.toml
@@ -0,0 +1,10 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "cargo_autoharness_harnesses_fail"
+version = "0.1.0"
+edition = "2024"
+
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }
diff --git a/tests/script-based-pre/cargo_autoharness_harnesses_fail/config.yml b/tests/script-based-pre/cargo_autoharness_harnesses_fail/config.yml
new file mode 100644
index 000000000000..f5b3400d03bf
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_harnesses_fail/config.yml
@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: harnesses_fail.sh
+expected: harnesses_fail.expected
diff --git a/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.expected b/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.expected
new file mode 100644
index 000000000000..7ceed3cc019a
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.expected
@@ -0,0 +1,57 @@
+Autoharness: Checking function panic against all possible inputs...
+panic.assertion\
+	 - Status: FAILURE\
+	 - Description: "explicit panic"
+
+Autoharness: Checking function integer_overflow against all possible inputs...
+assertion\
+	 - Status: FAILURE
+	 - Description: "attempt to add with overflow"
+
+Autoharness: Checking function oob_unsafe_array_access against all possible inputs...
+oob_unsafe_array_access.pointer_dereference\
+	 - Status: FAILURE\
+	 - Description: "dereference failure: pointer outside object bounds"
+
+Autoharness: Checking function oob_safe_array_access against all possible inputs...
+assertion\
+	- Status: FAILURE\
+	- Description: "index out of bounds: the length is less than or equal to the given index"
+
+Autoharness: Checking function unchecked_mul against all possible inputs...
+arithmetic_overflow\
+	 - Status: FAILURE\
+	 - Description: "attempt to compute `unchecked_mul` which would overflow"
+
+Verification failed for - panic
+Verification failed for - integer_overflow
+Verification failed for - oob_unsafe_array_access
+Verification failed for - oob_safe_array_access
+Verification failed for - unchecked_mul
+Complete - 0 successfully verified functions, 5 failures, 5 total.
+
+Checking harness panic_harness...
+panic.assertion\
+	 - Status: FAILURE\
+	 - Description: "explicit panic"
+
+Checking harness integer_overflow_harness...
+assertion\
+	 - Status: FAILURE\
+	 - Description: "attempt to add with overflow"
+
+Checking harness oob_unsafe_array_access_harness...
+oob_unsafe_array_access.pointer_dereference\
+	 - Status: FAILURE\
+
+Checking harness oob_safe_array_access_harness...
+assertion\
+	 - Status: FAILURE\
+	 - Description: "index out of bounds: the length is less than or equal to the given index"
+
+Checking harness unchecked_mul_harness...
+arithmetic_overflow\
+	 - Status: FAILURE\
+	 - Description: "attempt to compute `unchecked_mul` which would overflow"
+
+Complete - 0 successfully verified harnesses, 5 failures, 5 total.
diff --git a/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.sh b/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.sh
new file mode 100755
index 000000000000..b34d3203311f
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_harnesses_fail/harnesses_fail.sh
@@ -0,0 +1,9 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+cargo kani autoharness -Z unstable-options
+# We expect verification to fail, so the above command will produce an exit status of 1
+# However, we don't want the test to fail because of that exit status; we only want it to fail if the expected file doesn't match
+# So, exit with a status code of 0 explicitly.
+exit 0;
diff --git a/tests/script-based-pre/cargo_autoharness_harnesses_fail/src/lib.rs b/tests/script-based-pre/cargo_autoharness_harnesses_fail/src/lib.rs
new file mode 100644
index 000000000000..591c6b92ee5e
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_harnesses_fail/src/lib.rs
@@ -0,0 +1,68 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Test the bodies of the automatically generated harnesses:
+// do they catch the same failures as manual ones?
+// Note that this also indirectly tests that the automatic harness
+// subcommand also runs the manual harnesses in the crate.
+
+fn oob_safe_array_access(idx: usize) {
+    let v = vec![1, 2, 3];
+    v[idx];
+}
+
+fn oob_unsafe_array_access(i: usize) -> u32 {
+    let a: &[u32] = &[1, 2, 3];
+    if a.len() == 0 {
+        return 0;
+    }
+    return unsafe { *a.as_ptr().add(i % a.len() + 1) };
+}
+
+fn integer_overflow(x: i32) -> i32 {
+    if x <= i32::MAX - 100 {
+        let add_num = |mut x: i32, z: i64| x += z as i32;
+        add_num(x, 1);
+        // overflow
+        add_num(x, 101);
+    }
+    x
+}
+
+fn panic() {
+    if kani::any() {
+        panic!();
+    }
+}
+
+// Test that we can autoharness functions for unsafe functions
+unsafe fn unchecked_mul(left: u8, rhs: u8) -> u8 {
+    left.unchecked_mul(rhs)
+}
+
+#[kani::proof]
+fn oob_safe_array_access_harness() {
+    oob_safe_array_access(kani::any());
+}
+
+#[kani::proof]
+fn oob_unsafe_array_access_harness() {
+    oob_unsafe_array_access(kani::any());
+}
+
+#[kani::proof]
+fn integer_overflow_harness() {
+    integer_overflow(kani::any());
+}
+
+#[kani::proof]
+fn panic_harness() {
+    panic();
+}
+
+#[kani::proof]
+fn unchecked_mul_harness() {
+    unsafe {
+        unchecked_mul(kani::any(), kani::any());
+    }
+}
diff --git a/tests/script-based-pre/cargo_autoharness_include/Cargo.toml b/tests/script-based-pre/cargo_autoharness_include/Cargo.toml
new file mode 100644
index 000000000000..cceaa1bb7651
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_include/Cargo.toml
@@ -0,0 +1,10 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "cargo_autoharness_include"
+version = "0.1.0"
+edition = "2024"
+
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }
diff --git a/tests/script-based-pre/cargo_autoharness_include/config.yml b/tests/script-based-pre/cargo_autoharness_include/config.yml
new file mode 100644
index 000000000000..8df48ec69865
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_include/config.yml
@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: include.sh
+expected: include.expected
diff --git a/tests/script-based-pre/cargo_autoharness_include/include.expected b/tests/script-based-pre/cargo_autoharness_include/include.expected
new file mode 100644
index 000000000000..91d9eb4c399a
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_include/include.expected
@@ -0,0 +1,4 @@
+Autoharness: Checking function include::simple against all possible inputs...
+VERIFICATION:- SUCCESSFUL
+Verification succeeded for - include::simple
+Complete - 1 successfully verified functions, 0 failures, 1 total.
\ No newline at end of file
diff --git a/tests/script-based-pre/cargo_autoharness_include/include.sh b/tests/script-based-pre/cargo_autoharness_include/include.sh
new file mode 100755
index 000000000000..1b3fcc285c88
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_include/include.sh
@@ -0,0 +1,5 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+cargo kani autoharness -Z unstable-options --include-function include
diff --git a/tests/script-based-pre/cargo_autoharness_include/src/lib.rs b/tests/script-based-pre/cargo_autoharness_include/src/lib.rs
new file mode 100644
index 000000000000..68b30bf7afe8
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_include/src/lib.rs
@@ -0,0 +1,24 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+// Test that the automatic harness generation feature selects functions correctly
+// when --include-function is provided.
+
+// Each function inside this module matches the filter.
+mod include {
+    fn simple(x: u8, _y: u16) -> u8 {
+        x
+    }
+
+    // Doesn't implement Arbitrary, so still should not be included.
+    fn generic<T>(x: u32, _y: T) -> u32 {
+        x
+    }
+}
+
+// These functions are eligible for autoverification, but do not match the filter.
+mod excluded {
+    fn simple(x: u8, _y: u16) -> u8 {
+        x
+    }
+}
diff --git a/tests/script-based-pre/cargo_autoharness_loops_fixme/Cargo.toml b/tests/script-based-pre/cargo_autoharness_loops_fixme/Cargo.toml
new file mode 100644
index 000000000000..57d8cd0f0541
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_loops_fixme/Cargo.toml
@@ -0,0 +1,10 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "cargo_autoharness_loops_fixme"
+version = "0.1.0"
+edition = "2024"
+
+[lints.rust]
+unexpected_cfgs = { level = "warn", check-cfg = ['cfg(kani)'] }
diff --git a/tests/script-based-pre/cargo_autoharness_loops_fixme/config.yml b/tests/script-based-pre/cargo_autoharness_loops_fixme/config.yml
new file mode 100644
index 000000000000..fefb50875c7a
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_loops_fixme/config.yml
@@ -0,0 +1,4 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: loops.sh
+expected: loops.expected
diff --git a/tests/script-based-pre/cargo_autoharness_loops_fixme/loops.expected b/tests/script-based-pre/cargo_autoharness_loops_fixme/loops.expected
new file mode 100644
index 000000000000..4c43332f6db0
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_loops_fixme/loops.expected
@@ -0,0 +1 @@
+It's not yet clear what the ideal output is for this test, so this expected file is just a placeholder.
\ No newline at end of file
diff --git a/tests/script-based-pre/cargo_autoharness_loops_fixme/loops.sh b/tests/script-based-pre/cargo_autoharness_loops_fixme/loops.sh
new file mode 100755
index 000000000000..cec2f2e2a10b
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_loops_fixme/loops.sh
@@ -0,0 +1,5 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+cargo kani autoharness -Z unstable-options
diff --git a/tests/script-based-pre/cargo_autoharness_loops_fixme/src/lib.rs b/tests/script-based-pre/cargo_autoharness_loops_fixme/src/lib.rs
new file mode 100644
index 000000000000..99ba72445b6d
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_loops_fixme/src/lib.rs
@@ -0,0 +1,39 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Test that automatic harnesses terminate on functions with loops.
+
+// Since foo()'s arguments implement Arbitrary, we will attempt to verify it,
+// and enter an infinite loop.
+// Unclear what the best solution to this problem is; perhaps this is just a known limitation
+// and the user needs to specify some command line flag to skip this function,
+// or we can conservatively skip functions with loops that don't have loop contracts.
+fn infinite_loop() {
+    loop {}
+}
+
+/// Euclid's algorithm for calculating the GCD of two numbers
+#[kani::requires(x != 0 && y != 0)]
+#[kani::ensures(|result : &u8| *result != 0 && x % *result == 0 && y % *result == 0)]
+fn gcd(mut x: u8, mut y: u8) -> u8 {
+    (x, y) = (if x > y { x } else { y }, if x > y { y } else { x });
+    loop {
+        let res = x % y;
+        if res == 0 {
+            return y;
+        }
+
+        x = y;
+        y = res;
+    }
+}
+
+// Since we can specify an unwinding bound in a manual harness,
+// the proof will terminate.
+// Automatic harnesses, however, do not support unwinding bounds,
+// so the proof does not terminate.
+#[kani::proof_for_contract(gcd)]
+#[kani::unwind(12)]
+fn gcd_harness() {
+    gcd(kani::any(), kani::any());
+}