### Install Rust using rustup (Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_solana_installation.html.md

Installs the Rust programming language and its toolchain manager, rustup, by downloading and executing the official installation script.

```Shell
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh
```

--------------------------------

### Test Certora Platform Tools Installation (Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_solana_installation.html.md

Tests the installation of the Certora Platform Tools by running the `cargo certora-sbf` command with the `--no-build` flag, which downloads and installs the tools without building a project.

```Shell
cargo certora-sbf --no-build
```

--------------------------------

### Install Rust using curl (Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_sunbeam_installation.html.md

Installs the Rust programming language and its toolchain using the official `rustup` script downloaded via curl.

```Shell
curl --proto '=https' --tlsv1.2 -sSf https://sh.rustup.rs | sh
```

--------------------------------

### Install Rust Toolchain 1.79 (Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_solana_installation.html.md

Installs the specific Rust toolchain version 1.79 using the rustup toolchain command.

```Shell
rustup toolchain install 1.79
```

--------------------------------

### Example Gambit Configuration File (JSON)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_gambit_gambit.html.md

Provides an example of the structure and content of a JSON configuration file used with Gambit's `--json` option. It includes common fields like `filename`, `sourceroot`, and `solc_remappings`. Paths within this file are resolved relative to the directory containing the JSON file.

```JSON
{
"filename":"../10Power/TenPower.sol",
"sourceroot":"..",
"solc_remappings":[
"@openzeppelin=node_modules/@openzeppelin"
]
}
```

--------------------------------

### Install Rust Toolchain 1.75 (Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_solana_installation.html.md

Installs the specific Rust toolchain version 1.75 using the rustup toolchain command.

```Shell
rustup toolchain install 1.75
```

--------------------------------

### Install just via Cargo (Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_sunbeam_installation.html.md

Installs the `just` command runner tool using the Rust package manager, Cargo.

```Shell
cargo install just
```

--------------------------------

### Install Certora CLI (Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_sunbeam_installation.html.md

Command using pip3 to install the Certora CLI beta package. This is the main step for installing the Certora Prover tool.

```Shell
pip3 install certora-cli-beta
```

--------------------------------

### Install Rust Toolchain 1.81 (Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_solana_installation.html.md

Installs the specific Rust toolchain version 1.81 using the rustup toolchain command.

```Shell
rustup toolchain install 1.81
```

--------------------------------

### Install Certora Prover Beta Package (Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_user-guide_install.html.md

Install the pre-release beta version of the Certora Prover command-line interface package using pip. This is an optional installation.

```shell
pipinstallcertora-cli-beta
```

--------------------------------

### Example Certora Equivalence Check Command (CLI)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_equiv-check_index.html.md

This is a concrete example of the `certoraEqCheck` command using specific file paths and function names (`BasicMathGood:add` and `BasicMathBad:add_mult`) from the documentation's example, referencing the `testGood.conf` configuration file.

```Shell
certoraEqCheckconfTest/EqCheck/testGood.confBasicMathGood:addBasicMathBad:add_mult
```

--------------------------------

### Example: Mutate Single File (CLI)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_gambit_gambit.html.md

Provides a concrete example of using the `gambit mutate` command with the `-f` (filename) option to mutate a specific Solidity file located at `benchmarks/BinaryOpMutation/BinaryOpMutation.sol`. The target file must reside within the current working directory or a subdirectory.

```Command-line
gambitmutate-fbenchmarks/BinaryOpMutation/BinaryOpMutation.sol
```

--------------------------------

### Example using --packages option with Certora Prover CLI

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html.md

Provides a concrete example of using the `--packages` option to specify the locations of `ds-stop` and `ds-note` Solidity packages relative to the current working directory (`$PWD`).

```shell
certoraRunBank.sol--verifyBank:Bank.spec--packagesds-stop=$PWD/lib/ds-token/lib/ds-stop/srcds-note=$PWD/lib/ds-token/lib/ds-stop/lib/ds-note/src
```

--------------------------------

### Displaying CertoraRun Help

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_projects_tutorials_en_latest_lesson2_started_erc20_example.html.md

Shows the help documentation for the `certoraRun` command-line tool. This provides information on available options and syntax.

```Shell
certoraRun --help
```

--------------------------------

### Getting Help for CertoraRun Utility - Shell

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_user-guide_running.html.md

This command displays a concise summary of the available command-line options and usage instructions for the `certoraRun` utility.

```Shell
certoraRun--help
```

--------------------------------

### Add wabt bin to PATH (Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_sunbeam_installation.html.md

Adds the directory containing the `wabt` toolkit executables (like `wasm2wat`) to the system's PATH environment variable, making them available as commands.

```Shell
export PATH=~/path/to/wabt/bin:$PATH
```

--------------------------------

### Install cargo-certora-sbf (Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_solana_installation.html.md

Installs the `cargo-certora-sbf` subcommand, which is required for using the Certora Prover with Solana programs. It specifies using Rust toolchain 1.81 or above.

```Shell
cargo +1.81 install cargo-certora-sbf
```

--------------------------------

### Install solc-select (pip) - Shell

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_user-guide_install_evm_compiler.html.md

Installs the `solc-select` tool, a utility for managing multiple Solidity compiler versions, using the Python package installer `pip`. This is a prerequisite for using the `solc-select` method to install `solc`.

```Shell
pipinstallsolc-select
```

--------------------------------

### Certora CLI Example with dynamic_bound and dynamic_dispatch

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html?highlight=--solc.md

This example shows how to use both `--dynamic_bound 1` and `--dynamic_dispatch` with `certoraRun`. This models the creation of `Foo.sol` by `C.sol` and attempts to automatically dispatch method calls made by the newly created `Foo` instance.

```CLI
certoraRunC.solFoo.sol--verifyC:C.spec--dynamic_bound1--dynamic_dispatch
```

--------------------------------

### Examples using --solc option with Certora Prover CLI

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html.md

Provides two examples for the `--solc` option: one using a compiler name found in the system's `$PATH` (`solc8.19`) and another using a full path to the executable (`/usr/local/bin/solc8.19`).

```shell
# Use a compiler version from $PATH
certoraRunBank.sol--verifyBank:Bank.spec--solcsolc8.19
# Use full path to the compiler
certoraRunBank.sol--verifyBank:Bank.spec--solc/usr/local/bin/solc8.19
```

--------------------------------

### Example Sunbeam Configuration File (with Build Script)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_sunbeam_usage.html.md

This JSON snippet illustrates a typical configuration file (.conf) used to run Sunbeam. It specifies a build script (`build_script`), the verification process (`process`), and a list of rules (`rule`) to be verified. The build script is responsible for compiling the project.

```JSON
{
  "build_script": "../certora_build.py",
  "process": "emv",
  "rule": [
    "init_balance",
    "transfer_is_correct",
    "transfer_no_effect_on_other",
    "transfer_fails_if_low_balance"
  ]
}
```

--------------------------------

### Certora CLI: Set Solc Optimize Runs (Example)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html.md

This example demonstrates using --solc_optimize to set the Solidity compiler's optimizer to run 300 times during a Certora run for Bank.sol.

```shell
certoraRunBank.sol--verifyBank:Bank.spec--solc_optimize300
```

--------------------------------

### Installing Rosetta on macOS

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_projects_tutorials_en_latest_lesson2_started_erc20_example.html.md

Executes the macOS `softwareupdate` command to install Rosetta. This is a troubleshooting step for resolving "Bad CPU type in executable" errors on certain macOS systems.

```Shell
softwareupdate --install-rosetta
```

--------------------------------

### Certora Prover CLI: Specify Vyper Compiler Examples

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html?highlight=--solc.md

