Automatic Harness Generation

Recall the harness for estimate_size that we wrote in First Steps:

#[cfg(kani)]
#[kani::proof]
fn check_estimate_size() {
    let x: u32 = kani::any();
    estimate_size(x);
}

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 harnesses and run Kani against them. Kani scans the crate for functions whose arguments it can generate nondeterministically (see Generating harnesses), 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 autoharness

or

# kani autoharness -Z autoharness <FILE>

If Kani can generate all of a function foo’s arguments, 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 function contract, 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>

Similarly, Kani will detect the presence of loop contracts and verify them.

Thus, -Z autoharness implies -Z function-contracts and -Z loop-contracts, i.e., opting into the experimental autoharness feature means that you are also opting into the function contracts and loop contracts features.

Kani generates and runs these harnesses internally—the user only sees the verification results.

For a full list of options, run kani autoharness --help.

To run autoharness on the Rust standard library itself, pass --std to the standalone command and point it at the library directory of a standard library checkout, such as the one in verify-rust-std:

# kani autoharness -Z autoharness --std <PATH>/library

The path must be a directory named library. Kani builds it with cargo -Z build-std through a temporary crate in the target directory, as kani verify-std does. --std is only available on kani autoharness, not on cargo kani autoharness.

When verifying the standard library, only the Kani definitions available to core can be used. Some models are available only in the full kani library: Box, Rc and Arc arguments, unbounded primitive slices and Vecs, and the function models for Fn-bound type parameters. These models are unavailable with --std. Affected arguments are generated with bounded values where core provides a bounded generator and --bounded-arguments is passed; otherwise the function is skipped.

Concrete playback (-Z concrete-playback) is not supported by the autoharness subcommand (#5109).

Example

Using the estimate_size example from First Steps again:

fn estimate_size(x: u32) -> u32 {
    if x < 256 {
        if x < 128 {
            return 1;
        } else {
            return 3;
        }
    } else if x < 1024 {
        if x > 1022 {
            panic!("Oh no, a failing corner case!");
        } else {
            return 5;
        }
    } else {
        if x < 2048 {
            return 7;
        } else {
            return 9;
        }
    }
}

We get (passing --output-format=regular so that the per-check detail is shown, c.f. Parallel verification):

# cargo kani autoharness -Z autoharness --output-format=regular
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.

How it works

For each selected function, autoharness builds the harness you would otherwise write by hand: generate nondeterministic arguments, call the function, and check the result. It works in three phases; click a box to jump to its section:

                         ┌────────────────────────────────────┐
                         │      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 inv. (ctor)   │
                              │ 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)   │
└───────────────────────────────────────┘

Selecting functions

Autoharness considers functions defined in the crate being verified, including free functions, inherent methods, trait-implementation methods, and trait methods with default implementations. Functions from dependencies are not candidates. For each eligible function, Kani selects one automatic harness; functions that fail a selection check are skipped. Kani reports selected functions and visible skip reasons before verification, unless --quiet is specified.

Each candidate function goes through a fixed sequence of selection checks, and the first check it fails determines its skip reason. Kani-internal and compile-time-only functions are rejected before generic instantiation. Generic functions are then instantiated (see Generic Functions), and the instantiated function is checked, in order, for a body, excluded if it is a proof harness or a Kani trait implementation, matched against the include and exclude patterns, checked for an unsupported calling convention, and finally checked for whether its arguments can be generated. The details of argument generation are described in Generating harnesses.

Include and exclude patterns

The autoharness subcommand has options --include-pattern [REGEX] and --exclude-pattern [REGEX] to include and exclude particular functions using regular expressions. When matching, Kani prefixes the function’s path with the crate name. For example, a non-generic function foo in the my_crate crate is matched as my_crate::foo. The selection algorithm is as follows:

• If only --include-patterns are provided, include a function if it matches any of the provided patterns.
• If only --exclude-patterns are provided, include a function if it does not match any of the provided patterns.
• If both are provided, include a function if it matches an include pattern and does not match any of the exclude patterns. Note that this implies that the exclude pattern takes precedence, i.e., if a function matches both an include pattern and an exclude pattern, it will be excluded.

Here are some examples:

# Include functions containing foo but not bar
kani autoharness -Z autoharness --include-pattern 'foo' --exclude-pattern 'bar'

# Include my_crate::foo exactly
kani autoharness -Z autoharness --include-pattern '^my_crate::foo$'

