Certora AI Security Starter Kit

Automated smart contract security analysis powered by formal verification.

The AI Security Starter Kit is run with a command line tool called proverlite.

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, the tool 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.

The tool 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 the tool.

You can also pass them inline: ANTHROPIC_API_KEY=sk-... CERTORAKEY=... proverlite src/Token.sol.