Metadata-Version: 2.4
Name: certora-proverlite
Version: 0.2.2
Summary: Automated smart contract security analysis powered by formal verification
Author-email: Certora Team <support@certora.com>
License: Proprietary
Project-URL: Homepage, https://certora.com
Keywords: certora,verification,smart contracts,security,audit
Classifier: Development Status :: 4 - Beta
Classifier: Intended Audience :: Developers
Classifier: Topic :: Software Development :: Testing
Classifier: Topic :: Security
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.12
Classifier: Programming Language :: Python :: 3.13
Requires-Python: >=3.12
Description-Content-Type: text/markdown
Requires-Dist: certora-cli-beta-mirror>=8.10.1
Requires-Dist: anthropic>=0.18.0
Requires-Dist: claude-agent-sdk>=0.1.0
Requires-Dist: Flask>=2.3.0
Requires-Dist: isodate>=0.6.0
Requires-Dist: Jinja2>=3.0.0
Requires-Dist: json5>=0.9.0
Requires-Dist: python-dotenv>=1.0.0
Requires-Dist: tqdm>=4.65.0
Requires-Dist: lark>=1.2.2
Requires-Dist: pycryptodome>=3.20.0
Requires-Dist: boto3>=1.26.0
Requires-Dist: requests>=2.28.0
Requires-Dist: urllib3>=1.26.0
Requires-Dist: beautifulsoup4>=4.12.0
Requires-Dist: chromadb>=0.4.0
Requires-Dist: langchain==0.3.27
Requires-Dist: langchain-anthropic==0.3.21
Requires-Dist: langchain-community==0.3.29
Requires-Dist: langchain-core==0.3.79
Requires-Dist: langchain-text-splitters==0.3.11
Requires-Dist: langgraph==0.6.7
Requires-Dist: langgraph-checkpoint-postgres==3.0.0
Requires-Dist: langgraph-sdk==0.2.6
Requires-Dist: numpy==2.3.2
Requires-Dist: psycopg==3.2.12
Requires-Dist: psycopg-binary==3.2.12
Requires-Dist: pydantic==2.11.7
Requires-Dist: pydantic-settings==2.10.1
Requires-Dist: sentence-transformers==5.1.0
Requires-Dist: spacy>=3.7.0
Requires-Dist: torch==2.8.0
Requires-Dist: transformers==4.56.0
Requires-Dist: einops>=0.8.0

# 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](https://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](https://prover.certora.com).

## Installation

With `uv`:
```bash
uv venv proverlite-env && source proverlite-env/bin/activate
uv pip install certora-proverlite
```

Or with `pip`:

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

## Usage

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

With an explicit contract name (when the contract name differs from the file name):

```bash
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`.
