### Run PercentageMath Example with Certora

Source: https://github.com/certora/examples/blob/master/FoundryIntegration/PercentageMath/README.md

Use this command to run the PercentageMath example with Certora Prover. Ensure you have the necessary configuration file.

```bash
certoraRun PercentageMath.conf
```

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

### Running Extension Contracts Example

Source: https://github.com/certora/examples/blob/master/CVLByExample/ExtensionContracts/README.md

Command to run the extension contracts example using the Certora Prover. This command references a configuration file for the analysis.

```shell
certoraRun ExtensionContracts.conf
```

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

### Running Extension Contracts Override Example

Source: https://github.com/certora/examples/blob/master/CVLByExample/ExtensionContracts/README.md

Command to run an example demonstrating the `contract_extensions_override` flag. This flag is used in proxy patterns where the base contract also implements functions delegated to extensions.

```shell
certoraRun overrideExtended.conf
```

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

### Certora Prover Run Command

Source: https://github.com/certora/examples/blob/master/CVLByExample/InternalFunctionsFromCVL/README.md

The command to execute the Certora Prover for this example.

```bash
certoraRun InternalFunctionCall.conf
```

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

### Certora Run Command Example

Source: https://github.com/certora/examples/blob/master/RevertConditions/ReturnSize/README.md

This is the command used to run Certora Prover on the ReturnSize.conf configuration file.

```bash
certoraRun ReturnSize.conf
```

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

### Certora Run Command

Source: https://github.com/certora/examples/blob/master/CVLByExample/NativeCodeSize/README.md

The command to execute the Certora verification for the `nativeCodesize` example.

```bash
certoraRun NativeCodesize.conf
```

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

### Run Base.spec

Source: https://github.com/certora/examples/blob/master/CVLByExample/Import/README.md

Run the base specification file using the certoraRun command. This example shows the command to execute the 'Base.spec' file.

```shell
certoraRun runImported.conf
```

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

### Run Certora Prover for AssertFalse Example

Source: https://github.com/certora/examples/blob/master/CVLByExample/Summarization/Keywords/README.md

Execute the Certora Prover with the provided configuration file to analyze a specification that includes an ASSERT_FALSE rule. This demonstrates how the prover identifies specification failures when no appropriate function implementation is found.

```bash
certoraRun runAssertFalse.conf
```

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

### Run ERC20 Mutation Test

Source: https://github.com/certora/examples/blob/master/DEFI/ERC20/README.md

Use this command to run a mutation test on the ERC20 example.

```bash
certoraMutate mutation.conf
```

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

### Certora Run Command for TransientStorage

Source: https://github.com/certora/examples/blob/master/CVLByExample/TransientStorage/Hooks/README.md

Command to execute the Certora verification for the TransientStorage example.

```bash
certoraRun runTransientStorage.conf --server production --prover_version master
```

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

### Certora Run Command

Source: https://github.com/certora/examples/blob/master/CVLByExample/Ecrecover/Readme.md

Command to run Certora verification for the ecrecover example.

```bash
certoraRun Fullecrecover.conf --server production --prover_version master
```

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

### Run sub.spec

Source: https://github.com/certora/examples/blob/master/CVLByExample/Import/README.md

Run the importing specification file using the certoraRun command. This example shows the command to execute the 'sub.spec' file, which imports and extends 'Base.spec'.

```shell
certoraRun runImport.conf
```

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

### Run Certora Prover for UnresolvedNondet Example

Source: https://github.com/certora/examples/blob/master/CVLByExample/Summarization/Keywords/README.md

Execute the Certora Prover with the configuration file for the UnresolvedNondet example. This spec demonstrates summarizing an unresolved external call to return a nondeterministic value, asserting that contract storage remains unchanged.

```bash
certoraRun runUnresolvedNondet.conf
```

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

### Run CVL Spec

Source: https://github.com/certora/examples/blob/master/CVLByExample/Types/Structs/DirectStorageAccessToFields/README.md

Command to run the CVL specification for the direct storage access example.

```bash
certoraRun RootStruct.conf
```

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

### Certora Run Command

Source: https://github.com/certora/examples/blob/master/CVLByExample/Invariant/RequireInvariantArray/README.md

The command to execute the Certora Prover with the specified configuration file. Ensure the Certora CLI is installed before running.

```bash
certoraRun SortedArray.conf
```

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

### Ghost Mapping Summation Example

Source: https://github.com/certora/examples/blob/master/CVLByExample/Summarization/GhostSummary/GhostSums/README.md

Demonstrates summing values from a ghost mapping using the `sum` keyword. The summed variable must be used as an index to the ghost.

```CVL
ghost mapping(address => mapping(uint => int)) myGhost;
rule r {
    ... // some stuff that writes values to myGhost
	address a;
    assert sum uint u. myGhost[a][u] > 0;
}
```

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

### Summarizing with CONSTANT keyword

Source: https://github.com/certora/examples/blob/master/CVLByExample/Summarization/Keywords/README.md

Summarize a function to always return the same value, which can be any value. This example shows `get2` summarized as CONSTANT.

```solidity
rule constantCanbeAnyValue = g2 == 7
rule constantVsAlways = g1 != g2
rule constantDoesNotChange = forall { set2(v) }
  (g2 == old g2)
```

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

### Certora Mutate Command

Source: https://github.com/certora/examples/blob/master/CVLByExample/Ecrecover/Readme.md

Command to perform mutation testing on the ecrecover example.

```bash
certoraMutate --mutation_conf mutation.mconf --prover_conf Fullecrecover.conf --server production
```

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

### Summarizing with ALWAYS keyword

Source: https://github.com/certora/examples/blob/master/CVLByExample/Summarization/Keywords/README.md

Summarize a function to always return a specific value. This example shows `get1` summarized to always be 7, while `get2` remains unsummarized.

```solidity
rule isG1Always7 = g1 == 7
rule isG2Always7 = g2 == 7
```

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

### Advanced Linking Features

Source: https://github.com/certora/examples/blob/master/CVLByExample/LinksBlock/README.md

Showcases advanced capabilities of the `links { }` block, including multi-target dispatch, wildcard arrays, wildcard precedence, address-keyed and bytes4-keyed mappings, nested mappings, and struct arrays. This example requires the `AdvancedLinking.conf` configuration file.

```bash
certoraRun AdvancedLinking.conf
```

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

### Command to Run CVL Verification

Source: https://github.com/certora/examples/blob/master/CVLByExample/Types/Strings/README.md

The command to execute the CVL verification process for the string comparison example. Ensure the Solidity contract and CVL rule are correctly configured in String.conf.

```bash
certoraRun String.conf
```

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

### Example of Extended Contract with Fallback

Source: https://github.com/certora/examples/blob/master/CVLByExample/ExtensionContracts/README.md

Demonstrates an `Extended` contract that uses a fallback function to delegate calls to an extension contract. This pattern is useful for modularizing contract logic.

```solidity
contract Extended {
    address public extensionAddress; // Address of contract Extension

    // Fallback function will handle all calls that don't match a function signature
    fallback() external payable {
        // Delegate the call to contract Extension
        (bool success, ) = bAddress.delegatecall(msg.data);
        require(success, "Delegatecall failed");
    }
}

Contract B {
	function foo() external { ... }
}
```

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

### Run Storage Comparison Configuration

Source: https://github.com/certora/examples/blob/master/CVLByExample/Storage/README.md

Use this command to run the storage comparison configuration. It points to the Certora Prover output for the run.

```bash
certoraRun runStorage.conf
```

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

### Run Certora Prover

Source: https://github.com/certora/examples/blob/master/RevertConditions/MsgValue/README.md

Execute the Certora prover with the specified configuration file to analyze the Solidity contract.

```bash
certoraRun NonPayableRevert.conf
```

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

### Running Certora Verification

Source: https://github.com/certora/examples/blob/master/CVLByExample/ReroutingSummaries/README.md

This command initiates the verification process using the Certora prover with the specified configuration file. Ensure all contract and spec files are correctly set up before running.

```bash
certoraRun StoragePointerExample.conf
```

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

### Run Certora Prover Configuration

Source: https://github.com/certora/examples/blob/master/CVLByExample/Events/README.md

Execute the Certora Prover with a specific configuration file for analyzing the AuctionFixed contract.

```shell
certoraRun runAuctionFixed.conf
```

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

### Basic Linking with `links { }`

Source: https://github.com/certora/examples/blob/master/CVLByExample/LinksBlock/README.md

Demonstrates common linking patterns using the `links { }` syntax for scalar, immutable, struct, and static array fields. This is the recommended approach for new specifications.

```bash
certoraRun BasicLinking.conf
```

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

### Run LibraryVSContractSummary Spec

Source: https://github.com/certora/examples/blob/master/CVLByExample/Summarization/UserDefinedReturnType/README.md

Command to execute the library vs. contract summarization specification.

```bash
certoraRun runLibraryVSContractSummary.conf
```

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

### Run Certora Prover with `new_fields.conf`

Source: https://github.com/certora/examples/blob/master/CVLByExample/ConfInheritance/README.md

Executes the Certora Prover using the `new_fields.conf` configuration, which merges settings from `base.conf` and adds new fields.

```bash
certoraRun new_fields.conf
```

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

### Run Certora Prover Command

Source: https://github.com/certora/examples/blob/master/CVLByExample/HookDisabledOnResetStorageCommand/README.md

Command to execute the Certora Prover with the BankReset.conf configuration file.

```bash
certoraRun BankReset.conf
```

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

### Certora Run Command

Source: https://github.com/certora/examples/blob/master/CVLByExample/ContractAlias/README.md

Execute the Certora prover with the specified configuration file to verify the contract alias functionality.

```bash
certoraRun ContractAlias.conf
```

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

### Run Certora Prover with Structs Configuration

Source: https://github.com/certora/examples/blob/master/CVLByExample/Types/Structs/BankAccounts/README.md

This command executes the Certora Prover with a specific configuration file designed for testing struct functionalities.

```bash
certoraRun runStructs.conf
```

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

### Run Certora Prover

Source: https://github.com/certora/examples/blob/master/RevertConditions/SafeMath/README.md

Command to run the Certora Prover with the SafeMathReverts.conf configuration file.

```bash
certoraRun SafeMathReverts.conf
```

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

### Running a Certora verification

Source: https://github.com/certora/examples/blob/master/CVLByExample/LastReverted/README.md

Execute a Certora verification run using the specified configuration file.

```Shell
certoraRun RevertingConditions.conf
```

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

### Run Full Liquidity Pool Specification

Source: https://github.com/certora/examples/blob/master/DEFI/LiquidityPool/README.md

This command executes the Certora Prover with a comprehensive specification for the Liquidity Pool, designed to uncover potential bugs and verify invariants.

```certoraRun
certoraRun runFullPool.conf
```

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

### Base Configuration (`base.conf`)

Source: https://github.com/certora/examples/blob/master/CVLByExample/ConfInheritance/README.md

Defines shared default settings for Certora Prover verification, including source files, contract-spec pairing, and loop configurations.

```jsonc
{
  "files": ["MainContract.sol"],
  "verify": "MainContract:MainContract.spec",
  "msg": "Main contract",
  "optimistic_loop": true,
  "loop_iter": "3",
  "rule_sanity": "basic"
}
```

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

### Comparison with Old `link` Conf Flag

Source: https://github.com/certora/examples/blob/master/CVLByExample/LinksBlock/README.md

Illustrates linking using the older `link` configuration flag. This method is limited to scalar and immutable fields and is not recommended for new specifications.

```bash
certoraRun ConfStyleLinking.conf
```

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

### Run Certora Prover with `override_fields.conf`

Source: https://github.com/certora/examples/blob/master/CVLByExample/ConfInheritance/README.md

Executes the Certora Prover using the `override_fields.conf` configuration, which merges settings from `base.conf` and overrides existing fields.

```bash
certoraRun override_fields.conf
```

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

### Run Full ERC20 Specification Verification

Source: https://github.com/certora/examples/blob/master/DEFI/ERC20/README.md

Use this command to run the verification for the full ERC20 specification.

```bash
certoraRun runERC20Full.conf
```

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

### Run Certora Prover on Correct Teams Implementation

Source: https://github.com/certora/examples/blob/master/CVLByExample/Teams/README.md

Execute this command to verify the correct implementation of the Teams contract using the provided configuration.

```bash
certoraRun correct.conf
```

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

### Run FunctionSummary Spec

Source: https://github.com/certora/examples/blob/master/CVLByExample/Summarization/MultiContract/README.md

Execute the FunctionSummary specification using the certoraRun command.

```bash
certoraRun runFunctionSummary.conf
```

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

