From 03e0016a1cc8b719e8bfb3f914d78a5221e0023b Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 29 Jul 2026 01:37:41 +0000
Subject: [PATCH 1/8] Autoharness: opt-in bounded slice and string arguments

Functions taking &[T]/&mut [T] (with T implementing or capable of deriving
Arbitrary) or &str were previously skipped with 'Missing Arbitrary
implementation'; in an evaluation across the top-100 crates.io crates these
argument types alone accounted for ~1400 skipped functions.

With the new --bounded-arguments option, the generated harness produces a
slice of nondeterministic length, backed by a nondeterministic array stored
in a dedicated harness local, via two new models: AnySliceRef returns
'&mut storage[..len]' with nondeterministic len (reborrowed as shared for
&[T] arguments), bounded at 16 elements; AnyStrRef returns the longest
valid-UTF-8 prefix of the nondeterministic bytes, bounded at 8 bytes,
reusing the algorithm of String's BoundedArbitrary implementation
(computing the valid prefix is a deterministic function of the bytes, which
symbolic execution handles well, whereas assuming from_utf8().is_ok() is
intractable even at a bound of 4 bytes; measured cost 10s@4/28s@8/180s@16,
so bound 8 stays within the default 60s harness timeout).

Because a verification result for such a harness only holds up to the
bound -- a bug that requires a larger input will not be found -- bounded
harness generation is strictly opt-in and visibly reported:
- without --bounded-arguments, eligible functions are skipped with the new
  reason 'Requires --bounded-arguments for argument(s) ...';
- with the option, such harnesses are marked '(bounded)' in the summary
  table (via a new HarnessMetadata::is_bounded field), and a note after the
  table spells out the caveat.

