Status:
Experimental
Leads:
@feliperodri
GitHub milestone:
Autoharness

Overview

AutoHarness is Kani’s automatic harness generation feature, exposed through the autoharness subcommand (cargo kani autoharness -Z autoharness). Kani scans a crate for functions whose arguments all implement the kani::Arbitrary trait, generates a proof harness for each, and runs them. The generated harnesses are internal to Kani: it makes no changes to your source code. Where a function has a function contract or loop contracts, Kani verifies those instead.

Motivation

Many proof harnesses follow a predictable format: to verify a function foo, create arbitrary values for each of its arguments and call foo on them. AutoHarness automates writing that boilerplate so that users can start verifying a crate without first writing harnesses by hand.

Goals

The goal of AutoHarness is to fully automate the proof harness workflow proposed in Code-Level Model Checking in the Software Development Workflow. Users should be able to run Kani on their entire crate and immediately see:

  • what can be verified out of the box, and which guarantees that gives them;
  • what needs contracts before it can be verified;
  • what hits Kani’s limitations, and why.

Current Work

The feature is experimental and enabled with -Z autoharness. Active and completed work is tracked in the Autoharness milestone and the tracking issue (#3832). Refer to those for current status rather than this page.

Resources

Get Involved