Autoharness documentation is out of date and missing several features

The autoharness reference page (docs/src/reference/experimental/autoharness.md) is out of date with the implementation on main. Some sections are now wrong, and several user-visible features are not documented at all.

Incorrect / outdated content

Slices and Vec are no longer always bounded (Autoharness: unbounded slice, mutable slice and Vec arguments #4721). &[T], &mut [T] and Vec<T> arguments whose element type is a primitive integer or float are generated as fresh allocations of nondeterministic length. They are eligible by default (no --bounded-arguments needed) and are not marked "(bounded)". See automatic_harness_partition in kani-compiler/src/kani_middle/codegen_units.rs and UnboundedModels in kani-compiler/src/kani_middle/transform/automatic.rs. The "Bounded Arguments" and "Limitations > Arguments Implementing Arbitrary" sections currently say slices require --bounded-arguments.
Generic functions bounded by Fn/FnMut/FnOnce are no longer skipped. They are instantiated with nondeterministic closure models (fn_bound_candidates, resolve_deferred_fn_slots and NondetFnModels in codegen_units.rs). Arities 0-3 are supported; for reference-taking shapes only arity 1 and 2. The "Generic Functions" section should describe this and its limits.

Undocumented features

Box<T> / Rc<T> / Arc<T> arguments whose pointee implements or can derive Arbitrary are supported and unbounded (SmartPointerModels in kani-compiler/src/kani_middle/mod.rs; test cargo_autoharness_smart_pointers).
Layout niche assumptions. Generated values of types with scalar valid ranges (e.g. NonZero*, Duration's nanoseconds field) are constrained to their valid range (assume_scalar_niche). This is sound and needs no flag, but it explains why such types do not produce false alarms.
Default verification settings. kani autoharness sets --harness-timeout 60s and --default-unwind 20 (kani-driver/src/autoharness/mod.rs). The page only mentions the unwind bound in passing.
The full list of skip reasons. Only "Generic Function" and "Requires --bounded-arguments" are documented. Missing:
- Comptime (can only be called at compile time)
- KaniImpl
- NoBody
- UnsupportedVariadic
- UserFilter
- MissingArbitraryImpl
See AutoHarnessSkipReason in kani_metadata/src/lib.rs.
Additional generic-instantiation rejections:
- SIMD-invalid instantiations (e.g. simd_imin::<T> with a non-SIMD T; invalid_simd_instantiation).
- Functions with const-generic preconditions that the substituted value would violate (has_const_generic_precondition).
Smaller CLI items:
- kani autoharness --std (run on the standard library).
- --list --format <FORMAT>.
- The bound flags (--slice-bound, --string-bound, --bounded-arbitrary-bound) are rejected unless --bounded-arguments is passed.

Suggested restructuring

The page has grown feature by feature. Consider reorganizing it as:

Overview + how it works (pipeline: select functions → generate harness → verify → summary)
Selecting functions (filters, --list, skip reasons)
Generating arguments, split into:
- unbounded: Arbitrary/derive, raw pointers, smart pointers, unbounded slices/Vec, Fn-bound generics, niches
- opt-in under-approximations: --bounded-arguments, --constructor-args
Assumptions and checks (contracts, Invariant, mined invariants / --check-invariants)
Running and reading results (parallelism, defaults, "(bounded)" / "(ctor)" markers)
Soundness caveats in one place (bounds, ctor vacuity Autoharness --constructor-args: an unsatisfiable constructor yields a vacuous (always-Success) harness #4757, mined-invariant heuristic Autoharness --constructor-args: assumed mined invariants may exclude valid values (heuristic under-approximation) #4763, aliasing Autoharness: model caller-controlled aliasing between reference/pointer arguments #4750, single monomorphization)

@Tianshu-Huang

@Tianshu-Huang cc.

I'll take this. Since #4958 also touches this page, I'll start once it lands to avoid conflicts.

The new autoharness book chapter should follow this overall structure. It starts with the core idea, then covers the three phases (select → generate → verify/report), and ends by collecting the soundness caveats and the internals in one place each:

                         ┌────────────────────────────────────┐
                         │      AUTOHARNESS: the core idea    │
                         │  "for each fn: x = any(); f(x)"    │
                         └─────────────────┬──────────────────┘
                                           │
        ┌──────────────────────────────────┼──────────────────────────────────┐
        ▼                                  ▼                                  ▼
┌────────────────┐            ┌─────────────────────────┐          ┌────────────────────┐
│ 1. SELECT      │            │ 2. GENERATE             │          │ 3. VERIFY & REPORT │
│ which fns?     │            │ what goes in each       │          │ run it, read it    │
│                │            │ harness?                │          │                    │
├────────────────┤            ├─────────────────────────┤          ├────────────────────┤
│ • include /    │            │ 2a. ARGUMENTS           │          │ • parallel / -j    │
│   exclude regex│            │   Unbounded (default):  │          │ • terse vs regular │
│ • --list       │            │   ├ Arbitrary / derive  │          │ • 60s timeout,     │
│ • skip reasons │            │   ├ raw pointers        │          │   unwind 20        │
│ • generics:    │            │   ├ Box / Rc / Arc      │          │ • summary table    │
│   pick one     │            │   ├ prim. slices / Vec  │          │ • (bounded) /      │
│   instantiation│            │   ├ Fn-bound closures   │          │   (ctor) markers   │
│   (Fn bounds,  │            │   └ fmt-trait impls     │          │ • bounds note      │
│   SIMD, const) │            │   Opt-in (under-approx):│          └────────────────────┘
└────────────────┘            │   ├ --bounded-arguments │
                              │   └ --constructor-args  │
                              │ 2b. ASSUMPTIONS         │
                              │   ├ contracts (requires)│
                              │   ├ Invariant::is_safe  │
                              │   ├ layout niches       │
                              │   └ mined invariants    │
                              │ 2c. CHECKS              │
                              │   ├ UB / panics (always)│
                              │   ├ contracts (ensures) │
                              │   └ --check-invariants  │
                              └─────────────────────────┘
                                           │
        ┌──────────────────────────────────┴──────────────────────────────────┐
        ▼                                                                     ▼
┌───────────────────────────────────────┐   ┌──────────────────────────────────────────┐
│ SOUNDNESS CAVEATS (what "Success"     │   │ ARCHITECTURE (for contributors)          │
│ does NOT mean)                        │   │ driver → partition → harness pass →      │
│ • one monomorphization only           │   │ codegen → CBMC → summary                 │
│ • no aliasing between args (#4750)    │   │ (see the architecture diagram below)     │
│ • bounded args only up to bound       │   └──────────────────────────────────────────┘
│ • ctor may be vacuous (#4757)         │
│ • mined-invariant heuristic (#4763)   │
└───────────────────────────────────────┘

Architecture diagram (for the contributors section)

┌──────────────────────────── kani-driver ────────────────────────────┐
│ args/autoharness_args.rs   CLI: --include/--exclude-pattern,        │
│                            --bounded-arguments, --constructor-args, │
│                            --check-invariants, --list, bounds       │
│ autoharness/mod.rs  setup_session(): parallel defaults, timeout,    │
│                     unwind, add_auto_harness_args() → --autoharness-*│
│ call_single_file.rs: adds those flags to the kani-compiler call     │
└────────────────┬────────────────────────────────────────────────────┘
                 ▼
┌──────────────────────────── kani-compiler ──────────────────────────┐
│ kani_middle/codegen_units.rs                                        │
│   automatic_harness_partition()  → chosen / skipped (+reasons)      │
│   get_all_automatic_harnesses()  → AutomaticHarnessIntrinsic::<fn>  │
│                                    + gen_automatic_proof_metadata() │
│ kani_middle/transform/automatic.rs                                  │
│   AutomaticHarnessPass    dummy body → [contract init] args = any() │
│                           [assume invariants] f(args) [checks]      │
│   AutomaticArbitraryPass  T::any() for derivable types              │
│ codegen_cprover_gotoc → goto; KaniMetadata { autoharness_md, ... }  │
└────────────────┬────────────────────────────────────────────────────┘
                 ▼
┌──────────────────────────── kani-driver ────────────────────────────┐
│ postprocess_project(): chosen/skipped tables, --list stops here     │
│ harness_runner.rs: CBMC per harness → print_autoharness_summary()   │
└─────────────────────────────────────────────────────────────────────┘

@Tianshu-Huang

@Tianshu-Huang I need more time to review #4958 so don't wait on it to be merged to start working on this one.

@CYJ904

Thank you, the structure is clear!

I wrote my earlier reply last night, before our sync today. After the sync, the team decided that Sriv and I will take the verification-result analysis, and @CYJ904 @acearyanarun @wodex1nhaoIeng will work on this one.

Fill in the soundness caveats of the autoharness reference page

docs(autoharness): document function selection and skip reasons

Document autoharness default settings and the summary table

Document running autoharness on the standard library

Add an architecture overview for autoharness contributors

Polish the autoharness reference page for consistency

Document autoharness assumptions and checks

Clarify autoharness model availability and generation limits

Document the missing "(ctor)" marker for mined-invariant filtering

Add a "How it works" overview to the autoharness docs

Make the "How it works" diagram boxes link to their sections

Restructure and update the autoharness reference page (model-checking…

Navigation Menu

Repository navigation

Autoharness documentation is out of date and missing several features #4979

Incorrect / outdated content

Undocumented features

Suggested restructuring

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Autoharness documentation is out of date and missing several features #4979

Description

Incorrect / outdated content

Undocumented features

Suggested restructuring

Activity

feliperodri commented on Oct 6, 2026

Tianshu-Huang commented on Oct 6, 2026

feliperodri commented on Oct 6, 2026

feliperodri commented on Oct 6, 2026

Tianshu-Huang commented on Oct 7, 2026

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions