Set up AutoProver, run formal verification, configure project context, understand billing, and troubleshoot common issues
AutoProver is an agentic pipeline for automatic specification inference and formal verification. It extracts intent from code and design documents, formalizes that intent into implementation-independent properties, and compiles the properties into CVL rules verified by the Certora Prover. Its companion engine, AutoFuzzer, turns generated properties into Foundry tests.
AutoProver is currently in beta and supports Solidity contracts.
For classic Certora Prover verification using your own CVL specifications and certoraRun, see Certora Prover access and billing. That guide covers Free-plan API keys, monthly verification minutes, and compatible clients. You can learn CVL in the Certora Verification Language documentation.
The platform also provides AI Auditor, a language-agnostic engine for finding issues in code and design documents, and AutoFuzzer, which generates and executes Foundry tests for Solidity contracts. Select All in one when you want AI Auditor, AutoProver, and AutoFuzzer to run together.
The workflow consists of six stages.
AutoProver extracts intended behavior from source code, comments, and documentation. A plain-language design document improves inference quality but is not required for a standalone AutoProver run.
Inferred intent is formalized into implementation-independent properties. These properties can cover individual modules and cross-module interactions.
AutoProver compiles properties into CVL rules for the Certora Prover. AutoFuzzer compiles generated properties into concrete scenario and Foundry fuzz tests. Select All in one to run both paths alongside AI Auditor.
Specialized agents run the generated tests and rules, triage failures, and troubleshoot tool invocations. Feedback agents validate soundness before results are reported. A separate bug-hunting agent checks for issues not covered by the inferred properties.
An AutoProver report presents:
AutoFuzzer reports include their generated tests, and All in one also includes the AI Auditor finding report. Generated artifacts can include CVL specifications, invariants, harnesses, tests, and configuration files. When the report contains eligible artifacts, use Create PR to propose them to the repository.
Retrying a run preserves its previous configuration so you can refine the inputs and analyze a newer commit.
AI Auditor findings, including those produced by All in one, can be marked Valid, Acknowledged, or Invalid with an optional note. Acknowledged feedback can update repository memory for later AI Auditor runs. This finding-feedback control is not currently available on every standalone AutoProver property.
| Engine | Language support | Purpose |
|---|---|---|
| AI Auditor | Any language | Finds issues in code and design documents |
| AutoProver | Solidity | Generates properties and verifies CVL rules with the Certora Prover |
| AutoFuzzer | Solidity | Generates and executes Foundry tests |
| All in one | Requires Solidity contracts; its AI Auditor portion can also inspect other languages | Runs all three engines together |
Rust support for AutoProver and AutoFuzzer is planned for a future release.
Open the sign-in dialog and choose one of the available methods:
When creating a new email and password account, follow the verification link sent to your inbox.
An organization is created automatically with your account. You can create additional organizations and invite members later.
Before starting your first run, make sure the organization has enough prepaid USD balance. Only an organization owner can manage billing or add funds.
From the organization dashboard, select Top Up Balance.
You can also open Settings, select Billing, and then open the Plan tab.
In the Balance card, select Top up balance and complete the Stripe checkout.
The run preview shows its estimated price and minimum balance requirement before anything starts. See Billing information for details.
An organization owner can connect GitHub for the whole organization:
Once connected, organization members can select repositories from the repository picker.
You can also start a run by entering a repository URL directly:
repo and read:org scopes.A standalone AutoProver run verifies one Solidity contract. For a combined AI Auditor, AutoProver, and AutoFuzzer review with up to three Solidity contracts, select All in one instead.
Prioritized is the default run mode. It selects the top-ranked property and its supporting cluster. Comprehensive formalizes all candidate properties, which usually takes more work, so we recommend a higher maximum budget for it. Both modes use the same conservative estimate. The overview shows your selected mode before launch. Closing Expert settings restores Prioritized.
Use Retry on a previous dashboard entry to prefill its repository and configuration. Review the selected commit and inputs, make any changes, and start the new run. The previous report remains available in history.
Diff runs are currently supported by AI Auditor only.
To analyze a change set, open Run, select AI Auditor, choose Diff, and provide the base and head commits. Both commits are resolved to full commit SHAs before launch.
Select All in one when you want:
The three engines run under one dashboard entry, and the report separates their results by engine and contract.
Standalone AutoProver derives project context from the selected Solidity contract and repository. It does not require the AI Auditor context and scope fields.
All in one includes AI Auditor, so it also lets you configure:
Keep the scope focused on the code that needs review while retaining enough surrounding context to understand dependencies and system behavior.
AutoProver automatically detects the likely main contract after you select a repository and commit.
Open Expert settings to replace the automatic selection when the repository contains several candidates or when you want to analyze a specific target.
The design document is one of the most important inputs for producing high-quality specifications. Project-specific documentation helps AutoProver infer intended behavior and generate more accurate rules and tests.
In Expert settings, select a repository-local Markdown (.md or .markdown) or PDF (.pdf) file. A design document is optional for both standalone AutoProver and All in one, but supplying one is strongly recommended.
A useful design document describes:
Focus on intended behavior rather than implementation details. Build instructions, deployment information, blockchain addresses, and source-code listings are generally unnecessary.
The document does not need to express invariants with mathematical precision. Complete and precise natural-language descriptions give AutoProver better material to formalize into verification properties.
A threat model identifies the attack vectors, trust assumptions, and failure modes that matter most to the project. Under Expert settings, you can select a repository-local Markdown or PDF threat-model file for AutoProver or All in one.
The document can include potential or known issues from:
AutoProver attempts to formalize these concerns into verification properties and uses generated tests and rules to determine whether the described behavior is feasible or impossible.
AutoFuzzer does not use a threat-model file.
The test and rule generation components are available in the open-source Certora AutoProver repository.
The local workflow is separate from the hosted service. Follow the repository's current setup instructions for its Foundry project requirements, model configuration, and Certora Prover credentials.
An organization is created automatically when your account is created. You can create additional organizations and invite other members. AutoProver has three organization roles:
| Role | Access |
|---|---|
| Owner | Full organization access, including members, billing, payment methods, plans, and organization deletion |
| Admin | Can start runs, manage organization settings, and invite or remove members; cannot manage billing |
| Member | Can start runs and view reports; cannot manage organization settings, members, or billing |
Every organization must retain an owner. Only an owner can grant the owner role. The number of members allowed depends on the organization's subscription plan.
See the dedicated REST API Reference for authentication, endpoint and scope tables, strict request schemas, complete examples, lifecycle behavior, errors, retries, and rate limits.
The API page supports two uses: paid engine runs through the Runs API, and classic Certora Prover verification. Runs API access is available on Pro and Enterprise plans and supported legacy plans. Certora Prover key access is available on the Free plan too, with separate monthly verification-minute allowances and metered billing. Enable Use Certora Prover when creating a key for classic verification. See Certora Prover access and billing for setup and replacing an existing key that lacks this permission.
Open API in the organization sidebar to create a scoped organization API key and view the live OpenAPI 3.1 reference. Authenticate Runs API requests with Authorization: Bearer <key>.
Version 2 exposes a separate strict launch contract for each workflow:
POST /v2/ai-auditor-full-runsPOST /v2/ai-auditor-diff-runsPOST /v2/ai-auditor-finding-validations-runsPOST /v2/auto-prover-runsPOST /v2/auto-fuzzer-runsAppend /estimate to any launch endpoint to quote the same request without reserving balance. AutoProver and AutoFuzzer estimates include a short-lived estimate_quote_id. Send that value in the launch request's Estimate-Quote-Id header to pin the launch to the repository estimate the caller just reviewed. The quote expires after 15 minutes and is bound to the organization key, engine, repository, commit, and contract. If it expires or does not match, request a fresh estimate. The header is optional for backward compatibility; omitting it causes launch to calculate the repository estimate again.
AutoProver and AutoFuzzer resolve the exact commit and selected contract before issuing a quote or reserving balance. An inaccessible or nonexistent commit returns 422 source_revision_not_found; a contract path absent at that commit returns 422 contract_not_found. Correct the source reference and estimate again—neither error creates a run or balance hold.
AutoProver and AutoFuzzer each analyze one explicit Solidity contract per run. AutoProver may also receive a design document and threat model; AutoFuzzer may receive a design document. The combined All in one workflow remains dashboard-only.
For a full AI Auditor run, use_memory defaults to true. Accepted repository assumptions are prepended to the audit instructions; they do not change the source-file globs in context.
Every source uses an immutable 40-character commit SHA. Request bodies are strict and limited to 256 KiB: unknown properties are rejected rather than ignored. You may estimate before a new launch, then launch the same body with an Idempotency-Key header containing a stable, non-empty value of at most 200 characters. If a request is interrupted, retry with the same service key, idempotency key, and identical body without requiring a fresh estimate or additional available balance. Reusing the key with a different body returns a conflict; a rotated ephemeral_token value does not count as a different body. Accepted, reservation-backed, and unresolved launches have no time-based expiry; retries recover accepted runs without launching or reserving balance again, even after 24 hours. Only completed pre-dispatch 4xx failures with no run or reservation may expire after 24 hours. Do not change the key to bypass a pending recovery; a new key represents a separate, potentially billable run. Estimate-Quote-Id is deliberately separate from the request body, so an idempotent replay can recover the original launch even after the quote's 15-minute lifetime.
Use the shared lifecycle endpoints after launch:
GET /v2/access shows the key's scopes and enabled workflows.GET /v2/runs lists recoverable runs with cursor pagination.GET /v2/runs/{run_id} returns status, embedded progress, billing, result availability, and delivery state. There is no separate progress endpoint.GET /v2/runs/{run_id}/result returns a versioned result whose shape is selected by run_type.GET /v2/runs/{run_id}/artifacts lists filtered user-visible artifacts and short-lived signed download URLs. limit defaults to 100 and cannot exceed 100; continue until next_cursor is null, including when a filtered page is empty.POST /v2/runs/{run_id}/cancel requests cancellation and is safe to repeat.Poll the run resource no faster than every 15 seconds, back off after transient failures, and honor Retry-After. A run does not become succeeded until provider completion, local billing settlement, and result publication have converged. While that is happening it reports finalizing; failed and cancelled runs do not expose a result. Timestamps in v2 responses are RFC 3339 strings or null. started_at is the durable first time the application observed the provider running; it remains null while queued and may be null for a historical or fast-terminal run that was never observed in running.
Errors use application/problem+json with the real HTTP status, a stable code, request_id, and retryable flag. Validation failures include field_errors; query failures name the rejected query field, while request-body failures name the rejected body path. Unknown /api/* and /v2/* endpoints return a JSON 404 endpoint_not_found, never a successful HTML page. Do not branch on the human-readable detail text.
Repository authentication is explicit in source.authentication:
public sends no repository credential.organization_github_app uses the organization's GitHub App installation.ephemeral_token accepts a caller token for the paid launch without persisting it. Caller tokens never reach the unmetered estimate. For a private repository in any paid workflow, the organization GitHub App must therefore also have read access for estimation; otherwise the estimate returns 422 repository_connection_required. Use public instead when the repository is public.To commit generated CVL specifications or Foundry tests, bind an AutoProver or AutoFuzzer launch to an open same-repository pull request in its delivery field. The organization GitHub App must be connected to the repository and the pull request head must still match the audited commit. After the run succeeds, call POST /v2/runs/{run_id}/generated-files/commit; the GitHub App performs the write. The operation is idempotent and returns either committed with a commit SHA or no_changes.
Public automation uses separate organization buckets: 50 launches per rolling hour, 120 estimates per rolling hour, 1,000 general reads per rolling hour, 120 generated-file delivery requests per rolling hour, and 30 artifact-list requests per rolling minute. Downloading a returned signed artifact URL does not consume the API bucket.
API keys are scoped to one organization and tied to their creator. A key stops working if its creator leaves that organization or is banned, or if the key expires or is revoked. During offboarding, create a replacement key under a remaining member, update the affected integration, and revoke the old key. Keep keys secret and rotate a key immediately if it may have been exposed.
On an eligible plan, an organization owner can open GitHub Action in the sidebar and install the integration for a connected repository. The installer creates a pull request containing a workflow configured for one of these engines:
Pro organizations can install AI Auditor diff reviews and either standalone engine. Full AI Auditor reviews in the one-click CI installer require Enterprise or a supported legacy plan.
AutoProver and AutoFuzzer fail the check only when the normalized outcome is issues_found. Incomplete coverage or other verification gaps are reported as warnings so reviewers can inspect them without treating every gap as a confirmed vulnerability. Generated files are committed as a follow-up to the same run and are not billed as a second analysis.
Each AI Auditor, AutoProver, AutoFuzzer, and All in one run is billed from the organization's prepaid USD balance. Classic Certora Prover verification has its own monthly free minutes and metered billing; those allowances do not cover these engine runs.
Before a run starts, the platform calculates the plan-adjusted reservation requirement from the current billing configuration and workflow estimate, then holds that amount while the run executes. The preview and API launch response show the exact requirement for that run. When the run finishes, the platform charges the actual billable amount and releases the unused reservation.
For questions about cash refunds or an exceptional billing event, open Support and choose Talk to a human. Refund eligibility is governed by the applicable plan and terms.
Repository synchronization can take a few minutes. Refresh the repository picker after the connection finishes. If the repository still does not appear, verify that the GitHub installation can access it, reconnect GitHub if necessary, or enter its URL and use a PAT for that run.
The project may use a build system or configuration that AutoProver does not yet support. Confirm that the selected commit and contract are correct and that the project can be built. If the problem persists, contact Support with the run link.
A working Foundry configuration is strongly recommended before running AutoProver or AutoFuzzer, but the hosted pipeline may be able to prepare some projects that do not already include one.
You have several options:
Clarify the intended behavior in the design document and retry the run. The more complete and precise the design document is, the better AutoProver can infer intended properties and generate accurate rules and tests.
For an AI Auditor finding, use its Valid, Acknowledged, or Invalid control and add a note explaining the intended behavior.
Tests that depend on external or filesystem cheatcodes, or on FFI, can fail because those capabilities are disabled to reduce prompt-injection risk. Core testing cheatcodes such as prank, warp, and expectRevert remain available.
No. If a run fails before producing billable output, its reservation is released and the run is not charged. Cancelled runs are different: they are charged for work completed before cancellation.
A run that its time or token budget cut short is also different. If the report shows partial results (an unverified draft specification or drafted properties), the run is charged like a successful run. If the budget stopped the run before it produced anything, the run is not charged.
If a run checks several contracts, each contract is billed on its own. You pay for the contracts that produced results, and a contract that failed is not charged.
Open Support from any organization page and choose Talk to a human. Human handoff is free, and replies appear in the same support conversation.