Kani command cheatsheet

[zjp-CN]

Basic check commands

# check #[proof] annotated harnesses (i.e. standard harness)
kani path/to/single.rs

# check #[proof_for_contract] harnesses (i.e. contract harness)
kani path/to/single.rs -Zfunction-contracts

# check auto generated harnesses on non-proof or non-proof_for_contract functions
# * if the function is without requires and ensures, it's generated as a standard harness
# * if the function is with requires and ensures, it's generated as a contract harness
# * (unsure) if the function is with loop invariant, it's generated as a contract harness (or loop contract?)
kani autoharness -Zautoharness path/to/single.rs

Filtering

--harness
If specified, only run harnesses that match this filter. This option can be provided multiple times, which will run all tests matchi
ng any of the filters. If used with --exact, the harness filter will only match the exact fully qualified name of a harness

# any harness the name of which contains run_this
kani path/to/single.rs --harness run_this

# any harness the name of which contains run_this or and_this
kani path/to/single.rs --harness run_this --harness and_this

# only harness the name of which is exactly run_this
kani path/to/single.rs --harness run_this --exact
# specify a path to it match exactly against a harness under a submodule
kani path/to/single.rs --harness submodule::run_this --exact

# -Zfunction-contracts and `autoharness -Zautoharness` also applies for #[proof] and #[proof_for_contract] harnesses

But to filter autoharnesses, we should use --include-pattern regex or --exclude-pattern instead: doc

kani autoharness -Zautoharness path/to/single.rs --include-pattern this
kani autoharness -Zautoharness path/to/single.rs --include-pattern this --include-pattern or_this
kani autoharness -Zautoharness path/to/single.rs --include-pattern this --include-pattern or_this --exclude-pattern no_this

[zjp-CN]

List harnesses

For normal rs file:

list path/to/single.rs
autoharness -Z autoharness --list path/to/single.rs

For verify-rust-std:

list --std path/to/library
autoharness -Z autoharness --list --std path/to/library

These list commands will print harnesses if any:

• list: standard/contract
• autoharness --list: standard/contract/auto