# Include functions in the foo module, but not in foo::bar
kani autoharness -Z autoharness --include-pattern 'foo::.*' --exclude-pattern 'foo::bar::.*'

# Include functions starting with test_, but not if they're in a private module
kani autoharness -Z autoharness --include-pattern 'test_.*' --exclude-pattern '.*::private::.*'

# This ends up including nothing since all foo::bar matches will also contain bar.
# Kani will emit a warning that these options conflict.
kani autoharness -Z autoharness --include-pattern 'foo::bar' --exclude-pattern 'bar'

Note that because Kani prefixes function paths with the crate name, some patterns might match more than you expect. For example, given a function foo_top_level inside crate my_crate, the regex .*::foo_.* will match foo_top_level, since Kani interprets it as my_crate::foo_top_level. To match only foo_ functions inside modules, use a more specific pattern, e.g. .*::[^:]+::foo_.*.

Patterns match the instantiated name of a generic function. For example, my_crate::foo::<i32> does not match ^my_crate::foo$, although an unanchored foo pattern matches it. Regular expressions are unanchored unless explicitly anchored; invalid expressions and patterns containing whitespace are rejected. Kani also warns if an include-pattern string contains an exclude-pattern string.

Generic instantiation happens before include/exclude filtering. Consequently, a generic function for which Kani cannot find an instantiation is reported with the Generic Function skip reason even if the function would not match the supplied filters. The same applies to compile-time-only functions, which are rejected even before instantiation.

Listing functions

Autoharness also accepts --list, which compiles the project and runs the list subcommand, including automatic harnesses, without running verification. Unless --quiet is passed, Kani first prints the selected-functions and skipped-functions tables.

Use --list --format <FORMAT> to choose the output format:

For file-based formats, Kani prints the path of the written file. The --format option requires --list. Combining --quiet with --list --format pretty is not supported.

For example:

# List functions and harnesses without verification
cargo kani autoharness -Z autoharness --list

# Write the list as JSON
cargo kani autoharness -Z autoharness --list --format json

Skip reasons

Autoharness records one skip reason per skipped function: the first failed check in its selection process. The skipped-functions table has Crate, Skipped Function, and Reason for Skipping columns. Reasons visible to users include, in the order the checks run:

Missing argument names are displayed as _. If a function has both unsupported arguments and arguments requiring bounded generation, Missing Arbitrary implementation is the skip reason reported. See Generating harnesses for the supported argument models and Bounded Arguments for the opt-in behavior.

Kani’s internal implementation functions and functions already used as proof harnesses may be excluded internally with the Kani implementation reason, but these entries are not displayed in the skipped-functions table. The selected-functions table contains Crate and Selected Function columns. Where a generic instantiation is chosen, the tables display the instantiated function name (for example, foo::<i32>); a generic function that cannot be instantiated is listed under its uninstantiated name.

Generic Functions

For a generic function, Kani generates a harness for a single monomorphic instantiation: it substitutes concrete types for the function’s type parameters, requires the instantiation to satisfy the trait bounds and where clauses, and erases lifetime parameters.

Kani first tries the following primitive candidate types, using the same type for each type parameter: i32, u32, usize, u8, i64, u64, f64, f32, bool, and char. If no uniform choice works, it searches combinations of candidate types for individual parameters. Alongside the primitives, the candidates can include up to 16 concrete types derived from implementations of the parameter’s trait bounds (for example, a crate-local struct implementing a crate-local trait). This combinatorial search is limited to 256 attempts. If it finds no suitable instantiation, Kani makes one final attempt using () for every type parameter.

For example, given:

fn foo<T: Eq>(x: T, y: T) {
    if x == y {
        panic!("x and y are equal");
    }
}

Kani generates and runs a harness that verifies foo::<i32>, and the summary table shows the instantiated name, e.g.:

| Crate    | Selected Function | Kind of Automatic Harness | Verification Result |
| my_crate | foo::<i32>        | #[kani::proof]            | Failure             |

Verifying a single instantiation is an underapproximation of all of the function’s possible behaviors: a successful result for foo::<i32> does not imply that other instantiations of foo are also safe. Kani makes the chosen instantiation explicit by displaying its name. See Single monomorphization for the implications of this limitation.

