Automatic Context, Frontier Mode, and Audits That Report Inside GitHub

What's New

Certora AutoProver 3.1.0 brings automatic audit context to the dashboard, public API, GitHub Action, and Codex and Claude Code plugins. Choose what to review, and AI Auditor selects the supporting source and dependencies for you. Audits launched from CI now report back inside GitHub on their own — a pull-request check that waits for the real outcome, a summary comment, and an issue per finding. Alongside that, AI Auditor gains a Frontier model mode, AI Auditor gets 10% cheaper, AutoProver gains a shorter Prioritized run mode, one repository can run several CI configurations side by side, design documents can be uploaded instead of committed, dashboard launches can carry a spending ceiling you set yourself, and runs that stop early now hand back the work they finished.

AI Auditor

Context Chosen For You

• Pick scope, not context — The run form now asks only which files you want reviewed. AI Auditor selects enough of the repository around them to analyze that scope, so you no longer have to guess which supporting files the model needs.
• Watch it come together — Dashboard preview reports each step as it happens: loading the repository and its submodules, selecting context and planning the run, then calculating your estimate.
• Get told when it is ready — Dashboard preparation on a large repository can take a few minutes. Opt in to a browser notification and step away; you are told the moment your context and estimate are ready. Nothing is launched or billed while you wait for this preview.
• Prepared once, reused for a week — Dashboard previews keep a prepared configuration for your organization, so returning to the same commit and settings prices and launches quickly instead of starting over.
• Adjust the selection before you launch — Edit context in the preview dialog to add or remove files from the automatic selection, and the estimate updates to match what you kept.
• Manual context is still there — Explicit context, design, and threat-model overrides moved into expert settings for anyone who wants to drive the selection by hand.

Automatic Context in Your Tools

• Launch in one step — Public API, GitHub Action, and Codex and Claude Code plugin launches can now leave context empty. AI Auditor selects supporting code and runs the audit from the same launch request, without a separate preview.
• You still choose what gets reviewed — Full audits require your chosen scope. Diff audits use the complete set of changes, and finding checks use the finding you provide. Supplying context explicitly remains available when you want to control the supporting files yourself.
• Simpler GitHub setup — Automatic context is now the highly recommended default in the GitHub Action installer. Manual selection is available under expert settings; hiding the override returns to automatic selection.
• Balance checked before work starts — Integration launches automatically check a preliminary estimate and reserve balance before selecting context and auditing. You can still request an estimate separately, but it is not a required step or a guaranteed final price.

Normal and Frontier Modes

• Choose the model lineup — AI Auditor runs can be launched in Normal mode or Frontier mode. Preview prices the mode you selected, so you see what each one costs before committing.
• Normal mode — Claude Opus 5, GPT 5.6 Sol, and Kimi K3 review your code together, supported by GPT 5.6 Luna. This is the default and covers the large majority of audits.
• Frontier mode — Swaps the two lead reviewers for the newest frontier models, Claude Fable 5.1 and GPT 6 Astra, keeping Kimi K3 and GPT 5.6 Luna alongside them. Use it on the code where the last increment of depth is worth the higher price.
• Normal mode is 10% cheaper — Technical optimizations to how a run is executed cut the cost of every Normal-mode audit by 10%. The reduction is already reflected in the estimates you are quoted; nothing to opt into.
• Available everywhere you launch — The mode can be set in the dashboard, in the workflow the GitHub Action installer generates, and through the public API. Runs record the mode they used, and it appears in your history and on the report.
• The estimate keeps up — Switching modes inside preview re-prices without losing your place: the prepared files stay on screen and the panel keeps its size while the new estimate loads.

Audits That Report Inside GitHub

• A check that waits for the real result — AI Auditor audits launched from CI now publish their own Security Review check on the pull request. The workflow job turning green only means the audit was accepted; the check stays pending until the audit truly finishes and then reports the outcome, so it is the one worth requiring in branch protection or a repository ruleset.
• Fail on the severities you choose — Decide which severities should block a merge. Everything else is reported without standing in the way.
• A summary on the pull request — Findings are posted as a comment on the pull request, and a report that could only cover part of the code says so plainly rather than reading as a clean result.
• An issue per finding — Findings at the severities you pick can be opened as labeled GitHub issues, so they land in your backlog instead of living only in the dashboard.
• Your runner is freed immediately — CI audits hand off to the service instead of holding a GitHub Actions runner open for the length of the audit.
• Diffs pinned at launch — Diff workflows pin the current target-branch and pull-request commits before launching and decline outdated events, so a rerun cannot quietly start a second paid audit against a base that has moved.
• Same-repository pull requests — This delivery covers pull requests raised from a branch of the audited repository. Pull requests from forks are declined during preflight, before any balance is reserved or paid work starts.
• Tune depth and model in the installer — Set the number of DeepDive iterations, from 2 to 10, and the model mode while generating the workflow, instead of editing the file afterwards.

A Better Run Form

