cmzech@80a9971b5e20 playground % cargo kani -h    
Verify a Rust crate. For more information, see https://github.com/model-checking/kani

Usage: cargo-kani [OPTIONS] [COMMAND]

Commands:
  autoharness  Create and run harnesses automatically for eligible functions. Implies -Z function-contracts and -Z loop-contracts. See https://model-checking.github.io/kani/reference/experimental/autoharness.html for documentation
  list         List contracts and harnesses
  playback     Execute concrete playback testcases of a local package
  help         Print this message or the help of the given subcommand(s)

Options:
  -h, --help     Print help (see more with '--help')
  -V, --version  Print version

Verification Options:
      --cbmc-args [<CBMC_ARGS>...]
          Pass through directly to CBMC; must be the last flag. This feature is unstable and it requires `-Z unstable-options` to be used
      --concrete-playback <CONCRETE_PLAYBACK>
          Generate concrete playback unit test. If value supplied is 'print', Kani prints the unit test to stdout. If value supplied is 'inplace', Kani automatically adds the unit test to your source code. This option does not work with `--output-format old` [possible values: print, inplace]
      --default-unwind <DEFAULT_UNWIND>
          Specify the value used for loop unwinding in CBMC
      --exact
          When specified, the harness filter will only match the exact fully qualified name of a harness
      --fail-fast
          Stop the verification process as soon as one of the harnesses fails
      --force-build
          Force Kani to rebuild all packages before the verification
      --harness <HARNESS_FILTER>
          If specified, only run harnesses that match this filter. This option can be provided multiple times, which will run all tests matching any of the filters. If used with --exact, the harness filter will only match the exact fully qualified name of a harness
      --harness-timeout <HARNESS_TIMEOUT>
          Timeout for each harness with optional suffix ('s': seconds, 'm': minutes, 'h': hours). Default is seconds. This option is experimental and requires `-Z unstable-options` to be used
      --no-assertion-reach-checks
          Turn off assertion reachability checks
      --output-format <OUTPUT_FORMAT>
          Toggle between different styles of output [default: regular] [possible values: regular, terse, old]
      --randomize-layout [<RANDOMIZE_LAYOUT>]
          Randomize the layout of structures. This option can help catching code that relies on a specific layout chosen by the compiler that is not guaranteed to be stable in the future. If a value is given, it will be used as the seed for randomization See the `-Z randomize-layout` and `-Z layout-seed` arguments of the rust compiler
      --solver <SOLVER>
          Specify the CBMC solver to use. Overrides the harness `solver` attribute. If no solver is specified (with --solver or harness attribute), Kani will use CaDiCaL [possible values: cadical, kissat, minisat, bin=<SAT_SOLVER_BINARY>]
      --target-dir <TARGET_DIR>
          Directory for all generated artifacts
      --tests
          Enable test function verification. Only use this option when the entry point is a test function
      --unwind <UNWIND>
          Specify the value used for loop unwinding for the specified harness in CBMC

Memory Checks:
      --default-checks                Turn on all default checks
      --no-default-checks             Turn off all default checks
      --memory-safety-checks          Turn on default memory safety checks
      --no-memory-safety-checks       Turn off default memory safety checks
      --overflow-checks               Turn on default overflow checks
      --no-overflow-checks            Turn off default overflow checks
      --undefined-function-checks     Turn on undefined function checks
      --no-undefined-function-checks  Turn off undefined function checks
      --unwinding-checks              Turn on default unwinding checks
      --no-unwinding-checks           Turn off default unwinding checks

Common Options:
      --debug                        Produce full debug information
  -q, --quiet                        Produces no output, just an exit code and requested artifacts; overrides --verbose
  -v, --verbose                      Output processing stages and commands, along with minor debug information
  -Z, --unstable <UNSTABLE_FEATURE>  [possible values: async-lib, autoharness, concrete-playback, c-ffi, float-lib, function-contracts, gen-c, ghost-state, lean, list, loop-contracts, mem-predicates, restrict-vtable, source-coverage, stubbing, uninit-checks, unstable-options, valid-value-checks]

Cargo Common Options:
      --all-features          Activate all package features
  -e, --exclude <EXCLUDE>...  Exclude the specified packages
  -F, --features <FEATURES>   Comma separated list of package features to activate
      --manifest-path <PATH>  Path to Cargo.toml
      --no-default-features   Do not activate the `default` feature
  -p, --package <PACKAGE>...  Run Kani on the specified packages (see `cargo help pkgid` for the accepted format)
      --workspace             Build all packages in the workspace

Cargo Target Options:
      --bin <BIN>  Check only the specified binary target
      --bins       Check all binaries
      --lib        Check only the package's library unit tests