Metadata-Version: 2.4
Name: autocertora
Version: 1.0.0
Summary: CLI tool that generates and validates Certora formal verification suites for Solidity codebases
Author: AutoCertora contributors
License-Expression: MIT
Classifier: Development Status :: 3 - Alpha
Classifier: Environment :: Console
Classifier: Intended Audience :: Developers
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Topic :: Software Development :: Testing
Classifier: Topic :: Security
Requires-Python: >=3.11
Description-Content-Type: text/markdown
License-File: LICENSE
Requires-Dist: typer
Requires-Dist: rich
Requires-Dist: InquirerPy
Requires-Dist: solc-select
Provides-Extra: dev
Requires-Dist: build; extra == "dev"
Requires-Dist: twine; extra == "dev"
Dynamic: license-file

# AutoCertora

AutoCertora generates a runnable Certora verification suite for a Solidity project.

Given a project path, it creates CVL specs, Certora `.conf` files, helper method specs, and harnesses where needed. It can also run local Certora compile/type checks and optionally submit passing jobs to Certora cloud.

## Important Limit

AutoCertora helps build a verification suite; it does not guarantee that the target protocol is bug-free or fully verified. Review the generated CVL, inspect Prover results, refine weak properties, and iterate before treating the suite as assurance.

## What AutoCertora Produces

For a Solidity project, AutoCertora writes a structured Certora suite:

```text
output/
  certora/
    specs/
      contracts/      # contract specs
      libraries/      # library wrapper specs
      abstract/       # abstract contract specs
      methods/        # reusable interface method blocks
    confs/            # certoraRun config files
    harness/          # generated Solidity harnesses when needed
    README.md         # generated suite summary
  .autocertora/
    runs/             # prompts, AI outputs, run metadata
    cache/            # reusable run cache
```

The first generated suite usually focuses on compile-ready rules and invariants that can be improved in later Certora iterations.

## Install

### Option 1: Run From A Cloned Repo

Use this when you already cloned the repository.

```bash
cd autocertora
./autocertora --help
./autocertora run
```

The local `./autocertora` launcher runs the package from `src/`.

### Option 2: Install From A Local Clone

Use this when you want the `autocertora` command available in your shell.

```bash
cd autocertora
python3 -m venv .venv
source .venv/bin/activate
python -m pip install -e .
autocertora --help
```

### Option 3: Install With pipx From A Local Checkout

Use this before the package is published, or when testing a local checkout as an installed CLI.

If you are inside the AutoCertora repo, install the current directory:

```bash
pipx install .
autocertora --help
```

If you are in the parent directory, install the repo directory. Replace `PATH_TO_AUTOCERTORA_REPO` with the actual folder name on your machine:

```bash
pipx install PATH_TO_AUTOCERTORA_REPO
autocertora --help
```

Do not run `pipx install ./autocertora` from inside the repo. In a source checkout, `./autocertora` is the local launcher file, not the Python package directory.

To remove the local `pipx` install:

```bash
pipx uninstall autocertora
```

### Option 4: Install With pipx From PyPI

Use this after the `autocertora` package is available on PyPI:

```bash
pipx install autocertora
autocertora --help
```

To upgrade:

```bash
pipx upgrade autocertora
```

To remove a `pipx` install:

```bash
pipx uninstall autocertora
```

If you installed inside a virtual environment with `pip`, remove it with:

```bash
python -m pip uninstall autocertora
```

Avoid installing directly into system Python unless necessary. On modern macOS, Debian, Ubuntu, and WSL, system Python may reject global `pip install` commands with an `externally-managed-environment` error (PEP 668). To resolve this, we highly recommend using `pipx` or a virtual environment as shown above. Alternatively, you can bypass the safety check by appending `--break-system-packages` to your `pip install` commands.

## Requirements

- OS: macOS (Intel & Apple Silicon), Linux, Windows (Native & WSL)
- Python 3.11+
- Codex CLI or Claude CLI
- Node/npm only if AutoCertora needs to install a missing AI CLI locally
- `CERTORAKEY` only if you want cloud submission

AutoCertora uses AI CLI adapters. Configure/authenticate Codex or Claude CLI before running AI generation.

## Global Tool Installation

AutoCertora manages its helper tools globally in your home directory:

```text
~/.autocertora/tools/runtime/       # Python runtime for source launcher
~/.autocertora/tools/node/          # global npm prefix for Codex/Claude packages
~/.autocertora/tools/certora-cli/   # global certora-cli virtualenv
~/.autocertora/tools/java/          # global Java runtime for Certora checks
```

It manages its own tools independently within `~/.autocertora` without modifying your system-wide OS packages.

## Quick Start

Interactive:

```bash
autocertora run
```

Generate and locally validate a suite:

```bash
autocertora run ../my-protocol --source src --output ../my-protocol/output --adapter codex --yes
```

Generate only, without local Certora checks:

```bash
autocertora generate ../my-protocol --source src --output ../my-protocol/output --adapter codex --yes
```

