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
  • multi_example
  • project_sanity
  • rule_sanity
  • short_output
• Options that control the Solidity compiler
  • compiler_map
  • ignore_solidity_warnings
  • packages
  • packages_path
  • solc
  • solc_allow_path
  • solc_evm_version
  • solc_evm_version_map
  • solc_optimize
  • solc_optimize_map
  • solc_via_ir
  • solc_via_ir_map
  • vyper
• 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 job metadata and dashboard filtering
  • msg
  • protocol_author
  • protocol_name
• Options for controlling contract creation
  • dynamic_bound
  • dynamic_dispatch
  • prototype
• Version options
  • version
  • prover_version
• Conf file options
  • override_base_config
• Advanced options
  • 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