REST API Reference

Organization API keys support two uses:

The Certora Runs API is an organization-scoped REST API for the first use. The Certora Prover guide explains key setup, client compatibility, and verification-minute billing for the second. AutoProver generates CVL specifications; classic Certora Prover verifies specifications you supply. You can learn CVL in the Certora Verification Language documentation.

Use the version 2 endpoints documented here for new integrations. The engine-specific /api/ai-auditor/*, /api/auto-prover/*, /api/auto-fuzzer/*, and /api/all-in-one/* routes are internal dashboard interfaces and are not public integration contracts.

• Production base URL: https://app.certora.com
• OpenAPI 3.1 document: https://app.certora.com/v2/openapi.json
• Content type: application/json
• Error content type: application/problem+json

The All in one workflow is currently dashboard-only. Public API v2 supports AI Auditor full, diff, and finding-validation runs plus standalone AutoProver and AutoFuzzer runs.

Access and authentication

Runs API access requires an eligible plan, such as Pro or Enterprise. Certora Prover key access is also available on the Free plan. Open API in the organization sidebar to create an organization API key. Give each key only the scopes its integration needs. For classic Prover verification, enable Use Certora Prover (prover:access) under Permissions; this does not unlock paid engine endpoints.

Send the key as a bearer token on every request:

Authorization: Bearer <service-key>

Set these shell variables for the examples below:

export CERTORA_API_BASE_URL="https://app.certora.com"
export CERTORA_API_KEY="<service-key>"

Keys are scoped to one organization and tied to the user who created them. 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 integration, and revoke the old key. Never place a key in browser code, a repository, logs, or a request body.

Service-key scopes

Key permissions cannot be changed after creation. Existing keys are not automatically granted prover:access. If your Prover client's key lacks it, create a replacement with Use Certora Prover, update the client, and revoke the old key when it is no longer needed.

On a plan with Runs API access, GET /v2/access accepts any active key. Use it to verify authentication, inspect the key's scopes, list enabled run types, check GitHub App connectivity, and read the organization balance.

curl --fail-with-body \
  -H "Authorization: Bearer $CERTORA_API_KEY" \
  "$CERTORA_API_BASE_URL/v2/access"

GitHub CI setup

The SaaS CI installer requires both the GitHub Action and API integrations to be enabled. For the generated workflow, create a service key with runs:create, runs:read, and runs:cancel; AutoProver and AutoFuzzer also require generated_files:write.

In the target GitHub repository, open Settings > Secrets and variables > Actions, click New repository secret, and name it exactly CERTORA_API_KEY. Paste the full service key shown once at creation into Secret, then click Add secret. Use a repository secret, not an Actions variable or environment secret. Never paste the key into YAML or the setup PR.

Endpoint overview

Advanced Prover client integrations

This reference is for developers building compatible Prover clients. Verification users can follow the Prover access and billing guide; their client handles authentication and job billing.

Authenticate with an active organization API key carrying prover:access, whose creator remains a current, unbanned member. Enable Use Certora Prover when creating the key. This endpoint is available on Free and paid plans. No request body or Idempotency-Key is required. A key without the required scope receives 403 insufficient_scope.

curl --fail-with-body \
  -X POST \
  -H "Authorization: Bearer $CERTORA_API_KEY" \
  "$CERTORA_API_BASE_URL/v2/prover/token"

The successful response contains only the token, without a request_id or run envelope:

{
  "token": "<short-lived-jwt>"
}

The token identifies the key's creator and organization. Its lifetime is configured by CERTORA_JWT_TTL_SECONDS, defaulting to 300 seconds. Obtain a fresh token by repeating the exchange when needed. Exchanging a token creates no run, consumes no verification minutes, and reserves no balance; billing begins when the compatible Prover service reserves minutes for a job. See the OpenAPI specification for response and error schemas.

This HTTP example does not configure a legacy certoraRun installation. Organization-key verification requires a compatible client and backend; legacy clients that only accept hexadecimal CERTORAKEY credentials cannot use an organization API key through that setting.

Estimate and launch

Run lifecycle

Source and repository authentication

Every run is pinned to an immutable 40-character Git commit SHA. Branch names, tags, and abbreviated SHAs are not accepted.

The source.authentication object explicitly selects repository access:

Example source:

{
  "source": {
    "repository_url": "https://github.com/acme/vault",
    "commit_sha": "0123456789abcdef0123456789abcdef01234567",
    "authentication": {
      "type": "organization_github_app"
    }
  }
}

Estimation and the pre-launch balance preflight are unmetered and do not receive an ephemeral_token. A private repository therefore requires the organization GitHub App to have read access for this preflight, including automatic-context launches. Otherwise the request returns 422 repository_connection_required. The caller's ephemeral token is used only for execution after balance reservation.

Connecting or reconnecting that GitHub App requires a SaaS organization owner who is also the personal GitHub account owner or an active owner of the GitHub organization. Repository access alone does not authorize an installation-wide connection.

Request bodies are strict and limited to 256 KiB. Unknown properties are rejected rather than ignored. Repository paths must be canonical, repository-relative paths with forward slashes; absolute paths, backslashes, and . or .. segments are rejected.

Automatic context and optional estimates

For AI Auditor full, diff, and finding-validation runs, prefer omitting context or sending []. Send one audit request to the launch endpoint: the server performs a deterministic balance preflight, reserves funds, and selects context inside the queued audit job. No client preview, estimate call, or configuration key is required. Automatic full audits require a non-empty user-chosen scope; diff and finding validation derive their scope from the diff or finding. Non-empty context remains an expert override, and no client should replace omitted context with broad local globs or an invented whole-repository scope.

You may send the exact launch body to the matching /estimate endpoint first. Estimation does not create a run, reserve balance, or perform LLM context preparation. With automatic context it returns a conservative preliminary estimate over candidate source files, not the final selected context or a prepared audit configuration. Explicit-context estimates keep their existing behavior. Actual charged cost is settled after execution; the launch response reports the real reservation in run.billing.reserved_usd.

Auto Context uses read-only repository tools to select and validate context and audit shards. The server controls its spending, time, and request limits; these are not public request parameters or a client-selected budget for the audit. If planning cannot finish within those limits, the run reports a typed failure rather than passing an invalid or silently narrowed evidence plan to analysis. Recovering an accepted run with the same launch key does not create another planning attempt or reset its allowance.

AI Auditor full, diff, and finding-validation requests accept optional model_mode: normal (the default) or frontier. This selects the model lineup for audit execution, with the configured Luna helper unchanged. Estimate and launch with the same mode; retries must preserve the exact body and must never silently drop or downgrade the mode. AI Auditor estimates return the priced model_mode.

The interactive dashboard prepares automatic context/shards during a free preview. It lets you change Normal/Frontier, sharing context preparation between modes with the Normal planner. The prepared files stay visible while pricing updates, and launch waits for the selected mode's price. Closing Preview stops browser polling, not preparation; reopening with unchanged settings reconnects to the same attempt, including an existing failure. Only an explicit Retry starts a fresh preparation attempt. The dashboard assigns that click a fresh internal retry UUID and reuses it for transport retries. That UUID is not a public API input and is distinct from the launch Idempotency-Key. A stale or expired prepared configuration requires a refreshed preview and price confirmation before launch.

Public API, Guardian CI, and Codex/Claude plugin/MCP callers do not need this interactive preview; omitted or empty context selects the one-request flow described above. Optional API estimates and dashboard previews do not charge the organization or reserve its balance.

Model mode and iteration count are independent. Full and diff API runs retain optional max_iterations from 2–10, defaulting to 6 for either mode. Finding validation has no DeepDive iteration setting. The dashboard uses up to six iterations for Normal and Frontier; API and Guardian CI callers can retain their explicit iteration overrides. AutoProver and AutoFuzzer do not accept model_mode.

curl --fail-with-body \
  -X POST \
  -H "Authorization: Bearer $CERTORA_API_KEY" \
  -H "Content-Type: application/json" \
  --data @run.json \
  "$CERTORA_API_BASE_URL/v2/auto-prover-runs/estimate"

Estimate responses contain plan-adjusted decimal USD strings and whether the current balance can launch the run:

{
  "request_id": "9fb0634b-5353-4f3e-86ef-421a087e19c6",
  "estimate": {
    "estimated_cost_usd": "31.2500",
    "minimum_balance_required_usd": "31.2500",
    "balance_usd": "250.0000",
    "can_launch": true,
    "estimate_quote_id": "22222222-2222-4222-8222-222222222222"
  }
}

AutoProver and AutoFuzzer estimates include estimate_quote_id. The quote:

• Expires after 15 minutes
• Is bound to the organization key, engine, repository, commit, and contract
• Pins launch to the repository estimate the caller reviewed
• Must be sent in the Estimate-Quote-Id launch header, not in the request body

AI Auditor estimates do not return an estimate quote.

AutoProver and AutoFuzzer resolve the commit and contract before issuing a quote. An inaccessible commit returns 422 source_revision_not_found; a missing contract returns 422 contract_not_found. Neither error creates a run or balance hold.

Auto Context billing

For direct AI Auditor runs, including Guardian CI and plugin launches, known Auto Context usage is included exactly once in the successful or cancelled run's actual cost, with the normal plan-adjusted pricing. The existing overall hard-runtime timeout policy can supersede normal settlement with a full refund. Auto Context is not a separate preview fee. A failed run receives a full reservation refund, even if Auto Context consumed provider tokens before failing. The server's planning allowance is an execution limit, not an amount automatically charged to the customer.

Cancellation may need to finish recording an in-flight request's usage. Keep polling until run.billing.status is settled; an earlier progress value or cancellation acknowledgement is not the final charge. Unknown provider outcomes are not billed as though the full planning allowance was consumed.

Launch safely with idempotency

Every launch requires an Idempotency-Key header containing 1–200 characters. Generate one stable key for one logical launch:

export IDEMPOTENCY_KEY="$(uuidgen)"

curl --fail-with-body \
  -X POST \
  -H "Authorization: Bearer $CERTORA_API_KEY" \
  -H "Content-Type: application/json" \
  -H "Idempotency-Key: $IDEMPOTENCY_KEY" \
  -H "Estimate-Quote-Id: 22222222-2222-4222-8222-222222222222" \
  --data @run.json \
  "$CERTORA_API_BASE_URL/v2/auto-prover-runs"

If the request is interrupted or its outcome is ambiguous, retry the same endpoint with the same service key, Idempotency-Key, and unchanged body. Reusing a key with a different body returns 409 idempotency_conflict. The value of an ephemeral_token is not part of the request identity (its type is), so a retry may carry a freshly minted token, such as a new CI job token. Accepted, reservation-backed, and unresolved launches remain protected without a time-based expiry, including GitHub reruns more than 24 hours later. Only completed pre-dispatch client failures (4xx) with no run or balance reservation may expire after 24 hours. Use a new key only when you intentionally want a separate, potentially billable run.

If the audit was accepted before the connection or server process failed, a retry recovers the original run and its client_reference without starting another audit or reserving balance again. Do not gate recovery on a new estimate: the original hold may have reduced the available balance, but recovering that run requires no additional funds. While acceptance is still being reconciled, honor the retryable response and Retry-After; do not switch to a new key to bypass it.

Estimate-Quote-Id is optional for backward compatibility. Omitting it makes AutoProver or AutoFuzzer recalculate the repository estimate. After estimate_quote_invalid or estimate_quote_unavailable, estimate again and launch with the new quote.

A successful launch returns 202 Accepted, a request_id, and the canonical run object.

Launch request schemas

AI Auditor full run

POST /v2/ai-auditor-full-runs

{
  "source": {
    "repository_url": "https://github.com/acme/protocol",
    "commit_sha": "0123456789abcdef0123456789abcdef01234567",
    "authentication": { "type": "organization_github_app" }
  },
  "model_mode": "normal",
  "scope": ["src/**/*.sol"],
  "instructions": "Focus on authorization and accounting invariants.",
  "skip_submodules": true,
  "max_iterations": 6,
  "use_memory": true,
  "client_reference": "release-2026-08-13"
}

context is optional: omission or [] selects context automatically from the non-empty scope. The example audits Solidity, but AI Auditor supports any programming language. A non-empty array of repository globs is an expert context override and should include relevant dependencies; for example, add "context": ["src/**", "lib/**"] when intentionally choosing those files. With an explicit override, scope optionally narrows the audited files. Without an override, scope is required and cannot be empty; the client must not infer **/*. max_iterations accepts 2–10 and defaults to 6. use_memory defaults to true; accepted repository assumptions are prepended to instructions without changing the requested scope.

AI Auditor diff run

POST /v2/ai-auditor-diff-runs

{
  "source": {
    "repository_url": "https://github.com/acme/protocol",
    "base_commit_sha": "0123456789abcdef0123456789abcdef01234567",
    "head_commit_sha": "89abcdef0123456789abcdef0123456789abcdef",
    "authentication": { "type": "organization_github_app" }
  },
  "model_mode": "frontier",
  "instructions": "Review security-relevant behavior changed by this diff.",
  "skip_submodules": true,
  "max_iterations": 6,
  "client_reference": "pull-request-418"
}

The base and head commits must differ. Omit context or send [] to audit the full diff with automatically selected supporting context. A non-empty context override retains the existing semantics: its globs also filter the changed files to audit. Selecting supporting files automatically does not expand the diff's audited scope.

AI Auditor finding validation

POST /v2/ai-auditor-finding-validations-runs

{
  "source": {
    "repository_url": "https://github.com/acme/protocol",
    "commit_sha": "0123456789abcdef0123456789abcdef01234567",
    "authentication": { "type": "organization_github_app" }
  },
  "model_mode": "normal",
  "finding": "An untrusted caller may withdraw another account's assets.",
  "skip_submodules": true,
  "client_reference": "finding-SEC-104"
}

The finding is required and may contain up to 8,000 characters. Omit context or send [] to select relevant context from the finding. Supply non-empty repository globs only when explicitly overriding that selection. No separate scope or preview request is required.

AutoProver run

POST /v2/auto-prover-runs

{
  "source": {
    "repository_url": "https://github.com/acme/vault",
    "commit_sha": "0123456789abcdef0123456789abcdef01234567",
    "authentication": { "type": "organization_github_app" }
  },
  "contract": {
    "path": "src/Vault.sol",
    "name": "Vault"
  },
  "limits": {
    "max_budget_usd": 150,
    "time_budget_seconds": 14400
  },
  "documents": {
    "design": "docs/design.md",
    "threat_model": "docs/threat-model.pdf"
  },
  "delivery": {
    "type": "github_pull_request",
    "pull_request_number": 418
  },
  "client_reference": "pull-request-418"
}

AutoProver analyzes one explicit Solidity contract. Design and threat-model documents are optional and must be repository-local Markdown or PDF files.

Optional run_mode is prioritized (the default) or comprehensive. Prioritized selects the top-ranked property and its supporting cluster. Comprehensive formalizes all candidate properties, which usually takes more work, so we recommend a higher max_budget_usd for it. Both modes use the same conservative estimate. AutoFuzzer does not accept run_mode.

Optional limits sets ceilings for this run; each field is independent and omitted fields keep the defaults:

• max_budget_usd caps the balance hold for the run, up to 10,000 with at most four decimal places. It must be at least the run's current estimated price, otherwise the launch returns 422 invalid_max_budget and nothing is reserved. The engine's AI budget is derived from it. AWS runtime is billed on top at settlement, so the final charge can be higher than this value. Omitted, the standard reservation applies.
• time_budget_seconds, from 1 to 72,000 (the engine's default), asks the run to wrap up and publish its results sooner. It can only shorten a run.

AutoFuzzer runs do not accept limits.

AutoFuzzer run

POST /v2/auto-fuzzer-runs

{
  "source": {
    "repository_url": "https://github.com/acme/vault",
    "commit_sha": "0123456789abcdef0123456789abcdef01234567",
    "authentication": { "type": "organization_github_app" }
  },
  "contract": {
    "path": "src/Vault.sol",
    "name": "Vault"
  },
  "documents": {
    "design": "docs/design.md"
  },
  "delivery": {
    "type": "github_pull_request",
    "pull_request_number": 418
  },
  "client_reference": "pull-request-418"
}

AutoFuzzer analyzes one explicit Solidity contract. It accepts an optional design document but does not accept a threat-model document.

Monitor a run

The launch response's run.id is the run UUID. Poll the canonical run endpoint no faster than every 15 seconds:

curl --fail-with-body \
  -H "Authorization: Bearer $CERTORA_API_KEY" \
  "$CERTORA_API_BASE_URL/v2/runs/$RUN_ID"

There is no separate v2 progress endpoint. Progress, billing, result availability, and generated-file delivery state are embedded in the run object.

During automatic context selection, an accepted run remains running; run.progress.phase may be _11_context_preparation. This is a planning phase, not a terminal status. The dashboard's separate preview flow uses milestones such as planning_context, with optional detail and attempt counts. Those preview milestones are not v2 run statuses. Keep polling the same run while planning is in progress; a long wait alone does not authorize another launch.

run.model_mode records the AI Auditor model mode. It is null for other engines and historical runs without a recorded mode; historical null values must not be relabeled as Normal. Guardian CI exposes the input as model-mode, supports full, diff, and finding-validation workflows, and keeps the field omitted when its input is left empty.

Canonical statuses are:

A succeeded run almost always carries a result, and result.available is then true. A run whose engine never published a readable result leaves finalizing for succeeded, with result.available set to false. The API checks for the result on your first read of the run, and then for up to an hour after the run settles. Read that field before you fetch the result.

Example response:

{
  "request_id": "9fb0634b-5353-4f3e-86ef-421a087e19c6",
  "run": {
    "id": "33333333-3333-4333-8333-333333333333",
    "run_type": "auto_prover",
    "model_mode": null,
    "status": "running",
    "source": {
      "repository_url": "https://github.com/acme/vault",
      "commit_sha": "0123456789abcdef0123456789abcdef01234567"
    },
    "client_reference": "pull-request-418",
    "progress": {
      "phase": "Generating CVL specs",
      "percent": 75,
      "completed_steps": 1,
      "total_steps": 2
    },
    "billing": {
      "status": "metering",
      "reserved_usd": "31.2500",
      "charged_usd": null
    },
    "result": { "available": false },
    "failure": null,
    "delivery": null,
    "cancellable": true,
    "created_at": "2026-08-13T10:00:00.000Z",
    "started_at": "2026-08-13T10:00:08.000Z",
    "completed_at": null,
    "dashboard_url": "https://app.certora.com/orgs/acme/run?report=33333333-3333-4333-8333-333333333333&reportApp=auto-prover"
  }
}

Timestamps are RFC 3339 strings or null. started_at records the first time this application observed provider execution; it stays null while queued and may remain null for a historical or fast-terminal run that was never observed running.

List and recover runs

GET /v2/runs supports cursor pagination and these optional filters:

• cursor: UUID returned as next_cursor
• limit: 1–100; defaults to 50
• status: one canonical status
• run_type: one supported v2 run type
• repository_url: exact repository URL
• commit_sha: exact 40-character commit SHA
• client_reference: exact caller-supplied reference

curl --fail-with-body \
  -H "Authorization: Bearer $CERTORA_API_KEY" \
  "$CERTORA_API_BASE_URL/v2/runs?status=running&run_type=auto_prover&limit=50"

Continue using next_cursor until it is null.

Retrieve results

After run.status is succeeded and run.result.available is true:

curl --fail-with-body \
  -H "Authorization: Bearer $CERTORA_API_KEY" \
  "$CERTORA_API_BASE_URL/v2/runs/$RUN_ID/result"

The response has a stable versioned envelope. Use result.run_type as the discriminator for result.data:

{
  "request_id": "9fb0634b-5353-4f3e-86ef-421a087e19c6",
  "result": {
    "schema_version": "1",
    "run_id": "33333333-3333-4333-8333-333333333333",
    "run_type": "ai_auditor_full",
    "data": {
      "report": {
        "format": "markdown",
        "content": "# Audit report\n\nNo critical findings."
      },
      "intermediate": null
    }
  }
}

AI Auditor reports use Markdown or JSON content. Finding validation omits intermediate. AutoProver and AutoFuzzer return a typed contract report. A run that is still settling returns 409 result_not_ready; failed and cancelled runs return 409 result_unavailable.

Retrieve artifacts

AutoProver and AutoFuzzer expose filtered, user-visible generated artifacts after success:

curl --fail-with-body \
  -H "Authorization: Bearer $CERTORA_API_KEY" \
  "$CERTORA_API_BASE_URL/v2/runs/$RUN_ID/artifacts?limit=100"

The response includes short-lived signed download_url values. Download those URLs directly without the service-key authorization header. Continue with next_cursor until it is null, even if a filtered page has an empty artifacts array. AI Auditor runs currently return an empty artifact list.

Cancel a run

Cancellation accepts an empty JSON object and is safe to repeat:

curl --fail-with-body \
  -X POST \
  -H "Authorization: Bearer $CERTORA_API_KEY" \
  -H "Content-Type: application/json" \
  --data '{}' \
  "$CERTORA_API_BASE_URL/v2/runs/$RUN_ID/cancel"

An already-terminal run is returned unchanged. 202 Accepted means cancellation was accepted or is still reconciling; continue polling until the run reaches a terminal status.

Commit generated files to a pull request

AutoProver and AutoFuzzer can commit generated files through the organization's GitHub App when the launch includes delivery.

Requirements:

• The run was bound to an open, same-repository pull request at launch
• The pull request head still matches the audited commit
• The organization GitHub App can read and write the repository
• The run has succeeded

curl --fail-with-body \
  -X POST \
  -H "Authorization: Bearer $CERTORA_API_KEY" \
  -H "Content-Type: application/json" \
  --data '{}' \
  "$CERTORA_API_BASE_URL/v2/runs/$RUN_ID/generated-files/commit"

The operation is idempotent. Its delivery status is committed when it created a commit and no_changes when the pull request already contained the generated content.

If GitHub received the generated commit before delivery status was saved, retry this endpoint for the same run. The server accepts only the exact generated child of the audited commit after checking its files, hashes, and modes. Guardian CI uses this recovery on the generated commit's follow-up run without launching another paid audit. Honor retryable responses and Retry-After while another delivery attempt holds the lease.

Errors and retries

HTTP request failures use their real HTTP status and an application/problem+json body. An accepted run that later fails is instead returned normally by GET /v2/runs/{run_id}, with run.status: "failed" and a run.failure object.

Auto Context failures expose only safe code, detail, and retryable fields:

Honor the returned retryable value rather than inferring it from the code. A retryable failed run is still terminal: replaying its launch key recovers that same failed run. Starting over requires an intentional new launch with a new key and a new balance reservation. Do not automatically create a new paid run. Historical or other failures may use run_failed; private planner state and budget ledgers are not part of the public response.

Example HTTP request failure:

{
  "type": "https://docs.certora.com/api/errors/validation_error",
  "title": "Unprocessable Content",
  "status": 422,
  "detail": "The request body is invalid.",
  "code": "validation_error",
  "request_id": "9fb0634b-5353-4f3e-86ef-421a087e19c6",
  "retryable": false,
  "field_errors": {
    "source.commit_sha": ["Must be a full 40-character commit SHA"]
  }
}

Branch on status and code, not the human-readable detail. Log request_id when contacting support. Validation failures include field_errors keyed by request-body path, query field, or header.

Retry only when retryable is true. Honor Retry-After on 429 and retryable 409 responses. For an ambiguous launch, retain the exact body and Idempotency-Key. Apply exponential backoff with jitter to transient failures.

Common statuses:

Unknown /api/* and /v2/* paths return JSON 404 endpoint_not_found, never a successful HTML page.

Rate limits

Public automation uses organization-scoped sliding-window buckets:

Downloading a returned signed artifact URL does not consume the API bucket.

Integration checklist

1. Create a least-privilege organization service key.
2. Call GET /v2/access and verify scopes, capabilities, GitHub App state, and balance.
3. Resolve branches or tags to immutable 40-character commit SHAs.
4. Build one strict request body. Prefer omitted or empty AI Auditor context; provide non-empty scope for a full audit. An estimate is optional and preliminary for automatic context.
5. For AutoProver or AutoFuzzer, retain the 15-minute estimate_quote_id.
6. Launch with a durable Idempotency-Key and the unchanged body. Preserve omitted context versus [], mode, and iteration options when retrying; do not turn an ambiguous launch into a new request.
7. Persist the returned run UUID and your client_reference.
8. Poll GET /v2/runs/{run_id} no faster than every 15 seconds.
9. Fetch results and artifacts only after success.
10. Honor problem details, retryable, and Retry-After.

The live OpenAPI 3.1 document is the source of truth for all strict schemas and response fields.