-
Notifications
You must be signed in to change notification settings - Fork 174
OpenAug 27, 2026
No due date
•Last updated Automatic harness generation (kani autoharness). Tracking issue: #3832.
This milestone serves two purposes:
- Active work. The in-flight series of autoharness PRs, worked in the order they were opened.
- Chronological archive. All closed autoharness PRs and issues since the original subcommand (#3874), so the full history of the tool is visible in one place.
Feature surface: kani-compiler/src/kani_middle/transform/automatic.rs, kani-driver/src/autoharness/, kani-driver/src/args/autoharness_args.rs, docs at docs/src/reference/experimental/autoharness.md, and the cargo_autoharness_* / autoharness-* suites under tests/script-based-pre/.
76% complete
List view
0 of 16 selected 0 issues of 16 selected
Tracking Issue: Automatic Harnesses
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.T-TrackingIssueIssues used to track a large amount of work related to a featureIssues used to track a large amount of work related to a featureZ-AutoharnessIssue related to autoharness subcommandIssue related to autoharness subcommandStatus: Open.#3832 In model-checking/kani;Tutorial: proof harness patterns
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.Status: Open.#847 In model-checking/kani;Warn if async harness does not have an unwind bound
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.Status: Open.#1517 In model-checking/kani;Allow disabling unwinding assertions for specific harnesses
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.Status: Open.#1710 In model-checking/kani;UI unclear: reported results need to be clearer about the harness
[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.[E] User ExperienceAn UX enhancement for an existing feature. Including deprecation of an existing one.An UX enhancement for an existing feature. Including deprecation of an existing one.Status: Open.UX Issue : Cargo Kani --harness [harness_list] only returns the results of the last harness
[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.Status: Open.Mechanism to enable users to select a suite of harnesses to run
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.Status: Open.#1865 In model-checking/kani;Support harness partition
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.Status: Open.#3006 In model-checking/kani;Kani always rebuilds when running verify-std
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.T-UserTag user issues / requestsTag user issues / requestsStatus: Open.#4079 In model-checking/kani;Untrustworthy outputs of multi-threaded verifications
[C] BugThis is a bug. Something isn't working.This is a bug. Something isn't working.Status: Open.Arbitrary/autoharness: nondeterministic
Rc<T>/Arc<T>values always havestrong_count == 1[F] SoundnessKani failed to detect an issueKani failed to detect an issueZ-AutoharnessIssue related to autoharness subcommandIssue related to autoharness subcommandStatus: Open.#4752 In model-checking/kani;Autoharness: model caller-controlled aliasing between reference/pointer arguments
Z-AutoharnessIssue related to autoharness subcommandIssue related to autoharness subcommandStatus: Open.#4750 In model-checking/kani;Autoharness: make --bounded-arguments bounds configurable and surface them in the output
Z-AutoharnessIssue related to autoharness subcommandIssue related to autoharness subcommandStatus: Open.#4751 In model-checking/kani;Autoharness --constructor-args: an unsatisfiable constructor yields a vacuous (always-Success) harness
[F] SoundnessKani failed to detect an issueKani failed to detect an issueZ-AutoharnessIssue related to autoharness subcommandIssue related to autoharness subcommandStatus: Open.#4757 In model-checking/kani;Autoharness: generate values for pattern-type fields, restoring layout-niche coverage for user-defined ranged types
[C] Feature / EnhancementA new feature request or enhancement to an existing feature.A new feature request or enhancement to an existing feature.Z-AutoharnessIssue related to autoharness subcommandIssue related to autoharness subcommandStatus: Open.#4758 In model-checking/kani;Autoharness --constructor-args: assumed mined invariants may exclude valid values (heuristic under-approximation)
Z-AutoharnessIssue related to autoharness subcommandIssue related to autoharness subcommandStatus: Open.#4763 In model-checking/kani;