certora-proverlite 0.1.21

Automated smart contract security analysis powered by formal verification

Certora ProverLite

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. ProverLite will first open your browser to authenticate with prover.certora.com.

Install

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

Or with pip:

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

Usage

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

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

proverlite src/Vault.sol:MyVault

[!IMPORTANT] Both CERTORAKEY and ANTHROPIC_API_KEY must be set in your environment before running ProverLite. You can also pass them inline: ANTHROPIC_API_KEY=sk-... CERTORAKEY=... proverlite 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, ProverLite prints the path to the generated HTML report in the current working directory.