certora-prover

# Certora Formal Verification Skill Formal verification of smart contracts using Certora Prover, providing mathematical proofs of contract correctness. ## Capabilities - **CVL Specifications**: Write Certora Verification Language specs - **Invariant Rules**: Define and verify state invariants - **Parametric Rules**: Write comprehensive property tests - **Ghost Variables**: Track abstract state - **Counterexamples**: Analyze verification failures - **Loop Handling**: Configure loop invariants and unrolling - **Summarization**: Abstract complex functions ## Installation ```bash # Install Java (required) sudo apt install openjdk-17-jdk # Install Certora CLI pip install certora-cli # Set API key export CERTORAKEY=<your-api-key> # Verify installation certoraRun --version ``` ## Project Setup ### Directory Structure ``` project/ ├── contracts/ │ └── Token.sol ├── certora/ │ ├── conf/ │ │ └── token.conf │ └── specs/ │ └── token.spec └── foundry.toml ``` ### Configuration File ```yaml # certora/conf/token.conf { "files": ["contracts/Token.sol"], "verify": "Token:certora/specs/token.spec", "solc": "solc-0.8.20", "msg": "Token verification", "rule_sanity": "basic", "optimistic_loop": true, "loop_iter": 3 } ``` ## CVL Specification Language ### Basic Rules ```cvl // certora/specs/token.spec methods { function balanceOf(address) external returns (uint256) envfree; function totalSupply() external returns (uint256) envfree; functio...