Const generic parameters. usize const generic parameters, such as array lengths, are instantiated with the value 2, so an instantiated function name might include ::<2>. Other const-generic parameter types are currently unsupported. Kani also skips a function if its const-generic parameter can reach a const {} block whose evaluation may constrain that parameter (for example, const { assert!(N >= 4) }). This check is conservative: Kani may skip a function even if the substituted value would satisfy the assertion, rather than risk an invalid compile-time evaluation.

Function-trait bounds. For parameters bounded by Fn, FnMut, or FnOnce, Kani can try nondeterministic function models instead of skipping the generic function. The models support zero to three by-value inputs, or one to two inputs involving shared references (including mixed reference/value arguments). The return type must implement Arbitrary. Models can also be selected for signatures that involve the generic function’s other type parameters, when the resulting bounds can be satisfied. If no available model is suitable, the function may be skipped as a generic function. See Fn-bound closures for the model’s behavior and limitations.

Other instantiation failures. Kani may skip a generic function when no candidate satisfies its bounds or the instantiation search reaches its limit. It also rejects candidate instantiations that would call a simd_* intrinsic in the function’s own body with incompatible non-SIMD types or an invalid SIMD comparison-result type; another valid candidate may still be selected. The Generic Function skip-reason detail identifies applicable failures, including unsupported const generics, const-generic preconditions, SIMD constraints, exhausted search attempts, or unsatisfied trait bounds.

If some caller of a generic function is eligible for an automatic harness, then additional monomorphized versions of the generic function may still be reachable (and thus verified) through the caller’s harness.

After Kani selects a function and, when necessary, an instantiation, it generates the harness arguments as described in Generating harnesses.

Generating harnesses

Arguments

Unbounded (default)

Kani uses the following argument generators by default, without requiring --bounded-arguments. Their supported types and modeling limits are described below.

Arguments Implementing Arbitrary

Kani generates an automatic harness when it can generate each of the function’s arguments nondeterministically. For an argument implementing Arbitrary, it uses kani::any(). For a shared or mutable reference to such a type, it generates a value of the referenced type in storage that lives for the entire harness, then passes a reference to it.

For supported structs and enums without an Arbitrary implementation, Kani can synthesize one by generating fields and, for enums, selecting a variant nondeterministically. Private fields are supported, but field generation has additional restrictions: bare reference fields and NonNull fields (including wrappers such as Option<NonNull<T>>) are not synthesized, and types with lifetime arguments cannot use automatic derivation. Other fields must implement Arbitrary or meet the recursive derivation requirements. Automatic derivation is available only for autoharness and does not require adding a derive attribute to the type. The argument models below do not make unsupported field types derivable.

The following sections describe additional argument models. Types that require a bounded generator are covered under Bounded Arguments.

Raw Pointers