### Certora Run Command

Source: https://github.com/certora/examples/blob/master/DEFI/LiquidityPool/README.md

Command to execute the Certora prover for invariant verification. This command initiates the analysis of the smart contract against the specified configuration.

```shell
certoraRun strongInv.conf
```

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

### Run With Dispatcher With Link

Source: https://github.com/certora/examples/blob/master/CVLByExample/Summarization/Keywords/README.md

This command runs a spec with a dispatcher and linking, demonstrating correct resolution of summarized functions across contracts.

```bash
certoraRun runWithDispatcherWithLink.conf
```

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

### Certora Run Command

Source: https://github.com/certora/examples/blob/master/CVLByExample/Summarization/WildcardVsExact/README.md

Run the spec using the certoraRun command with the specified configuration file.

```bash
certoraRun runWildcardVsExact.conf
```

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

### Run Certora Prover with Partial Contract

Source: https://github.com/certora/examples/blob/master/CVLByExample/Optional/README.md

This command runs the Certora Prover with the 'Partial' contract as the main contract. Non-parameterized rules referencing 'bar(uint256)' are skipped because 'bar' is undefined in 'Partial'. Parameterized rules instantiate only functions present in 'Partial', thus passing.

```certoraRun
certoraRun runPartialOptional.conf
```

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

### Run Pool Configuration with Linking

Source: https://github.com/certora/examples/blob/master/DEFI/LiquidityPool/README.md

This command runs the Certora Prover with a configuration that includes linking, intended to resolve dependencies and potentially fix verification issues.

```certoraRun
certoraRun WithLinking.conf
```

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

### Run Pool Configuration with Flexible Linking

Source: https://github.com/certora/examples/blob/master/DEFI/LiquidityPool/README.md

This command runs the Certora Prover with a flexible linking configuration, offering a different approach to dependency resolution compared to standard linking.

```certoraRun
certoraRun WithFlexibleLinked.conf
```

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

### Run Certora Prover with Non-Precise Bitwise Operations

Source: https://github.com/certora/examples/blob/master/CVLByExample/PreciseBitwiseOps/README.md

Execute the Certora Prover with default settings, which may overapproximate bitwise operations. This command is used to demonstrate potential inaccuracies.

```bash
certoraRun BrokenPreciseBitwiseOps.conf
```

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

### Run Certora Prover on Buggy Teams Implementation

Source: https://github.com/certora/examples/blob/master/CVLByExample/Teams/README.md

Execute this command to verify the buggy implementation of the Teams contract using the provided configuration.

```bash
certoraRun buggy.conf
```

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

### Run ERC4626 Full Specification Check

Source: https://github.com/certora/examples/blob/master/DEFI/ERC4626/README.md

Configuration file to run the full ERC4626 specification check. This is used with the certoraRun command.

```certoraRun
runERC4626Full.conf
```

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

### Run DoublyLinkedList Spec

Source: https://github.com/certora/examples/blob/master/CVLByExample/QuantifierExamples/README.md

Execute the Certora spec for DoublyLinkedList using the provided configuration file.

```bash
certoraRun linkedCorrectly.conf
```

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

### Run No Summary With Link

Source: https://github.com/certora/examples/blob/master/CVLByExample/Summarization/Keywords/README.md

This command runs a spec with summarization and linking, showing how linking resolves function results correctly.

```bash
certoraRun runNoSummaryWithLink.conf
```

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

### Run Flashloan with Trivial Receiver

Source: https://github.com/certora/examples/blob/master/DEFI/LiquidityPool/README.md

This command runs the Certora Prover for a flashloan scenario using a trivial FlashLoanReceiver implementation. It verifies the system's behavior with a basic recipient.

```certoraRun
certoraRun FlashLoanTrivial.conf
```

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

### Certora Run Command

Source: https://github.com/certora/examples/blob/master/CVLByExample/TransientStorage/PreservedonTransactionBoundary/README.md

Command to execute the Certora verification with the 'preserved onTransactionBoundary' feature enabled. Ensure you have the correct configuration file.

```bash
certoraRun WithPreservedOnTransaction.conf
```

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

### Run Auction Configuration

Source: https://github.com/certora/examples/blob/master/CVLByExample/NativeBalances/README.md

This configuration file is used to run the Certora Prover on the Auction.sol contract. It is relevant for analyzing incorrect handling of native balances.

```certoraRun
runAuction.conf
```

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

### Run Certora Prover with Base Contract

Source: https://github.com/certora/examples/blob/master/CVLByExample/Optional/README.md

This command runs the Certora Prover with the 'Base' contract as the main contract. All rules, including those referencing 'bar(uint256)', will pass because 'bar' is defined in 'Base'.

```certoraRun
certoraRun runBaseOptional.conf
```

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

### Run EnumerableSet Spec

Source: https://github.com/certora/examples/blob/master/CVLByExample/QuantifierExamples/README.md

Execute the Certora spec for EnumerableSet using the provided configuration file.

```bash
certoraRun set.conf
```

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

### Running GhostSum Spec

Source: https://github.com/certora/examples/blob/master/CVLByExample/Summarization/GhostSummary/GhostSums/README.md

Command to run the `ghostSums.spec` configuration file using `certoraRun`.

```bash
certoraRun ghostSums.conf
```

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

### Run AuctionFixed Configuration

Source: https://github.com/certora/examples/blob/master/CVLByExample/NativeBalances/README.md

This configuration file is used to run the Certora Prover on the AuctionFixed.sol contract. It is relevant for analyzing the correct handling of native balances.

```certoraRun
runAuctionFixed.conf
```

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

### Run Certora Prover with Ghost Summary

Source: https://github.com/certora/examples/blob/master/CVLByExample/Summarization/GhostSummary/GhostMapping/README.md

Execute the Certora Prover with the `runInterest.conf` configuration file. This configuration utilizes a ghost function (`ghost_interest`) to provide a summarized behavior for `continuous_interest`, ensuring the monotonicity rule passes.

```bash
certoraRun.py runInterest.conf
```

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

### Certora Run Command for TargetCall with Linking

Source: https://github.com/certora/examples/blob/master/RevertConditions/TargetCall/README.md

Execute Certora Prover on the TargetCall contract configuration using linking.

```bash
certoraRun TargetCallLinking.conf
```

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

### Run Function Summarization with Environment

Source: https://github.com/certora/examples/blob/master/CVLByExample/Summarization/WithEnv/README.md

Command to run a CVL spec file that includes a function summary with the 'with env' attribute. Ensure you are in the correct directory.

```bash
certoraRun runWithEnv.conf
```

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

### Run Certora Prover with Broken Configuration

Source: https://github.com/certora/examples/blob/master/DEFI/ConstantProductPool/README.md

Execute the Certora Prover using the 'runBroken.conf' configuration file to check the incorrect ConstantProductPool contract. This command initiates the verification process for the faulty version.

```bash
certoraRun runBroken.conf
```

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

### Run Certora Prover with Precise Bitwise Operations

Source: https://github.com/certora/examples/blob/master/CVLByExample/PreciseBitwiseOps/README.md

Execute the Certora Prover with the `--precise_bitwise_ops` feature enabled for accurate modeling of bitwise operations. This command is used to verify smart contract logic precisely.

```bash
certoraRun PreciseBitwiseOps.conf
```

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

### Run Dispatcher Fallback Inlining

Source: https://github.com/certora/examples/blob/master/CVLByExample/Summarization/Keywords/README.md

This command runs a spec demonstrating how the prover can inline fallback functions when a direct implementation is not found, using a link configuration.

```bash
certoraRun runDispatcherFallbackInlining.conf
```

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

### Solidity Dummy Contract

Source: https://github.com/certora/examples/blob/master/CVLByExample/NativeCodeSize/README.md

A minimal Solidity contract used as a placeholder to demonstrate `nativeCodesize` verification.

```solidity
pragma solidity ^0.8.0;

contract Dummy {
}

```

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

### CVL Specification for Internal Function Calls

Source: https://github.com/certora/examples/blob/master/CVLByExample/InternalFunctionsFromCVL/README.md

Demonstrates calling internal Solidity functions from CVL, including summarization and restrictions on storage.

```cvl
methods {
    function summarizedInternal() internal returns (uint) => cvlSummary();
    // function anInternalFunction() internal returns (uint) envfree; <-- This will fail compilation: 'The envfree qualifier is not allowed on internal functions'
}

function cvlSummary() returns (uint) {
    return 1;
}

rule internalFunctionCall {
    env e;

    assert anInternalFunction(e) == 0;
    assert summarizedInternal(e) == 1;

    // A.S s;
    // internalFunctionWithStorageInput(e, s); <-- This will fail compilation: 'could not type expression "internalFunctionWithStorageInput(e,s)", message: Cannot call internal function internalFunctionWithStorageInput from spec because input parameter '_s' has storage location'
    // internalFunctionWithStorageOutput(e); <-- This will fail compilation: 'could not type expression "internalFunctionWithStorageOutput(e)", message: Cannot call internal function internalFunctionWithStorageOutput from spec because output parameter #0 has storage location'
}
```

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

### Run Flashloan with Malicious Receiver

Source: https://github.com/certora/examples/blob/master/DEFI/LiquidityPool/README.md

This command runs the Certora Prover for a flashloan scenario with a malicious receiver designed to exploit the pool. It tests the system's resilience against such attacks.

```certoraRun
certoraRun FlashLoanTransfer.conf
```

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

### Run Corrected Vat Contract Analysis

Source: https://github.com/certora/examples/blob/master/RealBugsFound/MakerDao/README.md

Execute the Certora Prover with the configuration file 'runVatFixed.conf' to analyze the corrected Vat contract.

```shell
certoraRun runVatFixed.conf
```

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

### Certora Run Command for TargetCall

Source: https://github.com/certora/examples/blob/master/RevertConditions/TargetCall/README.md

Execute Certora Prover on the TargetCall contract configuration.

```bash
certoraRun TargetCall.conf
```

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

### Run UserDefinedTypeSummary Spec

Source: https://github.com/certora/examples/blob/master/CVLByExample/Summarization/UserDefinedReturnType/README.md

Command to execute the user-defined type summarization specification, which covers functions returning structs.

```bash
certoraRun runUserDefinedTypeSummary.conf
```

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

### Run Unsummarized Square Root Spec

Source: https://github.com/certora/examples/blob/master/CVLByExample/Summarization/GhostSummary/SqrRoot/README.md

This command runs the Certora Prover with the original specification without any summarization for the square root function. It is used to demonstrate the timeout issue.

```bash
certoraRun runUnsummarizedSqrRoot.conf
```

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

### Run SinglyLinkedList Spec

Source: https://github.com/certora/examples/blob/master/CVLByExample/QuantifierExamples/README.md

Execute the Certora spec for SinglyLinkedList using the provided configuration file.

```bash
certoraRun list.conf
```

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

### Run Incorrect Pool Configuration

Source: https://github.com/certora/examples/blob/master/DEFI/LiquidityPool/README.md

This command runs the Certora Prover with an incorrect configuration for the Liquidity Pool, which will likely fail due to unresolved methods.

```certoraRun
certoraRun JustPool.conf
```

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

### Run Incorrect Vat Contract Analysis

Source: https://github.com/certora/examples/blob/master/RealBugsFound/MakerDao/README.md

Execute the Certora Prover with the configuration file 'runVat.conf' to analyze the incorrect Vat contract.

```shell
certoraRun runVat.conf
```

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

### Run No Summary No Link

Source: https://github.com/certora/examples/blob/master/CVLByExample/Summarization/Keywords/README.md

This command runs a spec without summarization and without linking, demonstrating how unresolved function results can lead to havoc.

```bash
certoraRun runNoSummaryNoLink.conf
```

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

### Certora Prover Command

Source: https://github.com/certora/examples/blob/master/CVLByExample/AddressFunctionCall/README.md

Command to run the Certora Prover for the AddressCall specification.

```bash
certoraRun AddressCall.conf
```

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

### Run Hand-Crafted Summarized Square Root Spec

Source: https://github.com/certora/examples/blob/master/CVLByExample/Summarization/GhostSummary/SqrRoot/README.md

This command runs the Certora Prover with a custom ghost summary for the `sqrRoot` function, providing a precise and efficient way to handle the square root operation and successfully prove the desired property.

```bash
certoraRun.py runSummarizedSqrRoot.conf
```

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

### Certora Configuration File

Source: https://github.com/certora/examples/blob/master/CVLByExample/Invariant/RequireInvariant/README.md

A configuration file used to run the Certora Prover with the specified Solidity contract and CVL specification. This file directs the prover to use the `DataInvariant.conf` settings.

```properties
# Configuration file for Certora Prover

# Specify the Solidity contract to analyze
<contracts>
DataInvariant.sol
</contracts>

# Specify the CVL specification file
<spec>
DataInvariant.spec
</spec>

# Specify the main function to verify (optional, but good practice)
# In this case, we are not verifying a specific function, but rather checking invariants.
# main DataInvariant.deposit

# Specify the prover mode (e.g., :prover, :counterexample)
# :prover is used for general invariant checking.
prover = :prover

# Specify the CVL version to use for analysis.
# This is crucial for observing the difference in requireInvariant semantics.
# For versions before 8, use a version like 0.8.x or earlier.
# For versions from 8 onwards, use a version like 0.8.x or later.
# Example for version 8+:
# cvl_version = 0.8.10
# Example for version < 8:
# cvl_version = 0.7.6

# Additional prover options can be added here as needed.
# For example, to set a timeout:
# timeout = 300

```

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

### Run Certora Prover with NotSummarized.spec

Source: https://github.com/certora/examples/blob/master/CVLByExample/Summarization/GhostSummary/GhostMapping/README.md

Execute the Certora Prover with the `runInterestNotSummarized.conf` configuration file to analyze the `continuous_interest` function without a ghost summary. This configuration is used when the default over-approximation leads to a reported violation.

```bash
certoraRun.py runInterestNotSummarized.conf
```

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

### Run InternalExternalSummary Spec

Source: https://github.com/certora/examples/blob/master/CVLByExample/Summarization/MultiContract/README.md

Execute the InternalExternalSummary specification using the certoraRun command.

```bash
certoraRun runInternalExternalSummary.conf
```

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

### Solidity BankReset Contract

Source: https://github.com/certora/examples/blob/master/CVLByExample/HookDisabledOnResetStorageCommand/README.md

A simple Solidity contract with a funds mapping and a dontUseMe state variable to demonstrate hook behavior during storage reset.

```solidity
pragma solidity ^0.8.0;

contract BankReset {
    mapping (address => uint256) public funds;
    uint256 public dontUseMe;
}
```

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

### Run Corrected ERC20 Verification

Source: https://github.com/certora/examples/blob/master/DEFI/ERC20/README.md

Use this command to run the verification for the corrected ERC20 contract implementation.

```bash
certoraRun runERC20Fixed.conf
```

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

### Immutable Contract Configuration

Source: https://github.com/certora/examples/blob/master/CVLByExample/Immutable/Readme.md

Configuration file for running the Certora verifier on the Immutable.sol contract. It specifies the contract to verify and how to link external contracts.

```configuration
certoraRun runImmutable.conf
```

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

### Summarizing an unknown function

Source: https://github.com/certora/examples/blob/master/CVLByExample/Summarization/Keywords/README.md

When summarizing an unknown contract, use a wildcard entry in the methods block to represent functions whose behavior is not specified.

```solidity
methods {
  function _.get1() external =>  ...
}
```

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

### Configuration for Contract Extensions

Source: https://github.com/certora/examples/blob/master/CVLByExample/ExtensionContracts/README.md

Shows the JSON configuration format for the `contract_extensions` option. This option maps extended contracts to their extension contracts and specifies functions to exclude.

```json
"contract_extensions": {
    "A": [
        {
            "extension": "B",
            "exclude": ["value", "sender", "num"],
        },
        {
            "extension": "C",
            "exclude": ["value", "sender", "num"],
        },
    ],
	"D": [
		...
	],
    ...
}
```

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

### Run Auto-Summarized Square Root Spec

Source: https://github.com/certora/examples/blob/master/CVLByExample/Summarization/GhostSummary/SqrRoot/README.md

This command runs the Certora Prover with the `--nondet_difficult_funcs` flag enabled, which automatically applies nondeterministic summaries to difficult internal functions like square root. This can resolve timeouts but may yield incorrect results.

```bash
certoraRun runAutoSummarizedSqrRoot.conf
```

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

### Running a Certora verification with a forgotten @withrevert

Source: https://github.com/certora/examples/blob/master/CVLByExample/LastReverted/README.md

Execute a Certora verification run for a spec where `@withrevert` was omitted, which will likely lead to compilation errors.

```Shell
certoraRun RevertingConditionsForgotWithRevert.conf
```