Both bounds sit below Kani's default unwinding bound of 20 so that loops
over generated slices can be fully unwound by default. Like raw pointers
(#4678), slice references are supported in argument position only, where
the harness owns the backing storage. Top-level argument verdicts are no
longer inserted into the shared Arbitrary cache at all, eliminating the
argument-position vs. field-position cache-poisoning hazard class
(implements_arbitrary memoizes its own recursion, so repeated argument
types stay cheap).

Towards #3832

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
---
 .../src/reference/experimental/autoharness.md |  22 ++++
 kani-compiler/src/args.rs                     |   5 +
 .../src/kani_middle/codegen_units.rs          | 102 ++++++++-------
 .../src/kani_middle/kani_functions.rs         |   4 +
 kani-compiler/src/kani_middle/metadata.rs     |   3 +
 kani-compiler/src/kani_middle/mod.rs          |  77 +++++++++--
 .../src/kani_middle/transform/automatic.rs    | 122 +++++++++++++++++-
 kani-driver/src/args/autoharness_args.rs      |   7 +
 kani-driver/src/autoharness/mod.rs            |  38 +++++-
 .../src/frontend/tests/schema_utils_test.rs   |   4 +
 kani-driver/src/metadata.rs                   |   1 +
 kani-driver/src/sarif.rs                      |   1 +
 kani_metadata/src/harness.rs                  |   5 +
 kani_metadata/src/lib.rs                      |   5 +
 library/kani_core/src/arbitrary.rs            |  42 ++++++
 .../cargo_autoharness_filter/filter.expected  |   2 +-
 .../cargo_autoharness_slices/Cargo.toml       |  10 ++
 .../cargo_autoharness_slices/config.yml       |   5 +
 .../cargo_autoharness_slices/slices.expected  |  17 +++
 .../cargo_autoharness_slices/slices.sh        |   8 ++
 .../cargo_autoharness_slices/src/lib.rs       |  54 ++++++++
 21 files changed, 462 insertions(+), 72 deletions(-)
 create mode 100644 tests/script-based-pre/cargo_autoharness_slices/Cargo.toml
 create mode 100644 tests/script-based-pre/cargo_autoharness_slices/config.yml
 create mode 100644 tests/script-based-pre/cargo_autoharness_slices/slices.expected
 create mode 100755 tests/script-based-pre/cargo_autoharness_slices/slices.sh
 create mode 100644 tests/script-based-pre/cargo_autoharness_slices/src/lib.rs

diff --git a/docs/src/reference/experimental/autoharness.md b/docs/src/reference/experimental/autoharness.md
index 90e21f54ed3e..c6ff5f965014 100644
--- a/docs/src/reference/experimental/autoharness.md
+++ b/docs/src/reference/experimental/autoharness.md
@@ -145,6 +145,28 @@ Note that automatic harnesses do not *assert* type invariants, e.g., they do not
 To verify that a function preserves an invariant, add a [function contract](contracts.md) such as `#[kani::ensures(|result| result.is_safe())]`;
 autoharness verifies a function against its contract if it has one.
 
+## Bounded Arguments (opt-in: `--bounded-arguments`)
+By default, autoharness only generates harnesses whose nondeterministic inputs cover *all*
+possible values, so that a successful result carries Kani's usual guarantee. Some argument
+types (e.g. slices) can only be generated in a *bounded* fashion; because a bug that requires
+a larger input would then be missed, these are **disabled by default** and require the
+`--bounded-arguments` option. Functions that would become eligible with the option are
+reported in the skipped-functions table with reason "Requires --bounded-arguments". Harnesses
+that use bounded values are marked **"(bounded)"** in the summary table, and a note after the
+table repeats the caveat.
+
+With `--bounded-arguments`, for a function with `&[T]`/`&mut [T]` arguments (where `T`
+implements or can derive `Arbitrary`) or `&str` arguments, the generated harness produces a
+slice of nondeterministic length, backed by nondeterministic storage that lives for the entire
+harness: **up to 16 elements** for slices and **up to 8 bytes** for strings. Strings cover all
+valid UTF-8 contents up to the bound (the generated string is the longest valid-UTF-8 prefix of
+nondeterministic bytes, the same approach as `String`'s `BoundedArbitrary` implementation); the
+smaller bound reflects the cost of reasoning about UTF-8 for symbolic execution. The bounds are
+chosen to stay below the default loop-unwinding bound of 20, so that loops over the slice can
+be fully unwound by default.
+
+Nested slice references (e.g. `&&[u8]`) and slices inside user-defined types remain unsupported.
+
 ## Limitations
 ### Arguments Implementing Arbitrary
 Kani will only generate an automatic harness for a function if it can represent each of its arguments nondeterministically, without bounds.
diff --git a/kani-compiler/src/args.rs b/kani-compiler/src/args.rs
index f99c914a53e5..aae1b0169c3e 100644
--- a/kani-compiler/src/args.rs
+++ b/kani-compiler/src/args.rs
@@ -117,6 +117,11 @@ pub struct Arguments {
     /// See kani_driver::autoharness_args for documentation.
     #[arg(long = "autoharness-exclude-pattern", num_args(1))]
     pub autoharness_excluded_patterns: Vec<String>,
+    /// If we are running the autoharness subcommand, whether to generate harnesses for
+    /// functions whose arguments require bounded nondeterministic values (e.g. slice
+    /// references). See kani_driver::autoharness_args for documentation.
+    #[arg(long = "autoharness-bounded-arguments")]
+    pub autoharness_bounded_arguments: bool,
 }
 
 #[derive(Debug, Clone, Copy, AsRefStr, EnumString, VariantNames, PartialEq, Eq)]
diff --git a/kani-compiler/src/kani_middle/codegen_units.rs b/kani-compiler/src/kani_middle/codegen_units.rs
index c5af5b120699..bd20dbc30a21 100644
--- a/kani-compiler/src/kani_middle/codegen_units.rs
+++ b/kani-compiler/src/kani_middle/codegen_units.rs
@@ -9,13 +9,13 @@
 
 use crate::args::{Arguments, ReachabilityType};
 use crate::kani_middle::attributes::{KaniAttributes, is_proof_harness};
-use crate::kani_middle::autoharness_supported_arg_ty;
 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::stubbing::{check_compatibility, harness_stub_map};
+use crate::kani_middle::{ArgSupport, autoharness_supported_arg_ty};
 use crate::kani_queries::QueryDb;
 use kani_metadata::{
     ArtifactType, AssignsContract, AutoHarnessMetadata, AutoHarnessSkipReason, HarnessMetadata,
@@ -113,7 +113,9 @@ impl CodegenUnits {
                     .set(AutoHarnessMetadata {
                         chosen: chosen
                             .iter()
-                            .map(|func| crate::kani_middle::strip_local_crate_prefix(func.name()))
+                            .map(|(func, _)| {
+                                crate::kani_middle::strip_local_crate_prefix(func.name())
+                            })
                             .collect::<BTreeSet<_>>(),
                         skipped,
                     })
@@ -366,13 +368,13 @@ fn determine_targets(
 /// 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>,
+    verifiable_fns: Vec<(Instance, bool)>,
     kani_harness_intrinsic: FnDef,
     base_filename: &Path,
 ) -> HashMap<Harness, HarnessMetadata> {
     verifiable_fns
         .into_iter()
-        .map(|fn_to_verify| {
+        .map(|(fn_to_verify, is_bounded)| {
             // 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.
@@ -386,6 +388,7 @@ fn get_all_automatic_harnesses(
                 base_filename,
                 &fn_to_verify,
                 harness.mangled_name(),
+                is_bounded,
             );
             (harness, metadata)
         })
@@ -521,7 +524,7 @@ fn automatic_harness_partition(
     args: &Arguments,
     crate_name: &str,
     kani_any_def: FnDef,
-) -> (Vec<Instance>, BTreeMap<String, AutoHarnessSkipReason>) {
+) -> (Vec<(Instance, bool)>, BTreeMap<String, AutoHarnessSkipReason>) {
     let crate_fn_defs = rustc_public::local_crate().fn_defs().into_iter().collect::<FxHashSet<_>>();
     // Filter out CrateItems that are functions, but not functions defined in the crate itself, i.e., rustc-inserted functions
     // (c.f. https://github.com/model-checking/kani/issues/4189)
@@ -539,12 +542,14 @@ fn automatic_harness_partition(
     // Cache whether a type implements or can derive Arbitrary
     let mut ty_arbitrary_cache: FxHashMap<Ty, bool> = FxHashMap::default();
 
-    // If `instance` is not eligible for an automatic harness, return the reason why; if it is eligible, return None.
+    // If `instance` is not eligible for an automatic harness, return the reason why (`Err`); if it
+    // is eligible, return whether its harness requires *bounded* nondeterministic arguments
+    // (`Ok(true)` iff so).
     // Note that we only return one reason for ineligiblity, when there could be multiple;
     // we can revisit this implementation choice in the future if users request more verbose output.
-    let mut skip_reason = |instance: Instance| -> Option<AutoHarnessSkipReason> {
+    let mut skip_reason = |instance: Instance| -> Result<bool, AutoHarnessSkipReason> {
         if !instance.has_body() {
-            return Some(AutoHarnessSkipReason::NoBody);
+            return Err(AutoHarnessSkipReason::NoBody);
         }
 
         // Preprend the crate name so that users can filter out entire crates using the existing function filter flags.
@@ -560,55 +565,58 @@ fn automatic_harness_partition(
             || name.contains("kani::Arbitrary")
             || name.contains("kani::Invariant")
         {
-            return Some(AutoHarnessSkipReason::KaniImpl);
+            return Err(AutoHarnessSkipReason::KaniImpl);
         }
 
         if autoharness_filtered_out(&name, &included_set, &excluded_set) {
-            return Some(AutoHarnessSkipReason::UserFilter);
+            return Err(AutoHarnessSkipReason::UserFilter);
         }
 
         // Each argument of `instance` must be supported by automatic harness generation, i.e.,
-        // implement Arbitrary (or be capable of deriving it), or be a raw pointer,
+        // implement Arbitrary (or be capable of deriving it), be a raw pointer, or -- if the user
+        // opted in via --bounded-arguments -- be a supported slice/string reference,
         // c.f. `autoharness_supported_arg_ty`.
         // Note that generic functions have been instantiated with concrete types at this point,
         // so we know that each of these arguments has a concrete type.
         let mut problematic_args = vec![];
+        let mut bounded_args = vec![];
         for (idx, arg) in body.arg_locals().iter().enumerate() {
-            // Do not cache raw pointer types: `ty_arbitrary_cache` stores whether a type
-            // implements (or can derive) Arbitrary, which is false for raw pointers --
-            // `implements_arbitrary` inserts that verdict when it encounters a raw pointer as an
-            // ADT field. Raw pointers are nevertheless supported as harness arguments, so caching
-            // the argument-position verdict under the same key would poison the cache in one
-            // direction or the other (c.f. `autoharness_supported_arg_ty`).
-            let impls_arbitrary = if matches!(arg.ty.kind(), TyKind::RigidTy(RigidTy::RawPtr(..))) {
-                autoharness_supported_arg_ty(arg.ty, kani_any_def, &mut ty_arbitrary_cache)
-            } else {
-                if !ty_arbitrary_cache.contains_key(&arg.ty) {
-                    let supported =
-                        autoharness_supported_arg_ty(arg.ty, kani_any_def, &mut ty_arbitrary_cache);
-                    ty_arbitrary_cache.insert(arg.ty, supported);
-                }
-                *ty_arbitrary_cache.get(&arg.ty).unwrap()
-            };
-
-            if !impls_arbitrary {
-                // Find the name of the argument by referencing var_debug_info.
-                // Note that enumerate() starts at 0, while rustc_public argument_index starts at 1, hence the idx+1.
-                let arg_name = body
-                    .var_debug_info
-                    .iter()
-                    .find(|var| {
-                        var.argument_index.is_some_and(|arg_idx| idx + 1 == usize::from(arg_idx))
-                    })
-                    .map_or("_".to_string(), |debug_info| debug_info.name.to_string());
-                let arg_type = format!("{}", arg.ty);
-                problematic_args.push((arg_name, arg_type))
+            // Note: we deliberately do not insert the verdict into `ty_arbitrary_cache` here.
+            // The cache stores whether a type implements (or can derive) Arbitrary, which is the
+            // wrong semantics for types that are supported in argument position only (raw
+            // pointers, and slice/string references whose backing storage the harness owns):
+            // caching the argument-position verdict under the same key would poison the cache for
+            // the ADT-field checks. `implements_arbitrary` memoizes its own recursion internally,
+            // so repeated argument types stay cheap.
+            let support =
+                autoharness_supported_arg_ty(arg.ty, kani_any_def, &mut ty_arbitrary_cache);
+
+            if support == ArgSupport::Arbitrary {
+                continue;
+            }
+            // Find the name of the argument by referencing var_debug_info.
+            // Note that enumerate() starts at 0, while rustc_public argument_index starts at 1, hence the idx+1.
+            let arg_name = body
+                .var_debug_info
+                .iter()
+                .find(|var| {
+                    var.argument_index.is_some_and(|arg_idx| idx + 1 == usize::from(arg_idx))
+                })
+                .map_or("_".to_string(), |debug_info| debug_info.name.to_string());
+            let arg_type = format!("{}", arg.ty);
+            match support {
+                ArgSupport::Arbitrary => unreachable!(),
+                ArgSupport::Bounded => bounded_args.push((arg_name, arg_type)),
+                ArgSupport::Unsupported => problematic_args.push((arg_name, arg_type)),
             }
         }
         if !problematic_args.is_empty() {
-            return Some(AutoHarnessSkipReason::MissingArbitraryImpl(problematic_args));
+            return Err(AutoHarnessSkipReason::MissingArbitraryImpl(problematic_args));
         }
-        None
+        if !bounded_args.is_empty() && !args.autoharness_bounded_arguments {
+            return Err(AutoHarnessSkipReason::RequiresBoundedArguments(bounded_args));
+        }
+        Ok(!bounded_args.is_empty())
     };
 
     let mut chosen = vec![];
@@ -640,10 +648,12 @@ fn automatic_harness_partition(
             },
         };
 
-        if let Some(reason) = skip_reason(instance) {
-            skipped.insert(crate::kani_middle::strip_local_crate_prefix(instance.name()), reason);
-        } else {
-            chosen.push(instance);
+        match skip_reason(instance) {
+            Err(reason) => {
+                skipped
+                    .insert(crate::kani_middle::strip_local_crate_prefix(instance.name()), reason);
+            }
+            Ok(is_bounded) => chosen.push((instance, is_bounded)),
         }
     }
 
diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs
index 03817fb91c98..b4ea258288a5 100644
--- a/kani-compiler/src/kani_middle/kani_functions.rs
+++ b/kani-compiler/src/kani_middle/kani_functions.rs
@@ -69,6 +69,10 @@ pub enum KaniModel {
     Any,
     #[strum(serialize = "AnyPtrModel")]
     AnyPtr,
+    #[strum(serialize = "AnySliceRefModel")]
+    AnySliceRef,
+    #[strum(serialize = "AnyStrRefModel")]
+    AnyStrRef,
     #[strum(serialize = "AssumeSafeModel")]
     AssumeSafe,
     #[strum(serialize = "CopyInitStateModel")]
diff --git a/kani-compiler/src/kani_middle/metadata.rs b/kani-compiler/src/kani_middle/metadata.rs
index 5f8287bf64dc..d24248898ab5 100644
--- a/kani-compiler/src/kani_middle/metadata.rs
+++ b/kani-compiler/src/kani_middle/metadata.rs
@@ -42,6 +42,7 @@ pub fn gen_proof_metadata(tcx: TyCtxt, instance: Instance, base_name: &Path) ->
         contract: Default::default(),
         has_loop_contracts: false,
         is_automatically_generated: false,
+        is_bounded: false,
     }
 }
 
@@ -121,6 +122,7 @@ pub fn gen_automatic_proof_metadata(
     base_name: &Path,
     fn_to_verify: &Instance,
     harness_mangled_name: String,
+    is_bounded: bool,
 ) -> HarnessMetadata {
     let def = fn_to_verify.def;
     let pretty_name = readable_name(*fn_to_verify);
@@ -163,5 +165,6 @@ pub fn gen_automatic_proof_metadata(
         contract: Default::default(),
         has_loop_contracts: false,
         is_automatically_generated: true,
+        is_bounded,
     }
 }
diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs
index 6228db539941..62e301ee9b0c 100644
--- a/kani-compiler/src/kani_middle/mod.rs
+++ b/kani-compiler/src/kani_middle/mod.rs
@@ -9,8 +9,8 @@ use crate::kani_queries::QueryDb;
 use rustc_data_structures::fx::FxHashMap;
 use rustc_hir::{def::DefKind, def_id::DefId as InternalDefId, def_id::LOCAL_CRATE};
 use rustc_middle::ty::TyCtxt;
-use rustc_public::mir::TerminatorKind;
 use rustc_public::mir::mono::{Instance, MonoItem};
+use rustc_public::mir::{Mutability, TerminatorKind};
 use rustc_public::rustc_internal;
 use rustc_public::ty::{
     AdtDef, AdtKind, FnDef, GenericArgKind, GenericArgs, RigidTy, Span as SpanStable, Ty, TyKind,
@@ -400,25 +400,74 @@ fn can_derive_arbitrary(
     }
 }
 
-/// Can an automatic harness generate a nondeterministic value of type `ty` for a harness
-/// argument?
-/// In addition to the types that implement or can derive `Arbitrary`, automatic harnesses support
-/// raw pointer arguments, as long as the pointee type (after peeling all raw pointer layers)
-/// implements or can derive `Arbitrary`: for those, the harness generates a pointer in a
-/// nondeterministic allocation state (null, out of bounds, or valid),
-/// c.f. `KaniModel::AnyPtr`.
-/// Note that raw pointers are only supported as immediate harness arguments (or through other raw
-/// pointers): a raw pointer behind a reference or inside an ADT remains unsupported, since the
-/// pointee storage that the generated harness allocates would not outlive the generated value.
+/// How an automatic harness can generate a nondeterministic value of a given argument type,
+/// c.f. `autoharness_supported_arg_ty`.
+#[derive(Copy, Clone, Debug, Eq, PartialEq)]
+pub enum ArgSupport {
+    /// An unbounded nondeterministic value, via (implemented or compiler-derived) `Arbitrary`.
+    Arbitrary,
+    /// A *bounded* nondeterministic value; verification results only hold up to the bound.
+    /// Only used if the user passed `--bounded-arguments`.
+    Bounded,
+    /// The type is not supported.
+    Unsupported,
+}
+
+/// Determine how an automatic harness can generate a nondeterministic value of type `ty` for a
+/// harness argument.
+/// In addition to the types that implement or can derive `Arbitrary`, automatic harnesses support:
+/// - raw pointer arguments, as long as the pointee type (after peeling all raw pointer layers)
+///   implements or can derive `Arbitrary`: for those, the harness generates a pointer in a
+///   nondeterministic allocation state (null, out of bounds, or valid), c.f. `KaniModel::AnyPtr`;
+/// - slice references (`&[T]`/`&mut [T]`, provided `T` implements or can derive `Arbitrary`) and
+///   string slices (`&str`): for those, the harness generates a slice of *bounded* nondeterministic
+///   length backed by harness-local storage, c.f. `KaniModel::AnySliceRef` and
+///   `KaniModel::AnyStrRef`.
+///
+/// Note that raw pointers and slice/string references are only supported as immediate harness
+/// arguments (raw pointers also through other raw pointers): such a type behind a reference or
+/// inside an ADT remains unsupported, since the pointee/backing storage that the generated harness
+/// allocates would not outlive the generated value.
 fn autoharness_supported_arg_ty(
     ty: Ty,
     kani_any_def: FnDef,
     ty_arbitrary_cache: &mut FxHashMap<Ty, bool>,
-) -> bool {
+) -> ArgSupport {
+    let arbitrary_or_derive = |ty: Ty, cache: &mut FxHashMap<Ty, bool>| {
+        if implements_arbitrary(ty, kani_any_def, cache)
+            || can_derive_arbitrary(ty, kani_any_def, cache)
+        {
+            ArgSupport::Arbitrary
+        } else {
+            ArgSupport::Unsupported
+        }
+    };
+
     if let TyKind::RigidTy(RigidTy::RawPtr(inner_ty, _)) = ty.kind() {
+        // A raw pointer is supported as long as its pointee is: propagate the pointee's verdict,
+        // so a pointer to a bounded pointee (e.g. `*mut &[T]`) is itself reported as bounded.
         autoharness_supported_arg_ty(inner_ty, kani_any_def, ty_arbitrary_cache)
+    } else if let TyKind::RigidTy(RigidTy::Ref(_, inner_ty, inner_mutability)) = ty.kind() {
+        match inner_ty.kind() {
+            TyKind::RigidTy(RigidTy::Slice(elem_ty)) => {
+                if arbitrary_or_derive(elem_ty, ty_arbitrary_cache) == ArgSupport::Arbitrary {
+                    ArgSupport::Bounded
+                } else {
+                    ArgSupport::Unsupported
+                }
+            }
+            // There is no way to obtain a `&mut str` from our nondeterministic byte storage
+            // without breaking the UTF-8 safety invariant on writes, so only support `&str`.
+            TyKind::RigidTy(RigidTy::Str) => {
+                if inner_mutability == Mutability::Not {
+                    ArgSupport::Bounded
+                } else {
+                    ArgSupport::Unsupported
+                }
+            }
+            _ => arbitrary_or_derive(ty, ty_arbitrary_cache),
+        }
     } else {
-        implements_arbitrary(ty, kani_any_def, ty_arbitrary_cache)
-            || can_derive_arbitrary(ty, kani_any_def, ty_arbitrary_cache)
+        arbitrary_or_derive(ty, ty_arbitrary_cache)
     }
 }
diff --git a/kani-compiler/src/kani_middle/transform/automatic.rs b/kani-compiler/src/kani_middle/transform/automatic.rs
index 63e8e0286c92..13bd645ff99b 100644
--- a/kani-compiler/src/kani_middle/transform/automatic.rs
+++ b/kani-compiler/src/kani_middle/transform/automatic.rs
@@ -20,11 +20,11 @@ use rustc_public::CrateDef;
 use rustc_public::mir::mono::Instance;
 use rustc_public::mir::{
     AggregateKind, BasicBlockIdx, Body, BorrowKind, CastKind, Local, MutBorrowKind, Mutability,
-    Operand, Place, Rvalue, SwitchTargets, Terminator, TerminatorKind,
+    Operand, Place, ProjectionElem, Rvalue, SwitchTargets, Terminator, TerminatorKind,
 };
 use rustc_public::ty::{
-    AdtDef, AdtKind, FnDef, GenericArgKind, GenericArgs, Region, RegionKind, RigidTy, Ty, TyKind,
-    UintTy, VariantDef, VariantIdx,
+    AdtDef, AdtKind, FnDef, GenericArgKind, GenericArgs, Region, RegionKind, RigidTy, Ty, TyConst,
+    TyKind, UintTy, VariantDef, VariantIdx,
 };
 use rustc_public_bridge::IndexedVal;
 use tracing::debug;
@@ -38,6 +38,10 @@ struct AnyModels {
     kani_any: FnDef,
     /// The FnDef of KaniModel::AnyPtr
     kani_any_ptr: FnDef,
+    /// The FnDef of KaniModel::AnySliceRef
+    kani_any_slice_ref: FnDef,
+    /// The FnDef of KaniModel::AnyStrRef
+    kani_any_str_ref: FnDef,
     /// The FnDef of KaniModel::AssumeSafe
     kani_assume_safe: FnDef,
 }
@@ -48,6 +52,8 @@ impl AnyModels {
         Self {
             kani_any: *kani_fns.get(&KaniModel::Any.into()).unwrap(),
             kani_any_ptr: *kani_fns.get(&KaniModel::AnyPtr.into()).unwrap(),
+            kani_any_slice_ref: *kani_fns.get(&KaniModel::AnySliceRef.into()).unwrap(),
+            kani_any_str_ref: *kani_fns.get(&KaniModel::AnyStrRef.into()).unwrap(),
             kani_assume_safe: *kani_fns.get(&KaniModel::AssumeSafe.into()).unwrap(),
         }
     }
@@ -149,17 +155,33 @@ impl TransformPass for AutomaticArbitraryPass {
     }
 }
 
-/// Insert a call to kani::any::<ty>() in `body`; return the local storing the result.
+/// The maximum length for nondeterministic slices that automatic harnesses generate.
+/// Verification results for functions taking `&[T]`/`&mut [T]` arguments are only valid up to
+/// this bound. The value must stay below Kani's default unwinding bound (20), so that loops
+/// iterating over such a slice can be fully unwound by default.
+const AUTOHARNESS_SLICE_BOUND: u64 = 16;
+
+/// The maximum length (in bytes) for nondeterministic strings that automatic harnesses
+/// generate. Strings use a smaller bound than slices: the generated string is the longest
+/// valid-UTF-8 prefix of nondeterministic bytes, and reasoning about UTF-8 validity is
+/// expensive enough that 16 nondeterministic bytes exceed Kani's default 60s harness timeout,
+/// while 8 stay well within it.
+const AUTOHARNESS_STR_BOUND: u64 = 8;
+
 /// For raw pointer types, insert a call to the `KaniModel::AnyPtr` model instead, which generates
 /// a pointer in a nondeterministic allocation state (null, out of bounds, or valid);
 /// in the valid case, the pointer points to a nondeterministic value stored in a dedicated local
 /// of `body`, which keeps it alive for as long as the transformed body executes.
+/// For `&[T]`/`&mut [T]`/`&str`, insert calls to the `KaniModel::AnySliceRef`/`AnyStrRef`
+/// models instead, which return a slice of nondeterministic length (bounded by
+/// [AUTOHARNESS_SLICE_BOUND]) backed by a nondeterministic array stored in a dedicated local,
+/// which stays alive for the entire harness.
 /// If `ty` is an ADT that implements `Invariant`, additionally insert a call to the
 /// `KaniModel::AssumeSafe` model (`kani_assume_safe`), which assumes that the nondeterministic
 /// value respects the type's safety invariant, c.f.
 /// <https://rust-lang.github.io/unsafe-code-guidelines/glossary.html#validity-and-safety-invariant>.
 /// Panics if `ty` does not implement Arbitrary (and is not a reference or raw pointer to such a
-/// type).
+/// type, or a reference to a slice or str of such a type).
 fn call_kani_any_for_ty(
     models: AnyModels,
     body: &mut MutableBody,
@@ -168,7 +190,95 @@ fn call_kani_any_for_ty(
     source: &mut SourceInstruction,
     invariant_cache: &mut FxHashMap<Ty, bool>,
 ) -> Local {
-    if let TyKind::RigidTy(RigidTy::Ref(region, inner_ty, inner_mutability)) = ty.kind() {
+    if let TyKind::RigidTy(RigidTy::Ref(region, inner_ty, inner_mutability)) = ty.kind()
+        && matches!(
+            inner_ty.kind(),
+            TyKind::RigidTy(RigidTy::Slice(..)) | TyKind::RigidTy(RigidTy::Str)
+        )
+    {
+        let is_str = matches!(inner_ty.kind(), TyKind::RigidTy(RigidTy::Str));
+        let (elem_ty, model, model_args) = match inner_ty.kind() {
+            TyKind::RigidTy(RigidTy::Slice(elem_ty)) => (
+                elem_ty,
+                models.kani_any_slice_ref,
+                GenericArgs(vec![
+                    GenericArgKind::Type(elem_ty),
+                    GenericArgKind::Const(
+                        TyConst::try_from_target_usize(AUTOHARNESS_SLICE_BOUND).unwrap(),
+                    ),
+                ]),
+            ),
+            TyKind::RigidTy(RigidTy::Str) => (
+                Ty::unsigned_ty(UintTy::U8),
+                models.kani_any_str_ref,
+                GenericArgs(vec![GenericArgKind::Const(
+                    TyConst::try_from_target_usize(AUTOHARNESS_STR_BOUND).unwrap(),
+                )]),
+            ),
+            _ => unreachable!(),
+        };
+
+        // Generate the backing storage: a local holding a nondeterministic array of the
+        // element type. Since it is a local of the harness body, it stays alive for the
+        // entire harness.
+        let bound = if is_str { AUTOHARNESS_STR_BOUND } else { AUTOHARNESS_SLICE_BOUND };
+        let storage_ty = Ty::try_new_array(elem_ty, bound).unwrap();
+        let storage_lcl = call_kani_any_for_ty(
+            models,
+            body,
+            storage_ty,
+            Mutability::Mut,
+            source,
+            invariant_cache,
+        );
+
+        // Pass a mutable reference to the storage to the model, which returns a slice of
+        // nondeterministic (bounded) length.
+        let storage_ref_ty = Ty::new_ref(region.clone(), storage_ty, Mutability::Mut);
+        let storage_ref_lcl =
+            body.new_local(storage_ref_ty, source.span(body.blocks()), Mutability::Not);
+        body.assign_to(
+            Place::from(storage_ref_lcl),
+            Rvalue::Ref(
+                region.clone(),
+                BorrowKind::Mut { kind: MutBorrowKind::Default },
+                storage_lcl.into(),
+            ),
+            source,
+            InsertPosition::Before,
+        );
+        let model_inst = Instance::resolve(model, &model_args).unwrap();
+        // For `&str`, the model already returns the shared-reference type (there is no
+        // `&mut str` in practice); for slices it returns `&mut [T]`.
+        let model_ret_ty =
+            if is_str { ty } else { Ty::new_ref(region.clone(), inner_ty, Mutability::Mut) };
+        let slice_lcl = body.new_local(model_ret_ty, source.span(body.blocks()), mutability);
+        body.insert_call(
+            &model_inst,
+            source,
+            InsertPosition::Before,
+            vec![Operand::Move(Place::from(storage_ref_lcl))],
+            Place::from(slice_lcl),
+        );
+
+        if inner_mutability == Mutability::Not && !is_str {
+            // Reborrow the `&mut [T]` the model returned as `&[T]`.
+            let shared_lcl = body.new_local(ty, source.span(body.blocks()), mutability);
+            body.assign_to(
+                Place::from(shared_lcl),
+                Rvalue::Ref(
+                    region,
+                    BorrowKind::Shared,
+                    Place { local: slice_lcl, projection: vec![ProjectionElem::Deref] },
+                ),
+                source,
+                InsertPosition::Before,
+            );
+            shared_lcl
+        } else {
+            slice_lcl
+        }
+    } else if let TyKind::RigidTy(RigidTy::Ref(region, inner_ty, inner_mutability)) = ty.kind() {
         let inner_lcl =
             call_kani_any_for_ty(models, body, inner_ty, inner_mutability, source, invariant_cache);
         let ref_lcl = body.new_local(ty, source.span(body.blocks()), mutability);
diff --git a/kani-driver/src/args/autoharness_args.rs b/kani-driver/src/args/autoharness_args.rs
index 93d9eb439127..634fd8c0a086 100644
--- a/kani-driver/src/args/autoharness_args.rs
+++ b/kani-driver/src/args/autoharness_args.rs
@@ -23,6 +23,13 @@ pub struct CommonAutoharnessArgs {
     #[arg(long = "exclude-pattern", num_args(1), value_name = "PATTERN")]
     pub exclude_pattern: Vec<String>,
 
+    /// Also create automatic harnesses for functions whose arguments require *bounded*
+    /// nondeterministic values, e.g. slice references (`&[T]`, `&str`). Such harnesses are
+    /// marked "(bounded)" in the output, and their verification results only hold up to the
+    /// bounds; a bug that requires a larger input will not be found.
+    #[arg(long)]
+    pub bounded_arguments: bool,
+
     /// Run the `list` subcommand after generating the automatic harnesses. Note that this option implies --only-codegen.
     #[arg(long)]
     pub list: bool,
diff --git a/kani-driver/src/autoharness/mod.rs b/kani-driver/src/autoharness/mod.rs
index 0e94590e6441..79baf5153dd1 100644
--- a/kani-driver/src/autoharness/mod.rs
+++ b/kani-driver/src/autoharness/mod.rs
@@ -17,7 +17,7 @@ use crate::session::KaniSession;
 use crate::{InvocationType, print_kani_version, project, verify_project};
 use anyhow::Result;
 use comfy_table::Table as PrettyTable;
-use kani_metadata::{AutoHarnessSkipReason, KaniMetadata};
+use kani_metadata::{AutoHarnessSkipReason, HarnessMetadata, KaniMetadata};
 
 const AUTOHARNESS_TIMEOUT: &str = "60s";
 const LOOP_UNWIND_DEFAULT: u32 = 20;
@@ -57,6 +57,7 @@ fn setup_session(session: &mut KaniSession, common_autoharness_args: &CommonAuto
     session.add_auto_harness_args(
         &common_autoharness_args.include_pattern,
         &common_autoharness_args.exclude_pattern,
+        common_autoharness_args.bounded_arguments,
     );
 }
 
@@ -95,7 +96,8 @@ fn print_autoharness_metadata(metadata: Vec<KaniMetadata>) {
         );
         skipped_table.add_rows(autoharness_md.skipped.into_iter().filter_map(|(func, reason)| {
             match reason {
-                AutoHarnessSkipReason::MissingArbitraryImpl(ref args) => Some(vec![
+                AutoHarnessSkipReason::MissingArbitraryImpl(ref args)
+                | AutoHarnessSkipReason::RequiresBoundedArguments(ref args) => Some(vec![
                     md.crate_name.clone(),
                     func,
                     format!(
@@ -162,7 +164,12 @@ impl KaniSession {
     }
 
     /// Add the compiler arguments specific to the `autoharness` subcommand.
-    pub fn add_auto_harness_args(&mut self, included: &[String], excluded: &[String]) {
+    pub fn add_auto_harness_args(
+        &mut self,
+        included: &[String],
+        excluded: &[String],
+        bounded_arguments: bool,
+    ) {
         let mut args = vec![];
         for pattern in included {
             args.push(format!("--autoharness-include-pattern {pattern}"));
@@ -170,6 +177,9 @@ impl KaniSession {
         for pattern in excluded {
             args.push(format!("--autoharness-exclude-pattern {pattern}"));
         }
+        if bounded_arguments {
+            args.push("--autoharness-bounded-arguments".to_string());
+        }
         self.autoharness_compiler_flags = Some(args);
     }
 
@@ -208,20 +218,31 @@ impl KaniSession {
             "Verification Result",
         ]);
 
+        let harness_kind = |harness: &HarnessMetadata| {
+            if harness.is_bounded {
+                format!("{} (bounded)", harness.attributes.kind)
+            } else {
+                harness.attributes.kind.to_string()
+            }
+        };
+        let mut any_bounded = false;
+
         for success in successes {
+            any_bounded |= success.harness.is_bounded;
             verified_fns.add_row(vec![
                 success.harness.crate_name.clone(),
                 success.harness.pretty_name.clone(),
-                success.harness.attributes.kind.to_string(),
+                harness_kind(&success.harness),
                 success.result.status.to_string(),
             ]);
         }
 
         for failure in failures {
+            any_bounded |= failure.harness.is_bounded;
             verified_fns.add_row(vec![
                 failure.harness.crate_name.clone(),
                 failure.harness.pretty_name.clone(),
-                failure.harness.attributes.kind.to_string(),
+                harness_kind(&failure.harness),
                 failure.result.status.to_string(),
             ]);
         }
@@ -230,6 +251,13 @@ impl KaniSession {
             println!("{verified_fns}");
         }
 
+        if any_bounded {
+            println!(
+                "Note: harnesses marked \"(bounded)\" use bounded nondeterministic values for some arguments (--bounded-arguments);\n\
+                 their verification results only hold up to the bounds, i.e., bugs that require larger input values may be missed."
+            );
+        }
+
         if failing > 0 {
             println!(
                 "Note that `kani autoharness` sets default --harness-timeout of {AUTOHARNESS_TIMEOUT} and --default-unwind of {LOOP_UNWIND_DEFAULT}."
diff --git a/kani-driver/src/frontend/tests/schema_utils_test.rs b/kani-driver/src/frontend/tests/schema_utils_test.rs
index f1693cad5a14..73fa92546918 100644
--- a/kani-driver/src/frontend/tests/schema_utils_test.rs
+++ b/kani-driver/src/frontend/tests/schema_utils_test.rs
@@ -62,6 +62,7 @@ fn test_create_harness_metadata_json() {
         contract: None,
         has_loop_contracts: true,
         is_automatically_generated: false,
+        is_bounded: false,
     };
 
     let json = create_harness_metadata_json(&harness);
@@ -89,6 +90,7 @@ fn test_create_verification_result_json() {
         contract: None,
         has_loop_contracts: false,
         is_automatically_generated: false,
+        is_bounded: false,
     };
 
     let properties = vec![
@@ -168,6 +170,7 @@ fn test_create_verification_summary_json_real() {
         contract: None,
         has_loop_contracts: false,
         is_automatically_generated: false,
+        is_bounded: false,
     };
 
     // Create a VerificationResult
@@ -199,6 +202,7 @@ fn test_add_runner_results_to_json_real() {
         contract: None,
         has_loop_contracts: false,
         is_automatically_generated: false,
+        is_bounded: false,
     };
 
     let verification_result = VerificationResult {
diff --git a/kani-driver/src/metadata.rs b/kani-driver/src/metadata.rs
index 94b4a75a5b78..f37b27736484 100644
--- a/kani-driver/src/metadata.rs
+++ b/kani-driver/src/metadata.rs
@@ -179,6 +179,7 @@ pub mod tests {
             contract: Default::default(),
             has_loop_contracts: false,
             is_automatically_generated: false,
+            is_bounded: false,
         }
     }
 
diff --git a/kani-driver/src/sarif.rs b/kani-driver/src/sarif.rs
index 7c63f5fd36e9..cedf4e4e5c06 100644
--- a/kani-driver/src/sarif.rs
+++ b/kani-driver/src/sarif.rs
@@ -296,6 +296,7 @@ mod tests {
             contract: None,
             has_loop_contracts: false,
             is_automatically_generated: false,
+            is_bounded: false,
         }
     }
 
diff --git a/kani_metadata/src/harness.rs b/kani_metadata/src/harness.rs
index 6c90dc269c92..9a8434b30516 100644
--- a/kani_metadata/src/harness.rs
+++ b/kani_metadata/src/harness.rs
@@ -42,6 +42,11 @@ pub struct HarnessMetadata {
     pub has_loop_contracts: bool,
     /// If the harness was automatically generated or manually written.
     pub is_automatically_generated: bool,
+    /// Whether the (automatically generated) harness uses *bounded* nondeterministic values
+    /// for some arguments (e.g. slice references), in which case its verification result only
+    /// holds up to the bounds, c.f. the autoharness --bounded-arguments option.
+    #[serde(default)]
+    pub is_bounded: bool,
 }
 
 /// The attributes added by the user to control how a harness is executed.
diff --git a/kani_metadata/src/lib.rs b/kani_metadata/src/lib.rs
index 4e7fa0d2694b..3152222d438d 100644
--- a/kani_metadata/src/lib.rs
+++ b/kani_metadata/src/lib.rs
@@ -70,6 +70,11 @@ pub enum AutoHarnessSkipReason {
     /// The function does not have a body.
     #[strum(serialize = "The function does not have a body")]
     NoBody,
+    /// The function's arguments are only supported with bounded nondeterministic values, and
+    /// the user did not pass --bounded-arguments.
+    /// (The Vec<(String, String)> contains the list of (name, type) tuples for each such argument.)
+    #[strum(serialize = "Requires --bounded-arguments for argument(s)")]
+    RequiresBoundedArguments(Vec<(String, String)>),
     /// The function doesn't match the user's provided filters.
     #[strum(serialize = "Did not match provided filters")]
     UserFilter,
diff --git a/library/kani_core/src/arbitrary.rs b/library/kani_core/src/arbitrary.rs
index 66e280f67013..1ed78a5e702e 100644
--- a/library/kani_core/src/arbitrary.rs
+++ b/library/kani_core/src/arbitrary.rs
@@ -199,6 +199,48 @@ macro_rules! generate_arbitrary {
             }
         }
 
+        /// Generate a slice of nondeterministic length (at most `N`) referring to a prefix of
+        /// `storage`, a nondeterministic array that the caller keeps alive for as long as the
+        /// returned slice is in use.
+        ///
+        /// This model is used by the compiler to generate nondeterministic `&[T]` / `&mut [T]`
+        /// arguments for automatic harnesses (`kani autoharness`). Note that any verification
+        /// result obtained with a bounded value like this one is valid only up to the bound.
+        #[kanitool::fn_marker = "AnySliceRefModel"]
+        #[inline(never)]
+        #[doc(hidden)]
+        pub fn any_slice_ref<T, const N: usize>(storage: &mut [T; N]) -> &mut [T] {
+            let len: usize = crate::kani::any();
+            crate::kani::assume(len <= N);
+            &mut storage[..len]
+        }
+
+        /// Generate a string slice referring to the longest valid-UTF-8 prefix of `storage`, a
+        /// nondeterministic byte array (at most `N` bytes) that the caller keeps alive for as
+        /// long as the returned slice is in use. This is the same approach as `String`'s
+        /// `BoundedArbitrary` implementation: computing the valid prefix is a deterministic
+        /// function of the nondeterministic bytes, which symbolic execution handles well,
+        /// whereas *assuming* `str::from_utf8(..).is_ok()` over nondeterministic bytes and
+        /// length is intractable even for a handful of bytes. All string contents up to length
+        /// `N` are covered: a string of length `k < N` arises from storage whose byte at index
+        /// `k` starts an invalid sequence.
+        ///
+        /// This model is used by the compiler to generate nondeterministic `&str` arguments for
+        /// automatic harnesses (`kani autoharness`). Note that any verification result obtained
+        /// with a bounded value like this one is valid only up to the bound.
+        #[kanitool::fn_marker = "AnyStrRefModel"]
+        #[inline(never)]
+        #[doc(hidden)]
+        pub fn any_str_ref<const N: usize>(storage: &mut [u8; N]) -> &str {
+            let valid_len = match core_path::str::from_utf8(storage) {
+                Ok(_) => N,
+                // `valid_up_to` is always a character boundary.
+                Err(e) => e.valid_up_to(),
+            };
+            // SAFETY: `storage[..valid_len]` is the longest valid UTF-8 prefix of `storage`.
+            unsafe { core_path::str::from_utf8_unchecked(&storage[..valid_len]) }
+        }
+
         arbitrary_tuple!(A);
         arbitrary_tuple!(A, B);
         arbitrary_tuple!(A, B, C);
diff --git a/tests/script-based-pre/cargo_autoharness_filter/filter.expected b/tests/script-based-pre/cargo_autoharness_filter/filter.expected
index 45736ebefcf3..2e619294cc1c 100644
--- a/tests/script-based-pre/cargo_autoharness_filter/filter.expected
+++ b/tests/script-based-pre/cargo_autoharness_filter/filter.expected
@@ -106,7 +106,7 @@ If you believe that the provided reason is incorrect and Kani should have genera
 |--------------------------+----------------------------------------+----------------------------------------------------------------------------------|
 | cargo_autoharness_filter | no_harness::unsupported_no_arg_name    | Missing Arbitrary implementation for argument(s) _: std::vec::Vec<u8>            |
 |--------------------------+----------------------------------------+----------------------------------------------------------------------------------|
-| cargo_autoharness_filter | no_harness::unsupported_slice          | Missing Arbitrary implementation for argument(s) _y: &[u8]                       |
+| cargo_autoharness_filter | no_harness::unsupported_slice          | Requires --bounded-arguments for argument(s) _y: &[u8]                           |
 |--------------------------+----------------------------------------+----------------------------------------------------------------------------------|
 | cargo_autoharness_filter | no_harness::unsupported_vec            | Missing Arbitrary implementation for argument(s) _y: std::vec::Vec<u8>           |
 +--------------------------+----------------------------------------+----------------------------------------------------------------------------------+
diff --git a/tests/script-based-pre/cargo_autoharness_slices/Cargo.toml b/tests/script-based-pre/cargo_autoharness_slices/Cargo.toml
new file mode 100644
index 000000000000..2b8434555990
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_slices/Cargo.toml
@@ -0,0 +1,10 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+[package]
+name = "cargo_autoharness_slices"
+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_slices/config.yml b/tests/script-based-pre/cargo_autoharness_slices/config.yml
new file mode 100644
index 000000000000..c4335c2dac6f
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_slices/config.yml
@@ -0,0 +1,5 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+script: slices.sh
+expected: slices.expected
+exit_code: 1
diff --git a/tests/script-based-pre/cargo_autoharness_slices/slices.expected b/tests/script-based-pre/cargo_autoharness_slices/slices.expected
new file mode 100644
index 000000000000..0ddc080aa22e
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_slices/slices.expected
@@ -0,0 +1,17 @@
+[without --bounded-arguments]
+| cargo_autoharness_slices | count_a          | Requires --bounded-arguments for argument(s) s: &str        |
+[with --bounded-arguments]
+| cargo_autoharness_slices | nested           | Missing Arbitrary implementation for argument(s) xs: &&[u8] |
+- Status: SATISFIED
+- Status: SATISFIED
+- Status: SATISFIED
+- Status: SATISFIED
+| cargo_autoharness_slices | count_a           | #[kani::proof] (bounded)  | Success             |
+| cargo_autoharness_slices | slice_cover       | #[kani::proof] (bounded)  | Success             |
+| cargo_autoharness_slices | str_cover         | #[kani::proof] (bounded)  | Success             |
+| cargo_autoharness_slices | sum               | #[kani::proof] (bounded)  | Success             |
+| cargo_autoharness_slices | zero_all          | #[kani::proof] (bounded)  | Success             |
+| cargo_autoharness_slices | first             | #[kani::proof] (bounded)  | Failure             |
+| cargo_autoharness_slices | first_byte        | #[kani::proof] (bounded)  | Failure             |
+Note: harnesses marked "(bounded)" use bounded nondeterministic values for some arguments (--bounded-arguments);
+Complete - 5 successfully verified functions, 2 failures, 7 total.
diff --git a/tests/script-based-pre/cargo_autoharness_slices/slices.sh b/tests/script-based-pre/cargo_autoharness_slices/slices.sh
new file mode 100755
index 000000000000..6f6b0c659ed6
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_slices/slices.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+echo "[without --bounded-arguments]"
+cargo kani autoharness -Z autoharness --list 2>&1 | grep -m1 'Requires --bounded-arguments'
+echo "[with --bounded-arguments]"
+cargo kani autoharness -Z autoharness --bounded-arguments
diff --git a/tests/script-based-pre/cargo_autoharness_slices/src/lib.rs b/tests/script-based-pre/cargo_autoharness_slices/src/lib.rs
new file mode 100644
index 000000000000..0fd348b0b226
--- /dev/null
+++ b/tests/script-based-pre/cargo_autoharness_slices/src/lib.rs
@@ -0,0 +1,54 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+// Test that the autoharness subcommand supports slice reference (`&[T]`, `&mut [T]`) and
+// string slice (`&str`) arguments. The generated harness produces a slice of nondeterministic
+// length, bounded by AUTOHARNESS_SLICE_BOUND (16) for slices and AUTOHARNESS_STR_BOUND (8)
+// for strings, backed by nondeterministic harness-local storage, c.f. the `AnySliceRef` and
+// `AnyStrRef` models. The "TEST NOTE" comments explain the expected result per function.
+
+// TEST NOTE: should PASS: summing at most 16 u32s cannot overflow u64.
+pub fn sum(xs: &[u32]) -> u64 {
+    xs.iter().map(|&x| x as u64).sum()
+}
+
+// TEST NOTE: should FAIL: the slice may be empty, so the index may be out of bounds.
+pub fn first(xs: &[u8]) -> u8 {
+    xs[0]
+}
+
+// TEST NOTE: should PASS: writing through a mutable slice.
+pub fn zero_all(xs: &mut [u8]) {
+    for x in xs.iter_mut() {
+        *x = 0;
+    }
+}
+
+// TEST NOTE: should PASS, and the cover checks must be SATISFIED: nonempty slices of
+// nondeterministic contents and length are generated.
+pub fn slice_cover(xs: &[u8]) {
+    kani::cover!(xs.len() == 16 && xs[0] == 255, "maximum-length slice with nondet contents");
+    kani::cover!(xs.is_empty(), "empty slice");
+}
+
+// TEST NOTE: should PASS: iterating over the chars of a nondeterministic string.
+pub fn count_a(s: &str) -> usize {
+    s.chars().filter(|&c| c == 'a').count()
+}
+
+// TEST NOTE: should FAIL: the string may be empty, so the index may be out of bounds.
+pub fn first_byte(s: &str) -> u8 {
+    s.as_bytes()[0]
+}
+
+// TEST NOTE: should PASS, and the cover checks must be SATISFIED: nonempty strings with
+// specific contents are generated, including multi-byte (non-ASCII) characters.
+pub fn str_cover(s: &str) {
+    kani::cover!(s.len() == 3 && s.starts_with('a'), "3-byte string starting with 'a'");
+    kani::cover!(s.chars().next() == Some('\u{e9}'), "string starting with a non-ASCII char");
+}
+
+// TEST NOTE: skipped: nested slice references are not supported (yet).
+pub fn nested(xs: &&[u8]) -> usize {
+    xs.len()
+}

From 4fedca0897968ad9a8488f188f6d4abcded98475 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 30 Jul 2026 03:45:41 +0000
Subject: [PATCH 2/8] Build slice backing arrays element-wise

kani::any::<[T; N]>() is unresolvable when T's Arbitrary implementation is
compiler-derived ([T; N]'s blanket impl requires T: Arbitrary), so slice
arguments with such element types crashed harness generation. Found by
re-running the top-100 crates.io evaluation (e.g. aho-corasick's &[StateID]
arguments); regression-tested with a derivable-element slice argument.

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
---
 .../src/kani_middle/transform/automatic.rs    | 32 +++++++++++++++----
 .../cargo_autoharness_slices/slices.expected  |  8 ++---
 .../cargo_autoharness_slices/src/lib.rs       | 10 ++++++
 3 files changed, 38 insertions(+), 12 deletions(-)

diff --git a/kani-compiler/src/kani_middle/transform/automatic.rs b/kani-compiler/src/kani_middle/transform/automatic.rs
index 13bd645ff99b..2f9562fe0a0c 100644
--- a/kani-compiler/src/kani_middle/transform/automatic.rs
+++ b/kani-compiler/src/kani_middle/transform/automatic.rs
@@ -220,16 +220,34 @@ fn call_kani_any_for_ty(
 
         // Generate the backing storage: a local holding a nondeterministic array of the
         // element type. Since it is a local of the harness body, it stays alive for the
-        // entire harness.
+        // entire harness. The array is built element-wise (rather than via
+        // `kani::any::<[T; N]>()`) so that element types whose Arbitrary implementation the
+        // compiler derives are supported: `<[T; N] as Arbitrary>::any` is unresolvable for
+        // such `T`, whereas each element can be generated through the same path as any other
+        // value of that type.
         let bound = if is_str { AUTOHARNESS_STR_BOUND } else { AUTOHARNESS_SLICE_BOUND };
         let storage_ty = Ty::try_new_array(elem_ty, bound).unwrap();
-        let storage_lcl = call_kani_any_for_ty(
-            models,
-            body,
-            storage_ty,
-            Mutability::Mut,
+        let elem_lcls = (0..bound)
+            .map(|_| {
+                call_kani_any_for_ty(
+                    models,
+                    body,
+                    elem_ty,
+                    Mutability::Not,
+                    source,
+                    invariant_cache,
+                )
+            })
+            .collect::<Vec<_>>();
+        let storage_lcl = body.new_local(storage_ty, source.span(body.blocks()), Mutability::Mut);
+        body.assign_to(
+            Place::from(storage_lcl),
+            Rvalue::Aggregate(
+                AggregateKind::Array(elem_ty),
+                elem_lcls.into_iter().map(|lcl| Operand::Move(Place::from(lcl))).collect(),
+            ),
             source,
-            invariant_cache,
+            InsertPosition::Before,
         );
 
         // Pass a mutable reference to the storage to the model, which returns a slice of
diff --git a/tests/script-based-pre/cargo_autoharness_slices/slices.expected b/tests/script-based-pre/cargo_autoharness_slices/slices.expected
index 0ddc080aa22e..fbe4acbfb75e 100644
--- a/tests/script-based-pre/cargo_autoharness_slices/slices.expected
+++ b/tests/script-based-pre/cargo_autoharness_slices/slices.expected
@@ -1,17 +1,15 @@
 [without --bounded-arguments]
-| cargo_autoharness_slices | count_a          | Requires --bounded-arguments for argument(s) s: &str        |
+| cargo_autoharness_slices | count_a          | Requires --bounded-arguments for argument(s) s: &str              |
 [with --bounded-arguments]
 | cargo_autoharness_slices | nested           | Missing Arbitrary implementation for argument(s) xs: &&[u8] |
 - Status: SATISFIED
-- Status: SATISFIED
-- Status: SATISFIED
-- Status: SATISFIED
 | cargo_autoharness_slices | count_a           | #[kani::proof] (bounded)  | Success             |
 | cargo_autoharness_slices | slice_cover       | #[kani::proof] (bounded)  | Success             |
 | cargo_autoharness_slices | str_cover         | #[kani::proof] (bounded)  | Success             |
 | cargo_autoharness_slices | sum               | #[kani::proof] (bounded)  | Success             |
+| cargo_autoharness_slices | sum_derivable     | #[kani::proof] (bounded)  | Success             |
 | cargo_autoharness_slices | zero_all          | #[kani::proof] (bounded)  | Success             |
 | cargo_autoharness_slices | first             | #[kani::proof] (bounded)  | Failure             |
 | cargo_autoharness_slices | first_byte        | #[kani::proof] (bounded)  | Failure             |
 Note: harnesses marked "(bounded)" use bounded nondeterministic values for some arguments (--bounded-arguments);
-Complete - 5 successfully verified functions, 2 failures, 7 total.
+Complete - 6 successfully verified functions, 2 failures, 8 total.
diff --git a/tests/script-based-pre/cargo_autoharness_slices/src/lib.rs b/tests/script-based-pre/cargo_autoharness_slices/src/lib.rs
index 0fd348b0b226..7a0744e5be9c 100644
--- a/tests/script-based-pre/cargo_autoharness_slices/src/lib.rs
+++ b/tests/script-based-pre/cargo_autoharness_slices/src/lib.rs
@@ -48,6 +48,16 @@ pub fn str_cover(s: &str) {
     kani::cover!(s.chars().next() == Some('\u{e9}'), "string starting with a non-ASCII char");
 }
 
+// TEST NOTE: should PASS: slices of element types whose Arbitrary implementation the
+// compiler derives are supported (the backing array is built element-wise).
+pub struct OnlyDerivable {
+    pub v: u8,
+}
+
+pub fn sum_derivable(xs: &[OnlyDerivable]) -> u64 {
+    xs.iter().map(|x| x.v as u64).sum()
+}
+
 // TEST NOTE: skipped: nested slice references are not supported (yet).
 pub fn nested(xs: &&[u8]) -> usize {
     xs.len()

From 5480676b2b39207c5543a331de211590215d7704 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Wed, 5 Aug 2026 09:41:25 +0000
Subject: [PATCH 3/8] Fix clippy needless_borrow in the summary rendering

Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>
---
 kani-driver/src/autoharness/mod.rs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/kani-driver/src/autoharness/mod.rs b/kani-driver/src/autoharness/mod.rs
index 79baf5153dd1..4367f9ad2957 100644
--- a/kani-driver/src/autoharness/mod.rs
+++ b/kani-driver/src/autoharness/mod.rs
@@ -232,7 +232,7 @@ impl KaniSession {
             verified_fns.add_row(vec![
                 success.harness.crate_name.clone(),
                 success.harness.pretty_name.clone(),
-                harness_kind(&success.harness),
+                harness_kind(success.harness),
                 success.result.status.to_string(),
             ]);
         }
@@ -242,7 +242,7 @@ impl KaniSession {
             verified_fns.add_row(vec![
                 failure.harness.crate_name.clone(),
                 failure.harness.pretty_name.clone(),
-                harness_kind(&failure.harness),
+                harness_kind(failure.harness),
                 failure.result.status.to_string(),
             ]);
         }

From 73c1ab99d2c8904e96d73cb56ea3f8c31602757c Mon Sep 17 00:00:00 2001
From: Felipe Monteiro <felisous@amazon.com>
Date: Sat, 22 Aug 2026 02:30:22 +0000
Subject: [PATCH 4/8] Autoharness: lower str bound to 4 to fit the harness
 timeout

The cargo_autoharness_slices regression test timed out (CBMC hit the 60s
autoharness harness timeout) on the count_a harness across all CI runners.
count_a fully decodes every char (s.chars().filter(...).count()), which
unwinds the decoding loop to the default bound (20) over symbolic bytes; at
8 nondeterministic bytes this blows up to ~3.1M clauses and exceeds 60s.

Lower AUTOHARNESS_STR_BOUND from 8 to 4. This keeps all str_cover cover
checks satisfiable (they need at most 3 bytes) and brings the char-decoding
harness well within the timeout, while slices are unaffected (bound 16).
---
 docs/src/reference/experimental/autoharness.md         |  2 +-
 kani-compiler/src/kani_middle/transform/automatic.rs   | 10 ++++++----
 .../cargo_autoharness_slices/src/lib.rs                |  2 +-
 3 files changed, 8 insertions(+), 6 deletions(-)

diff --git a/docs/src/reference/experimental/autoharness.md b/docs/src/reference/experimental/autoharness.md
index c6ff5f965014..4949314dd3b5 100644
--- a/docs/src/reference/experimental/autoharness.md
+++ b/docs/src/reference/experimental/autoharness.md
@@ -158,7 +158,7 @@ table repeats the caveat.
 With `--bounded-arguments`, for a function with `&[T]`/`&mut [T]` arguments (where `T`
 implements or can derive `Arbitrary`) or `&str` arguments, the generated harness produces a
 slice of nondeterministic length, backed by nondeterministic storage that lives for the entire
-harness: **up to 16 elements** for slices and **up to 8 bytes** for strings. Strings cover all
+harness: **up to 16 elements** for slices and **up to 4 bytes** for strings. Strings cover all
 valid UTF-8 contents up to the bound (the generated string is the longest valid-UTF-8 prefix of
 nondeterministic bytes, the same approach as `String`'s `BoundedArbitrary` implementation); the
 smaller bound reflects the cost of reasoning about UTF-8 for symbolic execution. The bounds are
diff --git a/kani-compiler/src/kani_middle/transform/automatic.rs b/kani-compiler/src/kani_middle/transform/automatic.rs
index 2f9562fe0a0c..909ff99a6c8b 100644
--- a/kani-compiler/src/kani_middle/transform/automatic.rs
+++ b/kani-compiler/src/kani_middle/transform/automatic.rs
@@ -162,11 +162,13 @@ impl TransformPass for AutomaticArbitraryPass {
 const AUTOHARNESS_SLICE_BOUND: u64 = 16;
 
 /// The maximum length (in bytes) for nondeterministic strings that automatic harnesses
-/// generate. Strings use a smaller bound than slices: the generated string is the longest
+/// generate. Strings use a much smaller bound than slices: the generated string is the longest
 /// valid-UTF-8 prefix of nondeterministic bytes, and reasoning about UTF-8 validity is
-/// expensive enough that 16 nondeterministic bytes exceed Kani's default 60s harness timeout,
-/// while 8 stay well within it.
-const AUTOHARNESS_STR_BOUND: u64 = 8;
+/// expensive. On top of that, a harness that decodes every `char` (e.g. `s.chars().count()`)
+/// unwinds the decoding loop up to the default bound (20) over symbolic bytes, so the cost grows
+/// steeply with the number of bytes: 8 bytes already exceed Kani's default 60s harness timeout
+/// for such harnesses, while 4 stay well within it.
+const AUTOHARNESS_STR_BOUND: u64 = 4;
 
 /// For raw pointer types, insert a call to the `KaniModel::AnyPtr` model instead, which generates
 /// a pointer in a nondeterministic allocation state (null, out of bounds, or valid);
diff --git a/tests/script-based-pre/cargo_autoharness_slices/src/lib.rs b/tests/script-based-pre/cargo_autoharness_slices/src/lib.rs
index 7a0744e5be9c..f73c72dd6732 100644
--- a/tests/script-based-pre/cargo_autoharness_slices/src/lib.rs
+++ b/tests/script-based-pre/cargo_autoharness_slices/src/lib.rs
@@ -3,7 +3,7 @@
 
 // Test that the autoharness subcommand supports slice reference (`&[T]`, `&mut [T]`) and
 // string slice (`&str`) arguments. The generated harness produces a slice of nondeterministic
-// length, bounded by AUTOHARNESS_SLICE_BOUND (16) for slices and AUTOHARNESS_STR_BOUND (8)
+// length, bounded by AUTOHARNESS_SLICE_BOUND (16) for slices and AUTOHARNESS_STR_BOUND (4)
 // for strings, backed by nondeterministic harness-local storage, c.f. the `AnySliceRef` and
 // `AnyStrRef` models. The "TEST NOTE" comments explain the expected result per function.
 

From c843fe5a8946e1488183dff41fefec9df554db8c Mon Sep 17 00:00:00 2001
From: Felipe Monteiro <felisous@amazon.com>
Date: Sat, 22 Aug 2026 22:57:24 +0000
Subject: [PATCH 5/8] Autoharness: fix bounded-slices CI timeout and address
 review feedback

- Raise the harness timeout for the cargo_autoharness_slices test so the
  char-decoding count_a harness does not spuriously time out on slow CI
  runners (macos-15-intel).
- Validate the cargo kani --list status in slices.sh instead of masking it
  behind the grep pipeline.
- Assert each of the four cover descriptions together with its SATISFIED
  status, so regressions in boundary/UTF-8 generation are detected.
- Serialize is_bounded in create_harness_metadata_json (--export-json) and
  cover the true case in the unit test.
- Reconcile the autoharness docs so the bounded-arguments exception is not
  contradicted by the 'without bounds' eligibility statement.
- Clarify the AUTOHARNESS_STR_BOUND comment about slow-machine timeouts.
---
 docs/src/reference/experimental/autoharness.md     |  5 ++++-
 .../src/kani_middle/transform/automatic.rs         |  6 ++++--
 kani-driver/src/frontend/schema_utils.rs           |  2 +-
 .../src/frontend/tests/schema_utils_test.rs        | 10 +++++++---
 .../cargo_autoharness_slices/slices.expected       |  9 ++++++++-
 .../cargo_autoharness_slices/slices.sh             | 14 ++++++++++++--
 6 files changed, 36 insertions(+), 10 deletions(-)

diff --git a/docs/src/reference/experimental/autoharness.md b/docs/src/reference/experimental/autoharness.md
index 4949314dd3b5..ac308b675a33 100644
--- a/docs/src/reference/experimental/autoharness.md
+++ b/docs/src/reference/experimental/autoharness.md
@@ -169,7 +169,10 @@ Nested slice references (e.g. `&&[u8]`) and slices inside user-defined types rem
 
 ## Limitations
 ### Arguments Implementing Arbitrary
-Kani will only generate an automatic harness for a function if it can represent each of its arguments nondeterministically, without bounds.
+Kani will only generate an automatic harness for a function if it can represent each of its arguments nondeterministically.
+By default, it must be able to do so *without bounds*; the `--bounded-arguments` option (see above) relaxes this to
+additionally allow argument types that can only be represented up to a bound, such as slice (`&[T]`/`&mut [T]`) and
+string (`&str`) references.
 In technical terms, each of the arguments needs to implement the `Arbitrary`
 trait or be capable of deriving it, or be a reference (mutable or immutable)
 where any of the prior requirements is fulfilled by the referenced type.
diff --git a/kani-compiler/src/kani_middle/transform/automatic.rs b/kani-compiler/src/kani_middle/transform/automatic.rs
index 909ff99a6c8b..cabf24ebe37d 100644
--- a/kani-compiler/src/kani_middle/transform/automatic.rs
+++ b/kani-compiler/src/kani_middle/transform/automatic.rs
@@ -166,8 +166,10 @@ const AUTOHARNESS_SLICE_BOUND: u64 = 16;
 /// valid-UTF-8 prefix of nondeterministic bytes, and reasoning about UTF-8 validity is
 /// expensive. On top of that, a harness that decodes every `char` (e.g. `s.chars().count()`)
 /// unwinds the decoding loop up to the default bound (20) over symbolic bytes, so the cost grows
-/// steeply with the number of bytes: 8 bytes already exceed Kani's default 60s harness timeout
-/// for such harnesses, while 4 stay well within it.
+/// steeply with the number of bytes: on a typical machine 8 bytes already exceed Kani's default
+/// 60s harness timeout for such harnesses, while 4 stay comfortably within it (though a
+/// char-decoding harness can still approach the timeout on slow machines, so callers that must
+/// not time out should raise `--harness-timeout`).
 const AUTOHARNESS_STR_BOUND: u64 = 4;
 
 /// For raw pointer types, insert a call to the `KaniModel::AnyPtr` model instead, which generates
diff --git a/kani-driver/src/frontend/schema_utils.rs b/kani-driver/src/frontend/schema_utils.rs
index 2984f640b004..1c7cad662e70 100644
--- a/kani-driver/src/frontend/schema_utils.rs
+++ b/kani-driver/src/frontend/schema_utils.rs
@@ -235,7 +235,7 @@ pub fn create_harness_metadata_json(h: &HarnessMetadata) -> Value {
         },
         "has_loop_contracts": h.has_loop_contracts,
         "is_automatically_generated": h.is_automatically_generated,
-
+        "is_bounded": h.is_bounded,
     })
 }
 
diff --git a/kani-driver/src/frontend/tests/schema_utils_test.rs b/kani-driver/src/frontend/tests/schema_utils_test.rs
index 73fa92546918..9d2fbfbcbf70 100644
--- a/kani-driver/src/frontend/tests/schema_utils_test.rs
+++ b/kani-driver/src/frontend/tests/schema_utils_test.rs
@@ -61,8 +61,11 @@ fn test_create_harness_metadata_json() {
         attributes: HarnessAttributes::new(HarnessKind::Proof),
         contract: None,
         has_loop_contracts: true,
-        is_automatically_generated: false,
-        is_bounded: false,
+        // A bounded harness is always automatically generated; check that both flags are
+        // serialized so that JSON consumers can tell a bounded autoharness run apart from an
+        // unbounded one.
+        is_automatically_generated: true,
+        is_bounded: true,
     };
 
     let json = create_harness_metadata_json(&harness);
@@ -73,7 +76,8 @@ fn test_create_harness_metadata_json() {
     assert_eq!(json["source"]["start_line"], 10);
     assert_eq!(json["source"]["end_line"], 20);
     assert_eq!(json["has_loop_contracts"], true);
-    assert_eq!(json["is_automatically_generated"], false);
+    assert_eq!(json["is_automatically_generated"], true);
+    assert_eq!(json["is_bounded"], true);
 }
 
 #[test]
diff --git a/tests/script-based-pre/cargo_autoharness_slices/slices.expected b/tests/script-based-pre/cargo_autoharness_slices/slices.expected
index fbe4acbfb75e..ee5339f3a562 100644
--- a/tests/script-based-pre/cargo_autoharness_slices/slices.expected
+++ b/tests/script-based-pre/cargo_autoharness_slices/slices.expected
@@ -2,7 +2,14 @@
 | cargo_autoharness_slices | count_a          | Requires --bounded-arguments for argument(s) s: &str              |
 [with --bounded-arguments]
 | cargo_autoharness_slices | nested           | Missing Arbitrary implementation for argument(s) xs: &&[u8] |
-- Status: SATISFIED
+Status: SATISFIED\
+Description: "maximum-length slice with nondet contents"
+Status: SATISFIED\
+Description: "empty slice"
+Status: SATISFIED\
+Description: "3-byte string starting with 'a'"
+Status: SATISFIED\
+Description: "string starting with a non-ASCII char"
 | cargo_autoharness_slices | count_a           | #[kani::proof] (bounded)  | Success             |
 | cargo_autoharness_slices | slice_cover       | #[kani::proof] (bounded)  | Success             |
 | cargo_autoharness_slices | str_cover         | #[kani::proof] (bounded)  | Success             |
diff --git a/tests/script-based-pre/cargo_autoharness_slices/slices.sh b/tests/script-based-pre/cargo_autoharness_slices/slices.sh
index 6f6b0c659ed6..c82faf7be78f 100755
--- a/tests/script-based-pre/cargo_autoharness_slices/slices.sh
+++ b/tests/script-based-pre/cargo_autoharness_slices/slices.sh
@@ -2,7 +2,17 @@
 # Copyright Kani Contributors
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
+set -eu
+
 echo "[without --bounded-arguments]"
-cargo kani autoharness -Z autoharness --list 2>&1 | grep -m1 'Requires --bounded-arguments'
+# Capture the command status explicitly: piping straight into `grep` would mask a
+# failure of `cargo kani ... --list` (the pipeline would report grep's status).
+list_output=$(cargo kani autoharness -Z autoharness --list 2>&1)
+echo "$list_output" | grep -m1 'Requires --bounded-arguments'
+
 echo "[with --bounded-arguments]"
-cargo kani autoharness -Z autoharness --bounded-arguments
+# `count_a` iterates over every `char` of a nondeterministic string, which is expensive to
+# reason about; on slower CI runners it can exceed the autoharness default 60s harness timeout,
+# so raise it here to keep this (genuinely passing) harness from spuriously timing out.
+# This run reports failures (`first`/`first_byte`), so it exits non-zero (see config.yml).
+cargo kani autoharness -Z autoharness -Z unstable-options --bounded-arguments --harness-timeout 5m

From c7cdb18f86d6e024bcc32c944626330bf97bf463 Mon Sep 17 00:00:00 2001
From: Felipe Monteiro <felisous@amazon.com>
Date: Sat, 22 Aug 2026 23:21:22 +0000
Subject: [PATCH 6/8] Autoharness: qualify per-harness message for bounded runs

The per-harness progress line printed "against all possible inputs" for
every automatically generated harness, including bounded ones, which
contradicts the reporting guarantee that bounded results must not
masquerade as exhaustive. Branch on is_bounded so bounded harnesses print
"against all possible inputs (bounded for some arguments)", and assert the
qualified message in the cargo_autoharness_slices test.
---
 kani-driver/src/harness_runner.rs                    | 12 ++++++++++--
 .../cargo_autoharness_slices/slices.expected         |  1 +
 2 files changed, 11 insertions(+), 2 deletions(-)

diff --git a/kani-driver/src/harness_runner.rs b/kani-driver/src/harness_runner.rs
index 149138a64816..7731193acc94 100644
--- a/kani-driver/src/harness_runner.rs
+++ b/kani-driver/src/harness_runner.rs
@@ -246,14 +246,22 @@ impl KaniSession {
         if !self.args.common_args.quiet {
             // If the harness is automatically generated, pretty_name refers to the function under verification.
             let mut msg = if harness.is_automatically_generated {
+                // A bounded harness only explores some arguments up to a bound, so it does not
+                // check *all* possible inputs; qualify the message accordingly so a bounded run
+                // does not masquerade as exhaustive (c.f. the "(bounded)" marker in the summary).
+                let inputs = if harness.is_bounded {
+                    "all possible inputs (bounded for some arguments)"
+                } else {
+                    "all possible inputs"
+                };
                 if matches!(harness.attributes.kind, HarnessKind::Proof) {
                     format!(
-                        "Autoharness: Checking function {} against all possible inputs...",
+                        "Autoharness: Checking function {} against {inputs}...",
                         harness.pretty_name
                     )
                 } else {
                     format!(
-                        "Autoharness: Checking function {}'s contract against all possible inputs...",
+                        "Autoharness: Checking function {}'s contract against {inputs}...",
                         harness.pretty_name
                     )
                 }
diff --git a/tests/script-based-pre/cargo_autoharness_slices/slices.expected b/tests/script-based-pre/cargo_autoharness_slices/slices.expected
index ee5339f3a562..130f479befce 100644
--- a/tests/script-based-pre/cargo_autoharness_slices/slices.expected
+++ b/tests/script-based-pre/cargo_autoharness_slices/slices.expected
@@ -2,6 +2,7 @@
 | cargo_autoharness_slices | count_a          | Requires --bounded-arguments for argument(s) s: &str              |
 [with --bounded-arguments]
 | cargo_autoharness_slices | nested           | Missing Arbitrary implementation for argument(s) xs: &&[u8] |
+against all possible inputs (bounded for some arguments)...
 Status: SATISFIED\
 Description: "maximum-length slice with nondet contents"
 Status: SATISFIED\

From 327b212b2fd9439390f7490cd0567866ad8fdc26 Mon Sep 17 00:00:00 2001
From: Felipe Monteiro <felisous@amazon.com>
Date: Sat, 22 Aug 2026 23:29:57 +0000
Subject: [PATCH 7/8] Autoharness: document that harnesses do not explore
 cross-argument aliasing

Each reference/pointer/slice/string argument is generated from independent
storage, so autoharness does not explore aliasing between distinct
arguments (e.g. two &T arguments never share an address). This is a
pre-existing underapproximation of all reference arguments -- not specific
to --bounded-arguments -- so document it in the Limitations section rather
than changing generation semantics.
---
 docs/src/reference/experimental/autoharness.md | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/docs/src/reference/experimental/autoharness.md b/docs/src/reference/experimental/autoharness.md
index ac308b675a33..8ca00f4a9edc 100644
--- a/docs/src/reference/experimental/autoharness.md
+++ b/docs/src/reference/experimental/autoharness.md
@@ -179,6 +179,17 @@ where any of the prior requirements is fulfilled by the referenced type.
 Kani will detect if a struct or enum could implement `Arbitrary` and derive it automatically.
 Note that this automatic derivation feature is only available for autoharness.
 
+### Reference and Pointer Arguments
+Each reference, pointer, slice, or string argument is generated from its own independent
+nondeterministic storage. Autoharness therefore does *not* explore aliasing *between* distinct
+arguments: for example, given `fn f(a: &T, b: &T)`, the generated harness always passes two
+references to separate allocations, so `a` and `b` never share an address (`core::ptr::eq(a, b)`
+is always `false`), even though a caller could pass the same reference twice. A successful
+automatic harness is thus an underapproximation with respect to caller-controlled aliasing, in
+the same way that verifying a single monomorphization is an underapproximation for [generic
+functions](#generic-functions). This applies to all reference/pointer arguments and is
+independent of the length bound that `--bounded-arguments` introduces.
+
 ### Generic Functions
 For a generic function, Kani generates a harness for a single monomorphic instantiation of the function:
 it substitutes every type parameter with the first candidate from a fixed list of primitive types

From 016e4eec290b1dc0f04d49681acd72021cad7994 Mon Sep 17 00:00:00 2001
From: Felipe Monteiro <felisous@amazon.com>
Date: Sat, 22 Aug 2026 23:42:37 +0000
Subject: [PATCH 8/8] Autoharness: reference tracking issue #4750 for
 cross-argument aliasing

---
 docs/src/reference/experimental/autoharness.md | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/docs/src/reference/experimental/autoharness.md b/docs/src/reference/experimental/autoharness.md
index 8ca00f4a9edc..a1376d8fdd29 100644
--- a/docs/src/reference/experimental/autoharness.md
+++ b/docs/src/reference/experimental/autoharness.md
@@ -189,6 +189,8 @@ automatic harness is thus an underapproximation with respect to caller-controlle
 the same way that verifying a single monomorphization is an underapproximation for [generic
 functions](#generic-functions). This applies to all reference/pointer arguments and is
 independent of the length bound that `--bounded-arguments` introduces.
+Modeling caller-controlled aliasing between arguments is tracked in
+[#4750](https://github.com/model-checking/kani/issues/4750).
 
 ### Generic Functions
 For a generic function, Kani generates a harness for a single monomorphic instantiation of the function: