Certora Prover CLI

Contents

• CLI Options
• Most frequently used options
  • --verify
  • --msg
  • --rule
  • --exclude_rule
  • --split_rules
  • --method
  • --parametric_contracts
  • --wait_for_results
• Options affecting the type of verification run
  • --coverage_info
  • --foundry
  • --independent_satisfy
  • --multi_assert_check
  • --project_sanity
  • --rule_sanity
  • --short_output
• Options that control the Solidity compiler
  • --compiler_map
  • --packages
  • --packages_path
  • --solc
  • --solc_allow_path
  • --solc_evm_version
  • --solc_evm_version_map
  • --solc_optimize
  • --solc_optimize_map
  • --solc_via_ir
• Options regarding source code loops
  • --loop_iter
  • --optimistic_loop
• Options regarding summarization
  • --auto_dispatcher
  • --nondet_difficult_funcs
  • --nondet_minimal_difficulty
  • --optimistic_summary_recursion
  • --summary_recursion_limit
• Options regarding hashing of unbounded data
  • --optimistic_hashing
  • --hashing_length_bound
• Options that help reduce the running time
  • --compilation_steps_only
  • --disable_local_type_checking
  • --global_timeout
  • --method
  • --smt_timeout
• Options to set addresses and link contracts
  • --address
  • --contract_extensions
  • --contract_recursion_limit
  • --link
  • --optimistic_contract_recursion
  • --optimistic_fallback
  • --struct_link
• Options for controlling contract creation
  • --dynamic_bound
  • --dynamic_dispatch
  • --prototype
• Version options
  • --version
• Advanced options
  • --allow_solidity_calls_in_quantifiers
  • --java_args
  • --precise_bitwise_ops
  • --prover_args
  • Control flow splitting options
• Configuration (Conf) Files
  • How CLI options are mapped to JSON
  • Generating a conf file