• Preparation you can follow — Preview now fills a progress bar as preparation advances, instead of leaving you with an open-ended spinner.
• Instructions before expert settings — The run form now places Instructions above Expert settings on every audit type, with repository memory and the manual overrides tucked inside expert settings.
• Failures that say what to change — When context cannot be selected — a diff too large to process, a preparation timeout, a configuration that cannot be used — the preview names the problem, confirms no audit was started or billed, and tells you whether retrying will help or a setting needs to change.
• Repository memory stops re-preparing — A preview using repository memory now reuses the work it has already prepared instead of starting the preparation over each time it refreshes.

AutoProver

Shorter Runs with Prioritized Mode

• Prioritized run mode — AutoProver can formalize only the top-ranked property and the cluster of properties supporting it, instead of every candidate property. It is the shorter, cheaper pass for when full coverage is not what you are after.
• Comprehensive stays the default — Nothing changes unless you choose Prioritized under expert settings, and a retried run keeps the mode it was launched with.
• Suggested where the money is — The confirmation screen points out Prioritized while a run is still set to formalize everything, since it is the one choice on that screen that lowers the price rather than capping it.
• Available from the API — Run mode can be set on public API launches as well as in the dashboard.

Design Documents From Anywhere

• Upload instead of committing — AutoProver and AutoFuzzer runs can now take a design document or threat model as an upload. Documentation that lives outside the codebase — an exported PDF, a write-up that was never committed — no longer has to be added to the repository first.
• Repository or upload, per document — Both sources stay available and each document uses one of them. A run that cannot use the document you gave it stops and says so, rather than proceeding as though you had supplied nothing.
• Kept for your next run — Uploads are stored for your organization, so retrying a run does not mean uploading the document again.

Control What a Run Can Spend

• Set your own ceiling — The confirmation step now includes an editable maximum budget, pre-filled with the standard hold. Raise it for a run you want to let go further, or hold it close to the estimate to cap your exposure.
• Checked before you start — The budget is validated against both the quoted estimate and your balance, so an unusable figure is caught at confirmation rather than mid-run.

Reports and Pull Requests

• See partial results — When an AutoProver or AutoFuzzer run is curtailed before it finishes, the report offers the artifacts it produced beforehand, clearly labeled as drafted and unverified.
• Know what was cut — Reports name the components that were curtailed and the reason, and say plainly when something was never attempted.
• Readable in light mode — Code in AutoProver and AutoFuzzer reports is now correctly colorized in both light and dark themes.
• Cleaner pull requests — The ignore rules an AutoProver pull request adds to a repository now list only the one directory a run actually creates, leaving repositories that already ignore Certora output untouched.

Other

One Repository, Several CI Configurations

• Run engines and contracts side by side — The GitHub Action installer now creates one workflow per configuration, so the same repository can run an AI Auditor review, AutoProver on one contract, AutoProver on another, and AutoFuzzer on a third at the same time. Choose Add another configuration after a setup pull request to add the next one without replacing what is already there.
• Name a configuration to keep several — Give a configuration a name to run more than one setup for the same engine and contract, such as vault-properties and vault-invariants. Reusing a name updates that configuration; a new name creates another one. Configurations cannot cancel or overwrite each other's runs.
• No more empty setup pull requests — Reinstalling a workflow that is already up to date now tells you there is nothing to merge, and an open setup pull request is refreshed instead of duplicated.
• Connect only what you own — The installation picker now lists only GitHub installations whose account ownership was verified, so a connection cannot be bound by someone without the authority to grant it.
• Clearer finish line — The confirmation screen links straight to the repository secret settings for your CERTORA_API_KEY and to your organization's API keys page, and remembers exactly which repository and engine you set up.

A Consistent Preview

• The same layout for every engine — Preview presents each run the same way: the repository and the exact commit it is pinned to, the pipeline it will follow, its inputs, the scope and context patterns side by side, the files in context, the estimated price, the hold, and your current balance.
• Long selections scroll — Large pattern and file lists stay inside their own scrolling area instead of pushing the price and the start button out of reach.
• Your settings survive a refresh — Reopen the run form and your previous preview settings are restored, ready to reconnect.
• Repository addresses checked as you type — A mistyped or unsupported repository URL is caught immediately, with a message that says what is wrong.

Documentation and History

• A documentation home, not just a manual — The docs site is now Certora Documentation, covering the products alongside a complete REST API reference for the v2 Runs API, including authentication, every endpoint, and error formats.
• Find a run by its ID — Dashboard history search now matches a run's UUID as well as a repository name or URL.
• Current product names throughout — The last places still showing older product names — report authors, assistant tools, notifications — now read AI Auditor and AutoProver.

Reliability & Security Fixes

• Every support reply reaches you — Replies from support are no longer batched behind a delay; you are emailed each time someone answers you.
• Failures reach us without you reporting them — Failed runs are now raised for investigation automatically, so problems are picked up and resolved faster.
• Revoking an API key is immediate — Revocation now takes effect and confirms straight away instead of leaving the page waiting.
• Pages open sooner — Account pages and the organization not-found page now appear immediately rather than waiting on a lookup first.
• Security and reliability were improved across launching, billing, integrations, and reporting, and bugs were patched.