A New Model Lineup for AI Auditor, at a Lower Price

What's New

Certora AutoProver 3.1.1 moves AI Auditor to a newer generation of models in both Normal and Frontier modes, and lowers the price of running them. Claude Opus 5.5 now leads every audit, joined by the GPT 6 family, with Kimi K3 still reviewing alongside. This release also warns you before a CI configuration is set up on a branch where it can never run, shows GitHub token guidance as soon as you mark a repository private, and keeps the support chat from getting in your way.

AI Auditor

A New Model Lineup

• Normal mode — Claude Opus 5.5, GPT 6 Sol, and Kimi K3 review your code together, supported by GPT 6 Luna for the lighter, high-volume steps of a run. Normal remains the default and covers the large majority of audits.
• Frontier mode — Claude Opus 5.5 and GPT 6 Astra lead the review, with Kimi K3 and GPT 6 Luna alongside them. GPT 6 Astra is the deeper-reasoning lead that sets Frontier apart; use it on the code where the last increment of depth is worth the higher price.
• Smarter automatic context — The step that selects supporting source and dependencies for your chosen scope now runs on GPT 6 Sol.
• Nothing to change on your side — The new lineup applies automatically to runs launched from the dashboard, the GitHub Action, the public API, and the Codex and Claude Code plugins. Choosing a mode works exactly as before.

Lower Audit Prices

• Cheaper in both modes — The new models cost less to run, and that reduction is passed through to your estimates. For a larger 300k-token audit, the projected API-price reductions are ~44% in Normal mode and ~25% in Frontier mode.
• Better use of caching — Repeated context within a run is now priced at cached rates across the lineup, which is a large part of the saving on bigger audits.
• Your quote reflects it — Preview prices the new lineup, so the estimate you see before launching already includes the reduction. Actual savings will vary with token use, caching, and retries.
• Legacy runs are labeled correctly — Audits launched before model modes existed now show as Normal mode in your history instead of carrying no label.

Other

GitHub Action Setup

• Branches that would never run are flagged — Selecting a target branch other than your repository's default branch now shows a warning right away. The setup pull request is opened against the default branch, so a branch that never receives it would never see the workflow. The setup pull request also names each affected branch and the step needed to make it run there.

Improvements

• Token guidance from the start — Turning on "Private repository" in the run form now shows how to create a GitHub token immediately, instead of waiting until a repository URL has been entered.
• The support chat steps aside — The floating support chat button now turns faint and lets clicks pass through when it would cover a control on the page, so it never blocks what you are trying to click, and returns to full strength once the way is clear.
• Security and reliability were improved, and bugs were patched.