Kontrol Prove Flags


-h, --help

Show this help message and exit

--verbose, -v

Verbose output.


Debug output.

--workers WORKERS, -j WORKERS

Number of processes to run in parallel.


Directories to lookup K definitions in.

--main-module MAIN_MODULE

Name of the main module.

--syntax-module SYNTAX_MODULE

Name of the syntax module.

--md-selector MD_SELECTOR

Code selector expression to use when reading markdown.

--depth DEPTH

Maximum depth to execute to.

--definition DEFINITION_DIR

Path to definition to use.

--debug-equations DEBUG_EQUATIONS

Comma-separate list of equations to debug.


Check subsumption even on non-terminal nodes (default, experimental).


Do not check subsumption on non-terminal nodes (experimental).


Use fast-check on k-cell to determine subsumption (experimental).

--smt-timeout SMT_TIMEOUT

Timeout in ms to use for SMT queries.

--smt-retry-limit SMT_RETRY_LIMIT

Number of times to retry SMT queries with scaling timeouts.

--smt-tactic SMT_TACTIC

Z3 tactic to use when checking satisfiability. Example: (check-sat-using smt)


Log traces of all simplification and rewrite rule applications.

--kore-rpc-command KORE_RPC_COMMAND

Custom command to start RPC server.


Use the booster RPC server instead of kore-rpc (default).


Do not use the booster RPC server instead of kore-rpc.

--port PORT

Use existing RPC server on named port.

--maude-port MAUDE_PORT

Use existing Maude RPC server on named port.

--bug-report BUG_REPORT

Generate bug report with given name


Store a node for every EVM opcode step (expensive).


Store a node for every EVM jump opcode.


Store a node for every EVM call made.


Do not store a node for every EVM call made (default).


Store a node for every EVM SSTORE/SLOAD made.


Store a node for every EVM basic block (implies --break-on-calls).

--max-depth MAX_DEPTH

Maximum number of K steps before the state is saved in a new node in the CFG. Branching will cause this to happen earlier.

--max-iterations MAX_ITERATIONS

Number of times to expand the next pending node in the CFG.


Show failure summary for all failing tests (default).


Do not show failure summary for failing tests.


Automatically extract gas cell when infinite gas is enabled.


Show models for failing nodes (default).


Stop execution on other branches if a failing node is detected (default).


Continue execution on other branches if a failing node is detected.

--foundry-project-root FOUNDRY_ROOT

Path to Foundry project root directory.

--match-test TESTS

Specify contract function(s) to test using a regular expression. This will match functions based on their full signature, e.g., 'ERC20Test.testTransfer(address,uint256)'. This option can be used multiple times to add more functions to test.


Reinitialize CFGs even if they already exist.

--bmc-depth BMC_DEPTH

Enables bounded model checking. Specifies the maximum depth to unroll all loops to.


Include the contract constructor in the test execution.


Enables gas computation in KEVM.


Break on all Foundry rules.

--init-node-from DEPLOYMENT_STATE_PATH

Path to JSON file containing the deployment state of the deployment process used for the project.

--include-summary INCLUDE_SUMMARIES

Specify a summary to include as a lemma.


Flag used by Simbolik to initialise the state of a non test function as if it was a test function.


Generate a JUnit XML report


Use Compositional Symbolic Execution


Use hevm success predicate instead of foundry to determine if a test is passing.

Last updated