certora-proverlite 0.2.1

Automated smart contract security analysis powered by formal verification

Certora ProverLite

Automated smart contract security analysis powered by formal verification.

What it does

1. Builds your project and sets up verification infrastructure.
2. Generates formal verification rules (generic and AI-inferred) and dispatches them to the Certora Prover.
3. Analyzes results from the Certora Prover with AI and generates an HTML report of all findings, ranked by their estimated likelihood of being real issues.

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

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

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.

Installation

With uv:

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 an explicit contract name (when the contract name differs from the file name):

proverlite src/Vault.sol:MyVault

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.