Provides examples of using the `--vyper` option within a `certoraRun` command. It demonstrates how to specify the Vyper compiler by its name (which is searched in the system's $PATH) and by providing a full path to the executable.

```Shell
# Use a compiler version from $PATH
certoraRunBank.sol--verifyBank:Bank.spec--vypervyper0.3.10
# Use full path to the compiler
certoraRunBank.sol--verifyBank:Bank.spec--vyper/usr/local/bin/vyper0.3.10
```

--------------------------------

### Example: Running Certora Prover with Specific Depth

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html?highlight=--solc.md

This is an example command demonstrating how to run the Certora Prover with the '--prover_args'-depth 5'' option. It applies the verification process to the 'Bank.sol' contract using the 'bank.spec' specification file.

```Certora CLI
certoraRunBank.sol--verifyBank:bank.spec--prover_args'-depth 5'
```

--------------------------------

### Install Beta in Virtual Environment (Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_user-guide_install.html.md

Install the certora-cli-beta package using pip3 within the currently active certora-beta virtual environment. This isolates the beta installation.

```shell
pip3installcertora-cli-beta
```

--------------------------------

### Create Virtual Environment (Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_user-guide_install.html.md

Create a new Python virtual environment named certora-beta using the virtualenv tool. This environment will be used to install the beta version of the Certora Prover.

```shell
virtualenvcertora-beta
```

--------------------------------

### Install Specific Solidity Version (solc-select) - Shell

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_user-guide_install_evm_compiler.html.md

Downloads and installs a specific version of the Solidity compiler (`solc`) using the `solc-select` tool. Replace `0.8.0` with the desired version number.

```Shell
solc-selectinstall0.8.0
```

--------------------------------

### Certora CLI Example with dynamic_bound=1

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html?highlight=--solc.md

This example demonstrates using the `certoraRun` command with `--dynamic_bound 1` to verify a contract `C.sol` that creates an instance of `Foo.sol`, modeling the creation and inlining the constructor of `Foo` once.

```CLI
certoraRunC.solFoo.sol--verifyC:C.spec--dynamic_bound1
```

--------------------------------

### Build Gambit from Source (Cargo)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_gambit_gambit.html.md

Builds the Gambit executable from the source code located in the current directory using the `cargo install` command. This compiles the project and installs the resulting binary into a directory typically included in the system's PATH, making the `gambit` command globally available. Requires the Rust toolchain (rustc and cargo) to be installed on the system.

```Command-line
cargo install --path .
```

--------------------------------

### Foundry Test Setup with Contract Creation (Solidity)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_cvl_foundry-integration.html.md

Illustrates a common Foundry test pattern where the `setUp` function creates an instance of another contract (`MyContract`). This pattern requires special handling (linking) in the Certora Prover configuration to resolve cross-contract calls.

```Solidity
contract TestContract is Test {
    MyContract myContract;

    function setUp() external {
        myContract = new MyContract();
    }

    ...
}
```

--------------------------------

### Install solc executable

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_user-guide_ci.html.md

Moves the solc executable to a standard location in the system's PATH using sudo.

```Shell
sudo mv solc-static-linux /usr/local/bin/solc8.23
```

--------------------------------

### Install Certora Prover Package (Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_user-guide_install.html.md

Use pip3 to install the main Certora Prover command-line interface package. It is recommended to use a Python virtual environment.

```shell
pip3installcertora-cli
```

--------------------------------

### Example Output: GitHub API Language Breakdown

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_user-guide_github_highlighting.html.md

This is an example of the JSON response from the GitHub API's `/languages` endpoint for a repository. It shows the byte count breakdown by language, confirming that GitHub's Linguist has processed the `.gitattributes` changes and recognized Solidity and JSON5.

```JSON
{
 "Solidity": 21038,
 "JSON5": 443
 ...
}
```

--------------------------------

### Certora CLI: Set Solc Optimize Map (Example)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html.md

This example demonstrates using --solc_optimize_map to set 200 optimization runs for 'Bank' and 300 runs for 'Exchange' during a Certora run.

```shell
certoraRunBank.sol--verifyBank:Bank.spec--solc_optimize_mapBank=200,Exchange=300
```

--------------------------------

### Running Gambit with Default Source Root (Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_gambit_gambit.html.md

Executes Gambit's `mutate` command on a specific Solidity file (`benchmarks/BinaryOpMutation/BinaryOpMutation.sol`) requesting 1 mutant (`-n1`). The commands then display the generated mutants log and find the generated mutant file. This example uses the default source root, which is the current working directory.

```Shell
gambitmutate-fbenchmarks/BinaryOpMutation/BinaryOpMutation.sol-n1
catgambit_out/mutants.log
findgambit_out/mutants-name"*.sol"
```

--------------------------------

### Running Certora Solana Prover with Build Script

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_solana_options.html.md

Example command demonstrating how to run the Certora Solana Prover using the --build_script option, specifying the path to the build script and the rule to verify.

```Command Line
certoraSolanaProver--build_script<path_to_build_script>--rule<rule_name>
```

--------------------------------

### Example Certora Run with Depth Option

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html.md

An example command demonstrating how to run the Certora Prover on `Bank.sol` with the `bank.spec` specification, setting the control flow splitting depth to 5 using the `--prover_args'-depth 5'` option.

```cli
certoraRunBank.sol--verifyBank:bank.spec--prover_args'-depth 5'
```

--------------------------------

### Example Certora Prover Configuration File (JSON5)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_projects_tutorials_en_latest_lesson2_started_config_files.html.md

This JSON5 configuration file specifies parameters for running the Certora Prover. It includes the source files to analyze, the contract and specification to verify, options for waiting for results and rule sanity checks, and a custom message for the run.

```JSON5
{
"files":[
"ERC20.sol"
],
"verify":"ERC20:ERC20.spec",
"wait_for_results":"all",
"rule_sanity":"basic",
// Note: json5 supports comments!
"msg":"First run using .conf file"
}
```

--------------------------------

### Example Python Build Script Configuration for Sunbeam

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_sunbeam_usage.html.md

This Python code snippet shows key variables typically defined in a `certora_build.py` script used by Sunbeam. It configures the command to compile the project (`COMMAND`), the project directory (`PROJECT_DIR`), source files to include in the report (`SOURCES`), and the path to the compiled executable (`EXECUTABLES`).

```Python
# Command to run for compiling the rust project.
COMMAND = "just build"
# JSON FIELDS
PROJECT_DIR = (SCRIPT_DIR).resolve()
SOURCES = ["src/path/to/rust/files/*.rs", "Cargo.toml"]
EXECUTABLES = "target/wasm32-unknown-unknown/release/wasm_file_name.wasm"
```

--------------------------------

### Running Certora Equivalence Checker in Default Mode (Example Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_equiv-check_index.html.md

Demonstrates a specific example of using the certoraEqCheck command in default mode to compare the add function in BasicMathGood.sol with the add_pass function in BasicMathBad.sol, specifying the Solidity compiler version.

```Shell
certoraEqCheckdefTest/EqCheck/BasicMathGood.sol:add:solc8.0Test/EqCheck/BasicMathBad.sol:add_pass:solc8.0
```

--------------------------------

### Install Certora CLI using pip

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_gambit_mutation-verifier.html.md

Installs the Certora CLI tool using the pip package manager. This is the initial step required to use the mutation verifier and other Certora tools.

```Shell
pipinstallcertora-cli
```

--------------------------------

### Certora CLI: Example using contract_recursion_limit

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html.md

Demonstrates how to use the `--contract_recursion_limit` option with the `certoraRun` command. This example sets the limit to 3 for verifying `Bank.sol` with `Bank.spec`.

```Certora CLI
certoraRunBank.sol--verifyBank:Bank.spec--contract_recursion_limit3
```

--------------------------------

### Running Certora Prover with multi_example flag (Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html.md

This command runs the Certora Prover on MyContract.sol with the specification MyContract.spec, enabling the multi_example flag. This flag instructs the Prover to generate multiple counterexamples for failed assertions or multiple witnesses for verified satisfy statements, providing a broader view of the rule's behavior.

```Shell
certoraRunMyContract.sol--verifyMyContract:MyContract.spec--multi_example
```

--------------------------------

### Running Gambit and Listing Output (Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_gambit_gambit.html.md

Provides shell commands to execute Gambit mutation with a limit on the number of mutants and then display the resulting output directory structure using the `tree` command.

```Shell
gambit mutate -f benchmarks/BinaryOpMutation/BinaryOpMutation.sol -n 5
tree gambit_out -L 2
```

--------------------------------

### Certora CLI: Set EVM Version Map (Example)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html.md

This example demonstrates using --solc_evm_version_map to compile 'Bank' with the 'prague' EVM version and 'Exchange' with the 'cancun' EVM version during a Certora run.

```shell
certoraRunBank.sol--verifyBank:Bank.spec--solc_evm_version_mapBank=prague,Exchange=cancun
```

--------------------------------

### Example using --solc_allow_path option with Certora Prover CLI

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html.md

Demonstrates using the `--solc_allow_path` option to allow the Solidity compiler to load sources from the `~/Projects/Bank` directory during the Certora Prover run.

```shell
certoraRunBank.sol--verifyBank:Bank.spec--solc_allow_path~/Projects/Bank
```

--------------------------------

### Example Standard Job Output URL

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_portal_secrets.html.md

This is an example of a standard URL used to access the output files of a Certora Prover job via the web portal.

```Text
https://vaas-stg.certora.com/output/65540/270dce9623d492937d82/?anonymousKey=6edb93d7abae7871f1c3be3b10863d64d2d72fef
```

--------------------------------

### Defining Example Solidity Contract

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_cvl_v5-changes.html.md

Defines a simple Solidity contract `example` containing a state variable `i` and a public view function `getI` that returns the value of `i`. This contract is used as a base for demonstrating CVL rule changes.

```Solidity
contractexample{
uinti;
functiongetI()publicviewreturns(uint256){
returni;
}
}
```

--------------------------------

### Install rustfilt via Cargo (Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_sunbeam_installation.html.md

Installs the `rustfilt` tool using the Rust package manager, Cargo. `rustfilt` is used for demangling Rust symbols.

```Shell
cargo install rustfilt
```

--------------------------------

### Running Certora Solana Prover on Precompiled Binary

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_solana_options.html.md

Example command showing how to run the Certora Solana Prover directly on a precompiled Rust binary file, specifying the path to the binary and the rule to verify.

```Command Line
certoraSolanaProver<path_to_binary_file>--rule<rule_name>
```

--------------------------------

### Certora CLI: Enable Solc Via IR (Example)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html.md

This example demonstrates using the --solc_via_ir flag to enable the Solidity compiler's IR-based code generator globally for all contracts during a Certora run.

```shell
certoraRunBank.sol--verifyBank:Bank.spec--solc_via_ir
```

--------------------------------

### Set Active Solidity Version (solc-select) - Shell

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_user-guide_install_evm_compiler.html.md

Configures `solc-select` to use a specific installed Solidity compiler version as the default `solc` command. Replace `0.8.0` with the version you want to activate.

```Shell
solc-selectuse0.8.0
```

--------------------------------

### Certora CLI: Example with link Option

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html?highlight=--solc.md

Provides an example of using the `--link` option (related to `--struct_link`) in a `certoraRun` command. It links the `underlyingToken` slot in the `Bank` contract to the `BankToken` contract when verifying `Bank.sol` and `BankToken.sol`.

```CLI
certoraRunBank.solBankToken.sol--verifyBank:Bank.spec--linkBank:underlyingToken=BankToken
```

--------------------------------

### Check Java Version (Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_sunbeam_installation.html.md

Command to check the installed version of Java. This is a prerequisite step to ensure Java version 11 or later is available.

```Shell
java -version
```

--------------------------------

### Check Python Version (Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_sunbeam_installation.html.md

Command to check the installed version of Python 3. This is a prerequisite step to ensure Python 3.8.16 or newer is available.

```Shell
python3 --version
```

--------------------------------

### Example Output: Successful Git Attributes Check

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_user-guide_github_highlighting.html.md

This is an example of the expected output when the `git check-attr` command successfully identifies the configured `linguist-language` for `.spec` and `.conf` files, indicating the `.gitattributes` file is working locally.

```Output
path/to/file.spec: linguist-language: Solidity
path/to/file.conf: linguist-language: JSON5
```

--------------------------------

### Require Condition Mutation Example (Solidity)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_gambit_gambit.html.md

Shows how the condition of a `require` statement can be mutated, for example, to always evaluate to true. This tests if the code correctly relies on the original condition for its logic.

```Solidity
require(some_condition()) -> require(true)
```

--------------------------------

### Function Call Arguments Mutation Example (Solidity)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_gambit_gambit.html.md

Shows how the arguments passed to a function call can be mutated, for example, duplicating an argument. This mutation tests the function's behavior with altered inputs.

```Solidity
add(a, b) -> add(a, a)
```

--------------------------------

### Content for macOS PATH File - Path String

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_user-guide_install_evm_compiler.html.md

The content to be placed inside the file created in `/etc/paths.d`. This line should be the absolute path to the directory containing the downloaded `solc` executable. Multiple paths can be added, separated by colons.

```Shell
/full/path/to/solc/executable/folder
```

--------------------------------

### If Condition Mutation Example (Solidity)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_gambit_gambit.html.md

Shows how the conditional expression of an `if` statement can be mutated, for example, to always evaluate to true. This mutation checks if the code correctly handles different outcomes based on the original condition.

```Solidity
if (C) {...} -> if (true) {...}
```

--------------------------------

### Running Certora Prover (Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_projects_tutorials_en_latest_lesson1_prerequisites_formal_verification.html.md

This command executes the Certora Prover tool. It specifies the contract file `Empty.sol`, the specification file `sisters.spec` with the rule `sistersBirthMonths` to verify, and the Solidity compiler version `solc8.0`. This command initiates the formal verification process for the specified rule.

```shell
certoraRunEmpty.sol--verifyEmpty:sisters.spec--solcsolc8.0--rulesistersBirthMonths
```

--------------------------------

### Verify .profile Content (Linux)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_user-guide_install.html.md

Re-opens the .profile file using the nano text editor to verify its content after saving.

```Shell
nano.profile
```

--------------------------------

### Execute Certora Prover with Foundry Integration (Automatic Setup)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_cvl_foundry-integration.html.md

This command executes the Certora Prover in Foundry integration mode using the automatic setup. It requires Certora Prover version 7.25.1 or later and a Foundry project with test files (`.t.sol`) in the current directory. The `--foundry` flag automatically discovers and analyzes these test files.

```Shell
certoraRun --foundry
```

--------------------------------

### Add WASM Target to Rust (Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_sunbeam_installation.html.md

Adds the `wasm32-unknown-unknown` compilation target to the Rust toolchain, which is required for building WebAssembly modules.

```Shell
rustup target add wasm32-unknown-unknown
```

--------------------------------

### Running Certora Prover CLI for ERC20

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_projects_tutorials_en_latest_lesson2_started_erc20_example.html.md

Executes the Certora Prover on the ERC20 contract using the specified specification file and Solidity compiler version 0.8.0. This command initiates the verification process.

```Shell
certoraRun ERC20.sol --verify ERC20:ERC20.spec --solc solc8.0
```

--------------------------------

### Certora CLI: Example using optimistic_contract_recursion and contract_recursion_limit

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html.md

Demonstrates how to use both `--optimistic_contract_recursion` and `--contract_recursion_limit` options together in a `certoraRun` command. This example enables optimistic recursion handling with a limit of 1 for verifying `Bank.sol` with `Bank.spec`.

```Certora CLI
certoraRunBank.sol--verifyBank:Bank.spec--optimistic_contract_recursiontrue--contract_recursion_limit1
```

--------------------------------

### List Files Including Hidden (macOS)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_user-guide_install.html.md

Lists all files and directories in the current directory, including hidden ones (those starting with a dot), using the ls -a command.

```Shell
ls-a
```

--------------------------------

### Providing Inlining Files to Certora Solana Prover

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_solana_options.html.md

Example command showing how to use the --solana_inlining option to provide paths to inlining files when running the Certora Solana Prover, typically in conjunction with a build script and the --rule option.

```Command Line
certoraSolanaProver--build_script<path_to_build_script>--solana_inlining<path_to_inlining_file>--rule<rule_name>
```

--------------------------------

### Example: Setting Contract Address with Certora CLI

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html.md

Provides a concrete example of how to use the --address option in a certoraRun command. It shows setting the address of the Oracle contract to 12 while verifying Bank.sol and Oracle.sol with Bank.spec.

```CLI
certoraRunBank.solOracle.sol--verifyBank:Bank.spec--addressOracle:12
```

--------------------------------

### Certora Prover CLI: smt_timeout Example

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html?highlight=--solc.md

Provides an example of using the `--smt_timeout` option with the `certoraRun` command, setting the timeout to 300 seconds for verifying `Bank.sol` with `Bank.spec`. This limits the time spent by SMT solvers on each rule.

```CLI
certoraRunBank.sol--verifyBank:Bank.spec--smt_timeout300
```

--------------------------------

### Swap Operator Arguments Mutation Example (Solidity)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_gambit_gambit.html.md

Demonstrates swapping the operands of a non-commutative binary operator like subtraction. This mutation tests if the order of operands is critical for correctness.

```Solidity
a - b -> b - a
```

--------------------------------

### Example using --packages_path option with Certora Prover CLI

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html.md

Demonstrates using the `--packages_path` option to point the Certora Prover to a directory named `Solidity/packages` for resolving Solidity packages.

```shell
certoraRunBank.sol--verifyBank:Bank.spec--packages_pathSolidity/packages
```

--------------------------------

### Running Certora Prover with Fixed Spec

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_projects_tutorials_en_latest_lesson2_started_erc20_example.html.md

Executes the Certora Prover on the ERC20.sol contract, verifying it against the ERC20Fixed.spec specification file using Solidity compiler version 8.0.

```Command Line
certoraRun ERC20.sol --verify ERC20:ERC20Fixed.spec --solc solc8.0
```

--------------------------------

### Unary Operator Mutation Example (Solidity)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_gambit_gambit.html.md

Illustrates replacing a unary operator like bitwise NOT (~) with another like negation (-). This mutation checks if the code is robust against changes in unary operations.

```Solidity
~a -> -a
```

--------------------------------

### Running Gambit Mutation via CLI (Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_gambit_gambit.html.md

Demonstrates the basic command-line syntax for running Gambit's `mutate` command on a specific Solidity file.

```Shell
gambit mutate -f benchmarks/BinaryOpMutation/BinaryOpMutation.sol
```

--------------------------------

### Example Certora Specification File (CVL)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html?highlight=--solc.md

An example Certora Verification Language (CVL) specification file (`Bank.spec`) demonstrating the syntax for defining invariants and rules that can be targeted by the `--rule` or `--exclude_rule` CLI options.

```CVL
invariantaddress_zero_cannot_become_an_account()
rulewithdraw_succeeds()
rulewithdraw_fails()
```

--------------------------------

### Eliminate Delegatecall Mutation Example (Solidity)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_gambit_gambit.html.md

Illustrates changing a `delegatecall` to a standard `call` on an address. This mutation is relevant in smart contracts and tests the code's reliance on the specific context-preserving nature of `delegatecall`.

```Solidity
_c.delegatecall(...) -> _c.call(...)
```

--------------------------------

### Run Certora Prover with multi_example option (CLI)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html?highlight=--solc.md

Enables the Certora Prover to generate multiple counterexamples for failed assertions or multiple witnesses for verified satisfy statements. This provides a broader view of rule behavior across different scenarios, useful for debugging complex rules and identifying edge cases.

```shell
certoraRunMyContract.sol--verifyMyContract:MyContract.spec--multi_example
```

--------------------------------

### Open .profile File (Linux)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_user-guide_install.html.md

Opens the .profile file in the home directory using the nano text editor. This file is used to store environment variables for bash shell.

```Shell
nano.profile
```

--------------------------------

### Delete Expression Mutation Example (Solidity)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_gambit_gambit.html.md

Illustrates replacing an expression or function call with a no-operation statement like `assert(true)`. This tests if the removal of the original expression affects the program's behavior.

```Solidity
foo(); -> assert(true);
```

--------------------------------

### Open Linux .profile File (nano) - Shell

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_user-guide_install_evm_compiler.html.md

Opens the `.profile` file in the user's home directory using the `nano` text editor. This file is a script executed upon login for configuring the user's environment, including the PATH.

```Shell
nano.profile
```

--------------------------------

### Binary Operator Mutation Example (Solidity)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_gambit_gambit.html.md

Demonstrates replacing a binary operator like addition (+) with another like subtraction (-). This mutation tests the code's sensitivity to changes in arithmetic or logical operations.

```Solidity
a+b -> a-b
```

--------------------------------

### Example Certora Prover Output (Log)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_user-guide_running.html.md

Shows a typical output message from the Certora Prover indicating that a verification job has been submitted to the server and providing links to track the job status and view results online.

```Log
...
Job submitted to server
Follow your job at https://prover.certora.com
Once the job is completed, the results will be available at https://prover.certora.com/...

```

--------------------------------

### Certora Prover CLI: address Example

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html?highlight=--solc.md

Provides an example of using the `--address` option with the `certoraRun` command, setting the address of the `Oracle` contract to 12 when verifying `Bank.sol` and `Oracle.sol` with `Bank.spec`. This is useful for external contracts with constant addresses.

```CLI
certoraRunBank.solOracle.sol--verifyBank:Bank.spec--addressOracle:12
```

--------------------------------

### Pinning certora-cli to CVL 1 Version

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_cvl_cvl2_migration.html.md

Installs or updates the `certora-cli` package, specifically pinning it to a version less than 4.0.0 (e.g., 3.6.5) to continue using CVL 1 after the release of CVL 2.

```Shell
pip install 'certora-cli<4.0.0'
```

--------------------------------

### Assignment Right-Hand Side Mutation Example (Solidity)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_gambit_gambit.html.md

Demonstrates replacing the right-hand side of an assignment, changing the assigned value or expression. This mutation assesses the code's dependency on the specific value or result assigned.

```Solidity
x = foo(); -> x = -1;
```

--------------------------------

### Specify Summaries with Certora Solana Prover (Command Line)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_solana_options.html.md

Provides the Certora Prover with a list of paths to summary files for Solana contracts. These files are parsed and used to prove properties. This option is currently required for every project and can be passed as a flag or retrieved from a build script.

```Command Line
certoraSolanaProver--build_script<path_to_build_script>--solana_summaries<path_to_summaries_file>--rule<rule_name>
```

--------------------------------

### Certora Prover Configuration: contract_extensions Example

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html?highlight=--solc.md

Shows an example configuration snippet for the `contract_extensions` option in a `.conf` file. It demonstrates how to specify that contract `B` is an extension of contract `A`, excluding the `n` variable from being transferred. This helps the Prover analyze proxy patterns correctly.

```JSON
"contract_extensions":{
"A":[
{
"extension":"B",
"exclude":["n"]
}
]
}
```

--------------------------------

### Set Certora Key Environment Variable (Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_sunbeam_installation.html.md

Command to set a temporary environment variable CERTORAKEY with the personal access key received from Certora. This key is required for authentication with the Certora Prover.

```Shell
export CERTORAKEY=<personal_access_key>
```

--------------------------------

### Setting Solidity Compiler Version with solc-select

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_projects_tutorials_en_latest_lesson2_started_erc20_example.html.md

Uses the `solc-select` tool to set the active Solidity compiler version to 0.8.0. This is an alternative to specifying the compiler with the `--solc` flag in `certoraRun`.

```Shell
solc-select use 0.8.0
```

--------------------------------

### Swap Function Arguments Mutation Example (Solidity)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_gambit_gambit.html.md

Demonstrates swapping the order of arguments passed to a function call. This mutation is relevant for functions where argument order matters and tests the code's handling of swapped inputs.

```Solidity
add(a, b) -> add(b, a)
```

--------------------------------

### Navigate to Home Directory (Linux Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_user-guide_install.html.md

Change the current directory to the user's home directory (~) before editing configuration files like .profile on Linux for troubleshooting PATH issues.

```shell
cd~
```

--------------------------------

### Example: Mutate and Downsample (CLI)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_gambit_gambit.html.md

Illustrates how to use the `gambit mutate` command with both the `-f` (filename) and `-n` (num_mutants) options. This command mutates the specified Solidity file and then randomly selects only 3 mutants from the generated set.

```Command-line
gambitmutate-fbenchmarks/BinaryOpMutation/BinaryOpMutation.sol-n3
```

--------------------------------

### Create/Edit macOS PATH File (sudo nano) - Shell

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_user-guide_install_evm_compiler.html.md

Uses the `sudo` command and the `nano` text editor to create or edit a file named `SolidityCertoraProver` within the `/etc/paths.d` directory. This file will contain the path to the solc executables, making them accessible system-wide. Requires root privileges.

```Shell
sudonanoSolidityCertoraProver
```

--------------------------------

### Running Certora Prover with multiple contracts (Command Line)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_user-guide_multicontract_index.html.md

This command demonstrates how to run the Certora Prover with multiple Solidity source files (`Pool.sol` and `Asset.sol`) provided as command-line arguments. Adding `Asset.sol` makes the Prover aware of its code, adding it to the verification scene. The `--verify` option specifies the contract and specification file to use for the main verification target.

```Command Line
$certoraRuncontracts/Pool.solcontracts/Asset.sol--verifyPool:certora/specs/pool_havoc.spec...
```

--------------------------------

### Mutually Dependent Invariant Requirements

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_cvl_invariants.html.md

This example demonstrates two invariants, `i` and `j`, where each requires the other within their respective `preserved` blocks. This setup allows for a combined inductive proof showing that both `i(x)` and `j(x)` hold in all reachable states.

```CVL
invarianti(uintx)...{preserved{requireInvariantj(x);}}
invariantj(uintx)...{preserved{requireInvarianti(x);}}
```

--------------------------------

### Example Solidity Contract for Invariant Reversion Demo

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_cvl_invariants.html.md

A simple Solidity contract wrapping a dynamic array. It includes `add` to push elements and `get` to retrieve elements by index, used to illustrate how out-of-bounds access can cause invariant checks to revert prematurely.

```Solidity
contractExample{
privateuint[]a;
publicfunctionadd(uinti)external{
a.push(i);
}
publicfunctionget(uinti)externalreturns(uint){
returna[i];
}
}
```

--------------------------------

### Activate Virtual Environment (Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_user-guide_install.html.md

Activate the certora-beta virtual environment. Subsequent Python commands (like pip) will operate within this isolated environment.

```shell
sourcecertora-beta/bin/activate
```

--------------------------------

### CLI: Verify Rules Matching a Pattern with --rule

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html?highlight=--solc.md

Command-line example illustrating the use of the `--rule` option with a wildcard pattern (`withdraw*`) to verify all rules whose names start with 'withdraw_' in the `Bank.spec` file.

```CLI
certoraRunBank.sol--verifyBank:Bank.spec--rulewithdraw*
```

--------------------------------

### CLI: Exclude Rules Matching a Pattern with --exclude_rule

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html?highlight=--solc.md

Command-line example showing how to use the `--exclude_rule` option with a wildcard pattern (`withdraw*`) to skip verification for all rules whose names start with 'withdraw_' in the `Bank.spec` file.

```CLI
certoraRunBank.sol--verifyBank:Bank.spec--exclude_rulewithdraw*
```

--------------------------------

### Edit .profile File (Linux Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_user-guide_install.html.md

Open the .profile file in the user's home directory using the nano text editor to add or modify environment variables, such as the PATH, on Linux.

```shell
nano.profile
```

--------------------------------

### Running Certora Soroban Prover (Troubleshooting Step) - Shell

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_sunbeam_troubleshooting.html.md

Command to execute the `certoraSorobanProver` with a specified configuration file (`prover_config.conf`), used as a final step after setting up the environment and installing dependencies.

```Shell
certoraSorobanProver path/to/prover_config.conf
```

--------------------------------

### Create/Open .zshenv File (macOS)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_user-guide_install.html.md

Opens or creates the .zshenv file in the home directory using the nano text editor. This file is used to store environment variables for zsh shell.

```Shell
nano.zshenv
```

--------------------------------

### Certora CLI: Example with contract_recursion_limit

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html?highlight=--solc.md

Demonstrates how to use the `--contract_recursion_limit` option in a `certoraRun` command, setting the limit to 3 for verifying `Bank.sol` against `Bank.spec`.

```CLI
certoraRunBank.sol--verifyBank:Bank.spec--contract_recursion_limit3
```

--------------------------------

### Run Prover with Dynamic Bound - Certora Prover CLI

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html.md

Example command demonstrating how to run the Certora Prover with the `--dynamic_bound` option set to 1, verifying contract `C` using spec `C.spec` and including `Foo.sol`.

```CLI
certoraRunC.solFoo.sol--verifyC:C.spec--dynamic_bound1


```

--------------------------------

### Run Certora Rule totalSupplyAfterMint (Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_projects_tutorials_en_latest_lesson2_started_preconditions.html.md

This command executes the `totalSupplyAfterMint` rule from the `TotalGreaterThanUser.spec` file on the `ERC20.sol` contract using the Certora Prover CLI, specifying the solc version. Requires Certora Prover installation and the specified files.

```Shell
certoraRunERC20.sol--verifyERC20:TotalGreaterThanUser.spec--solcsolc8.0--ruletotalSupplyAfterMint
```

--------------------------------

### Using nondet_difficult_funcs Certora CLI Option

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html?highlight=--solc.md

When set, this option enables the Prover to automatically summarize view or pure internal functions that return a value type, are currently not summarized, and are heuristically identified as difficult. It helps in getting faster verification results and highlighting potentially problematic functions, especially when starting with a large codebase.

```Certora CLI
certoraRunBank.sol--verifyBank:Bank.spec--nondet_difficult_funcs
```

--------------------------------

### Running Certora Prover with Multiple Rules (CLI)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html.md

Command line example showing how to use the `--rule` option to verify multiple specific rules (`withdraw_succeeds` and `withdraw_fails`) in a single Certora Prover run.

```Certora CLI
certoraRunBank.sol--verifyBank:Bank.spec--rulewithdraw_succeedswithdraw_fails
```

--------------------------------

### Uninstall Certora Prover Package (Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_user-guide_install.html.md

Remove the standard certora-cli package using pip before installing the beta version to avoid conflicts. This is an optional step for beta installation.

```shell
pipuninstallcertora-cli
```

--------------------------------

### Install virtualenv (Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_user-guide_install.html.md

Install the virtualenv package using pip. This tool allows creating isolated Python environments, useful for managing different package versions like standard and beta Certora CLI.

```shell
pipinstallvirtualenv
```

--------------------------------

### Verifying Multiple Rules with Certora Solana Prover

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_solana_options.html.md

Command line example demonstrating how to use the --rule option to specify and verify multiple rules (rule_withdraw_succeeds and rule_withdraw_fails) in a single run of the Certora Solana Prover.

```Command Line
certoraSolanaProver--build_script<path_to_build_script>--rulerule_withdraw_succeedsrule_withdraw_fails
```

--------------------------------

### Example CVL Properties in Spec File

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html.md

Shows example invariant and rule definitions within a Certora spec file (`Bank.spec`). These properties are used as examples for the `split_rules` option, illustrating the types of rules that can be targeted.

```CVL
invariantaddress_zero_cannot_become_an_account()
rulewithdraw_succeeds()
rulewithdraw_fails()
```

--------------------------------

### Create/Edit PATH File (macOS Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_user-guide_install.html.md

Use sudo to create or edit a file named PythonForProver in /etc/paths.d using the nano text editor. This file will contain paths to be added to the system's PATH.

```shell
sudonanoPythonForProver
```

--------------------------------

### Certora Prover Configuration with Basic Mutations

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_gambit_mutation-verifier.html.md

Example of a Certora Prover configuration file (`.conf`) demonstrating the inclusion of a `mutations` object to enable and configure basic mutation testing using Gambit.

```JSON
{
"files":[
"contracts/ERC20.sol"
],
"verify":"ERC20:certora/spec/ERC20.spec",
"msg":"ERC20Rules",
"mutations":{
"gambit":[
{
"filename":"contracts/ERC20.sol",
"num_mutants":5
}
],
"msg":"basic mutation configuration"
}
}
```

--------------------------------

### Certora CLI command using method for one function

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html?highlight=--solc.md

Command line example demonstrating how to use the `method` option with `certoraRun` to focus the Prover analysis on a specific contract method (`C.deposit(uint)`), saving verification time.

```Shell
certoraRun--method'C.deposit(uint)'
```

--------------------------------

### Check Java Version (Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_user-guide_install.html.md

Execute this command in the terminal to check the installed version of Java. Requires JDK 11 or newer.

```shell
java-version
```

--------------------------------

### Strengthening Satisfy Condition (CVL)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_user-guide_satisfy.html.md

This snippet shows an alternative way to filter the examples produced by a `satisfy` statement. Instead of using a separate `require` statement, conditions can be added directly within the `satisfy` expression using logical operators like `&&` to ensure the generated examples meet specific criteria.

```CVL
satisfy(amount>0)&&...
```

--------------------------------

### Run Certora Prover with Configuration (Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_cvl_foundry-integration.html.md

Command line instruction to execute the Certora Prover using the specified configuration file. This initiates the verification process.

```Shell
certoraRun path/to/conf/file.conf
```

--------------------------------

### Run Prover with Dynamic Dispatch - Certora Prover CLI

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html.md

Example command demonstrating how to run the Certora Prover with both `--dynamic_bound` (set to 1) and `--dynamic_dispatch` options enabled, verifying contract `C` using spec `C.spec` and including `Foo.sol`.

```CLI
certoraRunC.solFoo.sol--verifyC:C.spec--dynamic_bound1--dynamic_dispatch


```

--------------------------------

### Check Python Version (Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_user-guide_install.html.md

Execute this command in the terminal to check the installed version of Python 3. Requires Python 3.8.16 or newer.

```shell
python3--version
```

--------------------------------

### Rule Demonstrating Full Withdrawal Scenario (CVL)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_user-guide_satisfy.html.md

This CVL rule, `possibleToFullyWithdraw`, demonstrates a scenario where a user deposits assets into a pool and immediately withdraws them. It uses the `satisfy` statement to request an example where the user's balance is the same before and after the deposit/withdrawal sequence. The `require amount > 0;` statement is included to filter out trivial examples.

```CVL
rulepossibleToFullyWithdraw(addresssender,uint256amount){
enveT0;
enveM;
setup(eM);
addresstoken;
requiretoken==_token0||token==_token1;
uint256balanceBefore=token.balanceOf(eT0,sender);
requireeM.msg.sender==sender;
requireeT0.msg.sender==sender;
requireamount>0;
token.transfer(eT0,currentContract,amount);
uint256amountOut0=mint(eM,sender);
// immediately withdraw 
burnSingle(eM,_token0,amountOut0,sender);
satisfy(balanceBefore==token.balanceOf(eT0,sender));
}
```

--------------------------------

### Certora Prover CLI: Set Max Loop Iterations Example

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html?highlight=--solc.md

Provides an example of using the `--loop_iter` option in a `certoraRun` command. This specific example sets the maximum number of loop unrolls to 2, allowing the prover to analyze scenarios involving up to two iterations of loops in the source code.

```Shell
certoraRunBank.sol--verifyBank:Bank.spec--loop_iter2
```

--------------------------------

### Running Certora Prover with Configuration File (Shell)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_projects_tutorials_en_latest_lesson2_started_config_files.html.md

This command executes the Certora Prover using the parameters defined in the `sample_conf.conf` file. The command assumes the configuration file is located in the current working directory.

```Shell
certoraRunsample_conf.conf
```

--------------------------------

### Example of Fully Unrolled Loop

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_approx_loops.html.md

The result of unrolling the constant loop example. The loop body is repeated three times, replacing the original loop structure.

```Generic
j++;
j++;
j++;
```

--------------------------------

### Using method via Certora CLI (Single)

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html.md

Demonstrates using the `--method` option on the command line to focus the Prover run on a single specific contract method (`C.deposit(uint)`). This is useful for debugging counterexamples by limiting the scope of verification.

```Shell
certoraRun--method'C.deposit(uint)'
```

--------------------------------

### Example using smt_initialSplitDepth CLI Option

Source: https://github.com/zgc-zgc/cerdocstest/blob/master/docs.certora.com_en_latest_docs_prover_cli_options.html?highlight=--solc.md

Demonstrates how to use the `smt_initialSplitDepth` option with the Certora Prover CLI, specifically setting it to `3` when running verification on `Bank.sol` with `bank.spec`. This is useful when initial splits are likely to timeout anyway.

```cli
certoraRunBank.sol--verifyBank:bank.spec--prover_args'-smt_initialSplitDepth 3'
```