certora-patrol 0.1.16

Automated smart contract security analysis powered by formal verification

Certora Patrol

Automated smart contract security analysis powered by formal verification.

Prerequisites

• Python 3.12+
• Java 21+ (required by the Certora prover)
• Foundry (forge build must succeed on your project)
• CERTORAKEY — Sign up at certora.com and store the API key from your signup email as an environment variable.
• ANTHROPIC_API_KEY — Beta testers will receive a Claude API key from Certora to cover LLM-related costs. Set it as an environment variable.

[!IMPORTANT] If you are a beta tester, make sure ANTHROPIC_API_KEY is set to the key provided by Certora, not your personal key. Patrol will first open your browser to authenticate with prover.certora.com.

Install

uv venv patrol-env && source patrol-env/bin/activate
uv pip install certora-patrol

Or with pip:

python -m venv patrol-env && source patrol-env/bin/activate
pip install certora-patrol

Usage

cd /path/to/your/contracts
patrol src/Token.sol

With explicit contract name (in case contract name does not match the file name):

patrol src/Vault.sol:MyVault

[!IMPORTANT] Both CERTORAKEY and ANTHROPIC_API_KEY must be set in your environment before running Patrol. You can also pass them inline: ANTHROPIC_API_KEY=sk-... CERTORAKEY=... patrol src/Token.sol.

What it does

1. Builds your project and sets up verification infrastructure
2. Runs formal verification checks (generic rules and AI-inferred rules)
3. Analyzes results with AI and generates an HTML report

Once complete, Patrol prints the path to the generated HTML report in the current working directory.