For a function with raw pointer arguments (*const T/*mut T, including nested raw pointers), the generated harness produces pointers in a nondeterministic allocation state, provided that the pointee type implements Arbitrary (or can derive it). Each generated pointer is aligned and is either:

• null,
• out of bounds of its allocation (and thus invalid for reads or writes), or
• valid: pointing to a nondeterministic value of the pointee type, which stays allocated for the entire harness.

Therefore, a function that dereferences a raw pointer argument without being able to rule out the null and out-of-bounds states will fail verification. For safe functions, such a failure points at a real robustness issue, since safe code can pass any pointer value. For functions whose safety relies on caller obligations (e.g., unsafe fns with documented preconditions), add function contracts with Kani’s memory predicates such as #[kani::requires(kani::mem::can_dereference(ptr))]: the automatic contract harness assumes the precondition, which excludes the invalid pointer states.

Current limitations of the generated pointers:

• Pointers are always aligned; misaligned-pointer bugs are not covered.
• No pointers to deallocated objects are generated (Kani’s memory predicates cannot reason about those).
• Distinct pointer arguments never alias each other, and the pointee is always initialized in the valid state.
• Raw pointers are only supported as direct arguments (possibly nested in other raw pointers), not behind references or inside user-defined types.

Box, Rc and Arc

Box<T>, Rc<T> and Arc<T> arguments are supported when the sized pointee type T implements Arbitrary or Kani can derive it automatically. Kani generates a nondeterministic pointee and constructs a new smart pointer around it. These arguments require no --bounded-arguments flag and do not add a “(bounded)” marker.

The generation models require allocation support and use the default allocator. They cover the pointee’s generated values; Rc and Arc start with one strong reference and no weak references, so states with existing owners or weak references are not explored. Unsized pointees such as str and [T] are outside these models; some types, such as Box<[T]>, can instead be generated through BoundedArbitrary with --bounded-arguments.

Primitive slices and Vec

Direct &[T], &mut [T] and Vec<T> arguments are generated without a length bound when T is a primitive integer or floating-point type, for example u8, i32 or f64. Each argument uses a fresh allocation with nondeterministic length and contents. The length is restricted only by Rust’s allocation-size requirements. Mutable slices have exclusive backing storage; the generated Vec uses the global allocator and a capacity of len.max(1).

These models require allocation support. They are enabled by default, do not add a “(bounded)” marker, and take precedence over bounded generation even when --bounded-arguments is passed. --slice-bound and --bounded-arbitrary-bound do not limit them. Element types such as bool, char, NonZeroU32 and user-defined structs use the bounded generators instead, when supported.

Unbounded argument length does not remove the loop-unwinding bound. A function that iterates over the input can fail an unwinding assertion if that bound is insufficient; see Loop unwinding. Nested slice references such as &&[u8] and slices inside user-defined types are outside these argument models.

Fn-bound closures

For supported generic parameters bounded by Fn, FnMut or FnOnce, Kani supplies a function item that returns a fresh kani::any() value on each call. The return type must implement Arbitrary. Repeated calls can return different values, even for the same inputs. The function item itself needs no Arbitrary implementation.

Models support zero through three arguments passed by value. For shared-reference inputs, models support one or two arguments, including a mix of shared references and values. The referenced types must be sized. These reference models can satisfy higher-ranked bounds such as for<'a> Fn(&'a T) -> R; there is no corresponding model for higher-ranked mutable references. Eligibility also depends on satisfying the generic function’s other bounds; see Generic Functions.

These models check the function under verification against arbitrary callback results. They do not execute a particular closure’s body or model its captures, mutations or other side effects. Use a handwritten harness when verification depends on a particular callback implementation. See Other limitations for what this means for a Success result, and #4994.

Formatting Trait Implementations

For the fmt methods of Debug, Display, Binary, Octal, LowerHex, UpperHex, LowerExp, UpperExp and Pointer implementations, Kani uses a special harness rather than the general bounded Formatter model. It formats a nondeterministic value of the implementing type into a sink that discards the output: the Formatter is constructed by the core formatting machinery (so it is always valid), and panics or undefined behavior inside the fmt implementation are detected as usual. These harnesses are unbounded with respect to the implementing type (its value is generated with kani::any), so they are generated by default and are unaffected by --bounded-arguments. If the implementing type implements Invariant, the generated value is assumed to satisfy it, as for any other automatic harness.

Current limitations:

• The Formatter carries the default formatting parameters, i.e. it is the one that format! with the trait’s bare specifier ({:?}, {}, {:x}, …) would produce. Code paths that a fmt implementation takes only for a non-default width, precision, fill, alignment, sign, or the alternate flag ({:#?}, {:#x}, and so on) are therefore not covered.
• The sink never fails, so fmt implementations that propagate write errors with ? are not verified against the error path.
• Because the harness goes through core::fmt, the core formatting machinery is verified along with the fmt implementation, so a reported failure may point at a location inside core.
• A fmt method that carries a function contract is not handled this way: the automatic contract harness calls the function directly, so its &mut Formatter argument comes from the bounded Formatter model and requires --bounded-arguments.

Opt-in under-approximations

Bounded argument generation

Some argument types require a bounded generator, including strings and slices whose elements are not primitive integers or floats. Because a bug requiring a larger input would be missed, these generators are disabled by default and require --bounded-arguments. 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 this limitation.

With --bounded-arguments, for a function with &[T]/&mut [T] arguments outside the unbounded primitive models (where T implements or can derive Arbitrary), or with &str, &CStr, &ByteStr or &Wtf8 arguments, the generated harness produces a slice of nondeterministic length, backed by nondeterministic storage that lives for the entire harness: by default up to 16 elements for slices and byte strings, up to 4 bytes for strings and WTF-8 strings, and up to 15 bytes plus the terminating NUL for C strings (which follow the slice bound, less one for the NUL). 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. WTF-8 strings are generated the same way, as the longest well-formed WTF-8 prefix, so they also cover values holding unpaired surrogate code points. 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.

The bounds are configurable with --slice-bound and --string-bound (and --bounded-arbitrary-bound, see below). All three flags require --bounded-arguments and accept positive bounds only. They apply only to bounded generators; the unbounded primitive slice and Vec models continue to use nondeterministic lengths. A larger bound covers more inputs at a higher solver cost. A bound that is not below the effective loop-unwinding bound (--default-unwind, 20 by default) leaves loops over such an argument only partially unwound, and Kani warns when a configured bound reaches it. The note printed after the summary table reports the bounds a run actually used.

&Formatter and &mut Formatter arguments (also requiring --bounded-arguments) are generated by any_formatter: a Formatter over a sink that discards its output, with every formatting option nondeterministic and its width and precision bounded by the slice bound. The sink never fails, so paths that handle a write error are not reached.

Additionally (also requiring --bounded-arguments), for arguments whose type implements BoundedArbitrary (e.g. Vec<bool>, String, or user types deriving it), the harness generates a bounded nondeterministic value with a default bound of 4 (via kani::bounded_any), overridable with --bounded-arbitrary-bound. The same caveat applies: verification results only hold up to the bound. The smaller bound reflects that these values are heap allocated and, for String, involve UTF-8 reasoning, both of which are costly for symbolic execution.

These argument models do not synthesize nested slice references (e.g. &&[u8]) or slice fields inside user-defined types; a source-defined Arbitrary implementation can supply such fields.

Constructor-based generation

By default, when a type does not implement Arbitrary, Kani synthesizes values field by field. For types whose private fields carry a representation invariant (e.g. a date type storing a packed, validated ordinal), raw field synthesis can produce values that violate the invariant, causing false alarms in every harness that generates the type. With --constructor-args, Kani instead generates values of private-field struct types through one of the type’s own constructors, preferring (in order):

1. An assert-guarded representation constructor: an unsafe, #[doc(hidden)], or *_unchecked-named associated function returning Self directly, whose preconditions are stated as assertions (e.g. debug_assert!) rather than validated returns. Kani inlines its body with nondeterministic arguments and converts every validity statement — kani::assert and assert_unchecked calls, panic entry points, and overflow (Assert) checks — into an assumption, so the constructor’s own assertions filter the arguments down to the values the crate considers valid. Calls the constructor makes to further assert-guarded helpers are inlined recursively (bounded in depth and size). Visibility is irrelevant here, since the body is inlined rather than called.
2. Otherwise, a checked public constructor: a public associated function returning Self, Option<Self>, or Result<Self, E>, called with nondeterministic arguments (assuming success for the Option<Self>/Result<Self, E> shapes).

Zero-argument constructors and constructors introducing their own type or const generic parameters are not considered. Constructors may have their own lifetime parameters.

--constructor-args additionally enables mined-invariant filtering: generated struct and enum values are constrained via kani::assume to satisfy the conditions Kani can extract from assertions in the type’s own methods (see Mined invariants). This filtering also applies to types with no usable constructor, at lower formula cost than constructor inlining.

This option is opt-in because it under-approximates: harnesses whose values are generated or constrained this way are marked “(ctor)” in the output. That marker therefore covers all of the mechanisms above — assert-guarded/checked constructors and mined-invariant filtering — and signals that verification results only cover values the chosen mechanism admits; a bug that requires a different value will not be found. Note also that a checked constructor which itself panics for some of its inputs (rather than rejecting them via Option/Result) turns those inputs into harness failures, so this option can trade one class of false alarm for another.

One exception: values of a type that has its own Arbitrary implementation are still filtered by mined invariants, but the harness is currently not marked “(ctor)” and no note is printed; see #4995.

See Soundness caveats.

Assumptions

Assumptions restrict the values and execution paths that the generated harness explores. The following mechanisms supply assumptions before Kani checks the function’s behavior.

Contracts (requires)

When the selected function has a function contract, Kani generates a #[kani::proof_for_contract] harness. The function’s #[kani::requires(...)] preconditions are assumed at entry, so verification covers only inputs that satisfy them. For example, #[kani::requires(x != 0)] excludes x == 0 from the automatic contract harness.

Autoharness does not infer caller obligations from an unsafe fn declaration or its safety documentation. Express those obligations as preconditions to avoid checking the function with inputs its callers are required to exclude; see the raw pointer example.

Type Safety Invariants

If a type implements the Invariant trait, Kani assumes that the nondeterministic struct and enum values it generates for automatic harnesses respect the type’s safety invariant, i.e., each generated value v satisfies v.is_safe(). When Kani synthesizes a struct or enum’s generation field by field, it also assumes the safety invariants of the struct and enum fields it generates, even if the enclosing type does not implement Invariant. For a source-defined Arbitrary implementation, nested invariants must be enforced by that implementation or the enclosing type’s Invariant. Invariants implemented for non-ADT types (e.g., tuples or arrays) are currently not assumed.

This matches the Unsafe Code Guidelines’ definition of a safety invariant: safe code is allowed to assume that the values it receives uphold their types’ safety invariants, so verifying a function against invariant-violating inputs would produce spurious counterexamples.

Layout niches

When Kani automatically derives Arbitrary for a struct or enum, it must respect any compiler-defined restrictions on its fields’ values. A field’s underlying integer type may allow more values than the field type itself. Kani reads the field type’s valid scalar range from the compiler’s layout information and adds kani::assume constraints when generating values.

For example, consider a Month type without an Arbitrary implementation whose field type restricts an underlying u8 to 1..=12. Generating an arbitrary u8 alone would also allow 0 and 13 through 255. Kani constrains it to 1..=12 before constructing the restricted field, so automatic derivation produces only valid month values. This relies on a restriction expressed in the field’s type; Kani does not infer it from the name Month.

Invalid bit patterns that the compiler can use for layout optimizations are called niches. For NonZeroU32, zero is such a pattern. Its existing Arbitrary implementation already excludes zero, so the additional layout assumption is redundant on that generation path; it is needed when automatically synthesizing generation for restricted types that have no such implementation.

These assumptions exclude language-level invalid values, preserving the valid inputs that the generator represents. They require no flag or Invariant implementation and do not add a “(ctor)” marker. They prevent false alarms caused by invalid scalar values; they do not infer additional relationships between fields or application-level invariants.

Mined invariants

Many types state conditions on their fields through assertions in their own inherent methods, such as assert!(self.value >= 1). Kani can mine these assertions, treating a condition as a candidate type invariant when:

• The assertion occurs on every path to a normal return of the method or the relevant enum match arm (post-dominance).
• Its condition is a supported pure expression over self’s fields and constants, including simple field getters whose expressions Kani can extract.
• The same condition is asserted in at least two distinct methods.

For enums, a condition read from a matched variant is applied only to that variant. Requiring assertions in two methods reduces the risk of treating a method’s precondition as a type invariant, but does not prove that the condition holds for every valid value.

Mining currently applies to struct and enum types without generic arguments. Methods can take self by value, shared reference or mutable reference; methods with their own type or const generic parameters are excluded.

Under --constructor-args, the mined conditions are assumed for generated values. This input filtering also applies when the type already implements Arbitrary; such harnesses are currently not marked “(ctor)” (#4995). It can exclude valid values if a mined condition is actually a precondition of the methods rather than an invariant of the type; see Soundness caveats. The separate --check-invariants option checks mined conditions on return values.

Checks

Undefined behavior and panics

By default, automatic harnesses use Kani’s usual checks for the selected function and code reachable from it, including assertions, panics, integer overflow, division by zero and invalid memory accesses. These checks also run when the function has a contract. The inputs they cover depend on the argument models and assumptions above.

See Undefined Behaviour for the forms of undefined behavior Kani can detect and its current limitations, and Verification results for how individual checks are reported.

Contracts (ensures)

For a function with a contract, the automatic contract harness checks each #[kani::ensures(...)] postcondition on return, under the function’s assumed preconditions. For example, #[kani::ensures(|result| result.is_safe())] checks that the returned value respects its type’s safety invariant.

Assuming Invariant::is_safe() for generated inputs does not automatically check it on outputs. Add such a postcondition to verify the returned value’s safety invariant; see function contracts.

--check-invariants

With --check-invariants, Kani asserts the type’s mined invariants on values returned by verified functions. Supported returns include a direct T, a reference to T, or the Some(T)/Ok(T) payload of an Option<T>/Result<T, E>; T must be a struct or enum for which conditions can be mined. None and Err returns do not check a payload. The checks do not recursively unwrap returns such as Option<&T>, inspect tuple or array elements, or check modified input arguments.

Failures include a message identifying the type and the methods that asserted the mined condition. Because mining is heuristic, a failure means the returned value violates a condition asserted by those methods, which may or may not indicate a bug in the returning function. This option checks mined predicates, rather than Invariant::is_safe(), and can be used independently of --constructor-args. For functions with contracts, these additional checks run under the same preconditions and supplement the postcondition checks.

Verifying and reading results

Parallel verification

Since autoharness typically generates many harnesses, it verifies them in parallel by default, i.e. as if --jobs (the thread pool’s default number of threads, normally one per logical CPU) and --output-format=terse had been passed. Note that plain kani/cargo kani verification is unaffected and remains sequential by default.

To override the default:

• -j <N> / --jobs=<N> caps the number of harnesses verified concurrently. Each thread runs its own CBMC process, so peak memory grows with the number of threads; lower <N> if a run exhausts the available memory. --jobs=1 keeps the terse output but verifies sequentially.
• --output-format=regular verifies harnesses sequentially, with Kani’s default, more detailed per-check output. (Parallel verification requires terse output, because interleaved detailed output is hard to read; passing --jobs together with --output-format=regular is therefore an error.)

In parallel runs each harness result line is prefixed with the thread that produced it, and results arrive in nondeterministic order; the summary table printed at the end is always sorted.

Default settings

Unless you pass them yourself, kani autoharness sets two verification options so that a single harness cannot hold up the whole run:

• --harness-timeout 60s: a harness whose verification takes longer than 60 seconds is stopped and reported as a failure.
• --default-unwind 20: loops are unwound up to 20 times. Automatic harnesses carry no #[kani::unwind] attribute, so this bound applies to every loop unless you pass --unwind. Kani’s unwinding checks stay enabled, so a loop that needs more iterations fails an unwinding assertion instead of being silently cut short.

To change either value, pass the option explicitly. When any automatic harness fails, Kani prints a reminder of these two defaults after the summary table, because the failure may come from a timeout or an insufficient unwinding bound rather than from a bug in the function. In that case, try larger values or, where possible, add a loop contract. The default bounds for bounded arguments are chosen to stay below the unwinding bound, and Kani warns if a configured bound reaches it.

Verification itself runs in parallel by default; see Parallel verification.

Summary table and markers

A run of kani autoharness prints its results in three stages:

1. Before verification, unless --quiet is passed, the tables of selected and skipped functions (see Skip reasons).
2. During verification, the result of each harness as it finishes.
3. After verification, the Autoharness Summary table, followed by a line of the form Complete - N successfully verified functions, M failures, T total. If the crate also contains manual harnesses, they are verified in the same run and reported separately in a Manual Harness Summary.

The summary table has the columns Crate, Selected Function, Kind of Automatic Harness and Verification Result. Rows are sorted by function name, with successes listed before failures. For a generic function, Selected Function shows the verified instantiation, e.g. foo::<i32>. Kind of Automatic Harness is #[kani::proof], or #[kani::proof_for_contract] when the function has a function contract, and may carry one or both of these markers:

• “(bounded)”: some arguments were generated with bounded values under --bounded-arguments. A note after the table lists the bounds the run used (slice length, string length, and the BoundedArbitrary bound) and repeats that the result only holds up to them.
• “(ctor)”: some values were generated through one of a type’s own constructors, or constrained by mined invariants, under --constructor-args. A note after the table repeats that the result only covers values reachable through that constructor. Harnesses filtered only by the mined invariants of a type with its own Arbitrary implementation are currently not marked; see Mined-invariant heuristic.

A Success without either marker still has the limitations described in Soundness caveats.

Soundness caveats

A Success result means that Kani found no failing check for any of the inputs the harness generated. The cases below are where those inputs, or the instantiation being verified, do not cover everything a caller could do, so a Success can still miss a bug. With Kani’s default checks, a harness that times out or needs more loop unwinding than the bound allows is reported as a failure, not a success (see Default settings).

Single monomorphization

For a generic function, autoharness verifies a single instantiation (see Generic Functions): each type parameter is replaced by one concrete type that satisfies its bounds, and each usize const generic parameter by the value 2. A Success for foo::<i32> therefore does not imply that foo::<u8> or foo::<MyType> is also safe. The summary table always shows the instantiated name, so it is visible which instantiation was verified.

Type parameters bounded by Fn, FnMut or FnOnce are the exception: they are instantiated with a model that covers every value a closure with that signature could return, rather than with one particular closure (see Other limitations for what the model does not cover). The function’s other type parameters are still verified for one choice only.

No aliasing between 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. 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.

Bounded arguments

Harnesses marked “(bounded)” use bounded nondeterministic values for some arguments, which --bounded-arguments enables (see Bounded Arguments). Their results only hold for inputs up to those bounds: a bug that needs a longer slice or string, or a larger BoundedArbitrary value, is not found. The bounds a run used are printed in a note after the summary table. Arguments that are generated without bounds by default, such as slices and Vecs of primitive integers or floats, are not affected.

Vacuous constructors

This applies to harnesses marked “(ctor)”, i.e. runs with --constructor-args (see Constructor-based generation). If the chosen constructor is unsatisfiable for the generated type — an assert-guarded constructor every argument of which trips an assertion, or a checked constructor that always returns None/Err — the generated body assumes false on all paths and the harness becomes vacuous, reporting Success without checking anything. Kani does not yet detect this case; see #4757.

Mined-invariant heuristic

This applies to runs with --constructor-args, where mined invariants are assumed for generated values (see Mined invariants). Such harnesses are normally marked “(ctor)”, but not when the filtered type has its own Arbitrary implementation, so a Success without the marker can still be affected; see #4995. The “asserted in ≥2 methods” filter is a heuristic, not a proof of type-invariance. If two methods share a precondition that is not a universal invariant, it is assumed for all generated values and may exclude otherwise-valid inputs — a potential missed bug. This is acceptable only under the opt-in, under-approximating --constructor-args contract; see #4763.

Other limitations

The following under-approximations apply by default, and the summary table does not mark the harnesses they affect:

• Closures have no side effects. The model used for Fn/FnMut/FnOnce-bounded type parameters returns a fresh nondeterministic value on every call but never modifies anything. It therefore does not cover closures that modify state the function can also observe, such as a static or a Cell that the caller also passes as an argument; see #4994.
• Raw pointers are well-behaved. Generated raw pointers are always aligned, never point to deallocated memory, and point to an initialized value whenever they are valid, so bugs that need a misaligned or dangling pointer are not found (see Raw Pointers).
• Formatting uses the default parameters and a sink that never fails. Harnesses for fmt trait implementations only cover the default formatting parameters, not a non-default width, precision, fill, alignment, sign or the alternate flag, and never reach the error path of a failed write (see Formatting Trait Implementations). The &Formatter model used under --bounded-arguments also writes to a sink that never fails.
• Specifications are assumed. Function contract preconditions and the is_safe() predicate of types implementing Invariant are assumed for generated values, so a precondition or invariant that is stronger than necessary excludes inputs that a caller could pass (see Contracts (requires) and Type Safety Invariants).

Architecture (for contributors)

This section is for contributors who want to change how autoharness works. The work is split between the driver (kani-driver), which handles the command line and runs verification, and the compiler (kani-compiler), which selects functions and builds the harnesses while it compiles the crate:

┌──────────────────────────── 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-* compiler flags                  │
│ 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()   │
└─────────────────────────────────────────────────────────────────────┘

1. Options and session setup (kani-driver). args/autoharness_args.rs defines and validates the autoharness options. setup_session in autoharness/mod.rs enables function and loop contracts, applies the parallel verification defaults and the default timeout and unwinding bound, and add_auto_harness_args turns the autoharness options into --autoharness-* flags, which the driver passes to kani-compiler (see call_single_file.rs).
2. Selection (kani-compiler, kani_middle/codegen_units.rs). automatic_harness_partition decides for every function in the crate whether it gets a harness, choosing an instantiation for generic functions and otherwise recording one of the skip reasons. It also records whether a harness will use bounded or constructor-based values; these become the “(bounded)” and “(ctor)” markers. For each selected function, get_all_automatic_harnesses creates an instance of the automatic_harness intrinsic in kani_core (marked AutomaticHarnessIntrinsic), whose body is still a placeholder, and generates its metadata with gen_automatic_proof_metadata.
3. Harness bodies (kani-compiler, kani_middle/transform/automatic.rs). AutomaticHarnessPass replaces each placeholder body with the actual harness: it sets up contract instrumentation if the function has a contract, generates each argument as described in Generating harnesses, assumes the applicable assumptions, calls the function, and adds the checks. AutomaticArbitraryPass synthesizes T::any() for structs and enums that can derive Arbitrary automatically.
4. Code generation. codegen_cprover_gotoc translates the crate, including the harnesses, into a goto program for CBMC, and the selected and skipped functions are stored in the autoharness_md field of the crate’s KaniMetadata.
5. Results (kani-driver). postprocess_project in autoharness/mod.rs prints the selected and skipped tables; with --list, the run stops here. Otherwise harness_runner.rs runs CBMC on each harness and then calls print_autoharness_summary to print the summary table.

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.