Generate, local-check, repair compile failures, and submit only when every generated job passes locally:

```bash
autocertora run ../my-protocol --source src --output ../my-protocol/output --adapter codex --submit --yes
```

AutoCertora keeps reusable run cache under the output directory, so rerunning the same command can reuse completed AI work and continue from already written generated files. Use a fresh output directory when you want a clean regeneration.

Sample compact output:

```text
Stage 1/7: Discovered Solidity files and contract definitions
Stage 2/7: Selected protocol profiles
Stage 3/7: Loaded invariant prompts
Stage 4/7: Code-analysis agent found invariant candidates
Stage 5/7: Generated specs
Stage 6/7: Wrote suite files
Stage 7/7: Final full-suite compile gate finished
```

## Commands

| Command | What it does |
| --- | --- |
| `autocertora` | Starts the interactive wizard. |
| `autocertora run [PROJECT]` | Generates the suite and runs local `certoraRun --compilation_steps_only` checks by default. |
| `autocertora generate [PROJECT]` | Generates suite files only. It does not run Certora checks. |
| `autocertora setup` | Detects Codex/Claude CLI and offers local installation if missing. |
| `autocertora init PATH` | Creates `.autocertora/settings.toml` defaults in a project. |
| `autocertora clean PATH` | Removes Python `__pycache__` folders from a project tree. |

## Flags

### Project Scope

| Flag | Meaning |
| --- | --- |
| `PROJECT` | Solidity project root. If omitted in interactive mode, AutoCertora asks for it. |
| `--source PATH` | Solidity source directory inside the project, usually `src` or `contracts`. |
| `--output PATH` | Directory where AutoCertora writes the generated suite. |
| `--full-scan` | Scan the selected source directory exactly instead of auto-detecting nested `src`/`contracts`. |
| `--include-interfaces` | Include interfaces in generation. Disabled by default. Libraries are always included. |
| `--yes`, `-y` | Use provided/default inputs without interactive prompts. |

### AI

| Flag | Meaning |
| --- | --- |
| `--adapter auto` | Pick the first available backend in priority order: Codex, then Claude. |
| `--adapter codex` | Use Codex CLI. |
| `--adapter claude` | Use Claude CLI. |
| `--model latest` | Model alias passed through AutoCertora's local adapter config. |
| `--ai-mode fast` | Default mode. One focused generation pass per concrete contract. |
| `--ai-mode deep` | More expensive multi-phase generation. Useful for manual research runs. |
| `--ai-mode off` | No AI calls. Writes only structural output that can be useful for debugging discovery; it does not create semantic specs. |
| `--analysis-agents N` | Override the number of code-analysis workers. |
| `--analysis-timeout N` | Optional timeout, in seconds, for code-analysis shards. No cap by default. |
| `--ai-timeout N` | Optional timeout, in seconds, for per-contract AI generation. No cap by default. |

### Protocol Selection

| Flag | Meaning |
| --- | --- |
| `--protocol lending` | Force a protocol profile instead of relying on inference. |
| `--protocol lending --protocol oracle` | Use multiple protocol profiles. |

Supported profiles include `access-control`, `algo-stables`, `amm`, `auction`, `bridge`, `cdp`, `cross-chain`, `derivatives`, `governance`, `lending`, `liquidity-manager`, `nft`, `oracle`, `prediction-market`, `privacy`, `rwa`, `staking`, `staking-pool`, `synthetics`, `vault`, `yield`, and `yield-aggregator`.

### Certora Validation

| Flag | Meaning |
| --- | --- |
| `--run-check` | Run local `certoraRun --compilation_steps_only` checks after generation. Default for `run`. |
| `--no-run-check` | Skip local Certora checks. |
| `--submit` | Submit the generated suite to Certora cloud only after every generated `.conf` passes local checks. |
| `--no-submit` | Do not submit jobs. Default. |
| `--certora-timeout N` | Optional timeout, in seconds, for local Certora checks/submissions. No cap by default. |
| `--repair-attempts N` | Maximum grouped AI compile-repair cycles before final validation. Default: `10`. Use `0` to disable AI repair. For large codebases, rerun the same command to resume or increase this value. |
| `--via-ir auto` | Follow project compiler config such as Foundry `via_ir = true`. Default. |
| `--via-ir on` | Force Certora config to use Solidity via-IR and optimizer. |
| `--via-ir off` | Do not add via-IR settings automatically. |

### Output And Debugging

| Flag | Meaning |
| --- | --- |
| `--debug` | Print full subprocess output and Python tracebacks on failure. |
| `--verbose`, `-v` | For `generate`, print every generated file path. |
| `--stage-delay N` | Keep completed progress stages visible for `N` seconds. Use `0` for no delay. |

## Environment Variables

Most users only need `CERTORAKEY` when submitting to Certora cloud. AutoCertora can read `CERTORAKEY` from a nearby `.env` file; it intentionally ignores other `.env` keys during normal Certora runs.

