autocertora 1.0.0

CLI tool that generates and validates Certora formal verification suites for Solidity codebases

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:

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.

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.

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:

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:

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:

pipx uninstall autocertora

Option 4: Install With pipx From PyPI

Use this after the autocertora package is available on PyPI:

pipx install autocertora
autocertora --help

To upgrade:

pipx upgrade autocertora

To remove a pipx install:

pipx uninstall autocertora

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

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:

~/.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:

autocertora run

Generate and locally validate a suite:

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

Generate only, without local Certora checks:

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:

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:

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:

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:

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 for contribution guidelines and CHANGELOG.md for release notes.

Run smoke tests:

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

Build a wheel locally:

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:

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.