| Variable | Meaning |
| --- | --- |
| `CERTORAKEY` | Certora cloud key. Used only when submitting jobs. Can be placed in `.env`. |
| `PYTHONDONTWRITEBYTECODE=1` | Prevents Python from writing `__pycache__` folders. AutoCertora sets this internally where possible. |
| `AUTOCERTORA_DEBUG=1` | Enables debug behavior in subprocess helpers, similar to `--debug`. |
| `AUTOCERTORA_TOOLS_DIR` | Overrides the managed tools directory. Default: `~/.autocertora/tools/`. |
| `AUTOCERTORA_RUNTIME_DIR` | Overrides the source launcher Python runtime directory. |
| `AUTOCERTORA_AI_ADAPTER` | Default AI adapter when no CLI flag is provided. |
| `AUTOCERTORA_MODEL` | Default model alias when no CLI flag is provided. |
| `SOLC_VERSION` | Solidity compiler version for manual `certoraRun` commands. AutoCertora sets this automatically. |
| `JAVA_HOME` | Java path for manual `certoraRun` commands. AutoCertora auto-installs and manages its own Java runtime. |
| `PATH` | May need the managed Certora CLI bin path when running `certoraRun` manually. |

Example smoke-test command:

```bash
PYTHONDONTWRITEBYTECODE=1 PYTHONPATH=src python3 -B tests/smoke.py
```

Put `.env` in the Solidity project root you pass to AutoCertora. For example, if you run `autocertora run ../my-protocol --source src`, put it at `../my-protocol/.env`:

```bash
CERTORAKEY=
```

You can start from AutoCertora's `.env.example`. During Certora runs, AutoCertora checks `.env` in this order: the target project root, the target project root's parent, the AutoCertora checkout, then the AutoCertora checkout's parent. It imports only `CERTORAKEY` and ignores every other key.
Do not commit `.env`; AutoCertora's repository ignores it by default, and your Solidity project should ignore it too.

Developer-only cache refresh variables, not needed for normal generation:

| Variable | Meaning |
| --- | --- |
| `SOLODIT_API_KEY` | Used only to refresh bundled invariant seed data. |
| `AUTOCERTORA_SOLODIT_CACHE` | Overrides the local Solodit findings cache directory. |
| `SOLODIT_BASE_URL` | Overrides the Solodit API base URL for internal refreshes. |

## Validation Flow

`autocertora run` does this:

1. Generate suite files.
2. Run an initial local `certoraRun --compilation_steps_only` pass.
3. Group compile failures by error family and ask the AI repair agent to repair only failing configs.
4. Recheck repaired configs up to `--repair-attempts` grouped repair cycles.
5. Run the final full-suite compile gate across every generated config.
6. Submit only when every generated config passes final local compilation and `--submit` is set.

Normal output is compact. Full error details are written under `OUTPUT/.autocertora/errors/`; use `--debug` when you also want full subprocess output in the terminal. If validation still fails after the repair limit, rerun the same command to resume from `OUTPUT/.autocertora/cache/`, or pass a larger `--repair-attempts` value.

## CVL Guardrails

AutoCertora tries to avoid common generated-CVL problems:

- missing `envfree` on safe public getters,
- useless mutating declarations in `methods {}`,
- trivial invariants like `uintGetter() >= 0`,
- broad parametric rules over complex protocol flows,
- avoidable memory/path explosions from large structs, callbacks, hashes, or dynamic calldata,
- empty library specs by requiring wrapper-backed rules, scalar models, or repairable blockers.

## Known Limitations

- Generated specs are a starting point, not a replacement for review by someone who understands the protocol and Certora.
- Very large projects can still take a long time because AI generation and Certora local checks are expensive.
- Cross-contract invariants may need manual refinement when they depend on deployment topology, external callbacks, or protocol-specific accounting not visible from one target.
- Complex libraries with structs, dynamic arrays, callbacks, or low-level calls may require custom harness work.
- Cloud submission requires a valid `CERTORAKEY` and is blocked unless every generated config passes the local compile gate.
- AutoCertora uses local Codex or Claude CLI adapters.

## Development

See [CONTRIBUTING.md](CONTRIBUTING.md) for contribution guidelines and [CHANGELOG.md](CHANGELOG.md) for release notes.

Run smoke tests:

```bash
cd autocertora
PYTHONDONTWRITEBYTECODE=1 PYTHONPATH=src python3 -B tests/smoke.py
```

Build a wheel locally:

```bash
python3 -m pip wheel --no-deps --no-build-isolation -w /tmp/autocertora-wheel-check .
```

If using `python -m build`, install it inside a virtual environment first:

```bash
python -m pip install build
python -m build
```

## Reporting Issues

When reporting a generated-CVL or Certora failure, include:

- AutoCertora command and flags,
- project layout summary,
- failing `.conf` path,
- relevant `OUTPUT/.autocertora/errors/` log,
- whether rerunning with the same output directory changed the result.

Do not include private keys, `CERTORAKEY`, API keys, proprietary source code, or non-public audit material in public issues.
