Prover Jobs, Mutation Reports and a Timeout Resolver API

What's New

Certora AutoProver 3.2.0 brings the Certora Prover into your dashboard. A new Prover Jobs page lists and manages your organization's Prover jobs, and a new Mutations page opens a coverage report for every mutation test. Prover jobs are now billed by the minute from your organization balance, with free monthly minutes for every member. A new Timeout Resolver API takes a rule that timed out in a finished Prover run and searches for a proof of it. AutoProver runs default to Prioritized mode, and the public API can now cap what an AutoProver run spends and how long it takes. Review reports carry AutoProver's own severity ratings, your team's triage status and your choice of logo. This release also brings a redesigned homepage and a long list of fixes.

Certora Prover

Prover Jobs

• All your Prover jobs in one place — The new Prover Jobs page in the organization menu lists the Prover jobs your organization has run. Filter and sort them, switch between active and archived jobs, choose which columns to show, and favorite, archive or cancel jobs one at a time or in bulk.
• Your own jobs first — The list opens on your own jobs, with a filter to show everyone in the organization or a single member.
• Stop a running job — A job in progress has a stop button next to its status, with a confirmation first, as on prover.certora.com.
• Durations you can trust — Finished jobs show how long they ran, and running jobs count up live from when they started, without the time spent waiting in the queue.
• Open reports quickly — The row you click shows a spinner until its report opens, and an "Open original report" button takes you to the full Prover report.

Mutations

• Mutation testing results — The new Mutations page lists every mutation test you can view. Each one opens a coverage report with summary statistics, a coverage chart, the rules and mutants, and the diff of each mutant.
• Accurate verdicts — A mutant that no rule caught, while some rules timed out or returned unknown, is shown as Inconclusive instead of Survived.
• Clear about access — Finished runs whose report you cannot open are not linked, and a tooltip explains why.

Pay for the Minutes You Use

• Billed by the minute — Certora Prover jobs are charged per minute of verification from your organization balance. A job sets aside its maximum before it starts and is charged only for the minutes it actually ran. A job that never starts costs nothing.
• Free monthly minutes — Every member has a monthly allowance of free minutes, and the organization has a shared monthly pool. A job uses whichever has less left, so one busy member cannot spend the whole organization's free minutes.
• Nothing stays on hold — If a job never reports back, the amount set aside for it is returned to your balance automatically after 24 hours.
• See your rate and allowance — The API page shows the current per-minute rate and your free minutes.

Timeout Resolver

• Resolve a rule that timed out — A new public API route, POST /v2/timeout-resolver-runs, sends one rule that timed out in a finished Certora Prover run to the Timeout Resolver. It searches for a proof of the property and returns a write-up of the proof with the lemmas it relies on.
• Start from the link you already have — Pass the run's report URL, including a shareable link, or the link to the job on your Prover Jobs page. Name the rule and describe the property it formalizes. Optionally, narrow a parametric rule to one contract or method, describe your application, and set a time budget.
• Follow it like any other run — Check progress, cancel, read the result and download the files through the same /v2/runs routes as your other runs. The downloads are the proof write-up, the source and specification patches, and the Lean lemma files.
• Runs from your organization — A key with run-creation permission can resolve runs owned by the member who created the key or by another member of the key's organization.
• Pay for what it uses — A fixed amount is set aside from your organization balance when the run starts. The run is charged for what it used and the rest is returned. A failed run is returned in full.
• API only for now — Timeout Resolver runs are launched and read through the API and do not appear in your dashboard history yet.

AutoProver

• Prioritized by default — New AutoProver runs use Prioritized mode, in the run form and in the API when no mode is given. Comprehensive remains available in Expert settings. When you choose it, the run overview recommends a higher maximum budget, because a Comprehensive run formalizes every candidate property.
• Cap cost and duration through the API — AutoProver runs launched through the public API accept optional limits: a maximum budget, a total time budget and a Prover timeout. Each is a ceiling, not a target. The maximum budget caps what the run sets aside and what the engine may spend on models. Compute time is billed on top, so the final charge can exceed it. AutoFuzzer runs accept the maximum budget too.
• Libraries can be the main contract — A Solidity file that contains only a library can now be selected and launched.
• Know which design document was used — The report, its markdown export and Create PR name the design document the run used, and say whether AutoProver found it in your repository or you uploaded it.
• Generated specs are back — AutoProver reports list the generated specifications and configuration files again, including verified ones grouped by component, and Create PR is available again on runs that produced them.
• Billing for runs cut short by their budget — A run that its time or model budget cut short is now charged when it still produced results, such as an encoding or drafted properties. A run that produced nothing is still fully refunded. Runs on several contracts are billed per contract: contracts that succeeded are charged, and a contract that failed is refunded.
• Spend limits are respected — AutoProver, AutoFuzzer and All in one runs now stop at the spend limit set for them.
• More reports open — Reports from AutoProver pipelines for languages other than Solidity no longer fail to open.

AI Auditor

• Clickable code locations — Findings in the report show their code locations as links, labeled with the file path and lines, so two files with the same name are easy to tell apart.
• Clearer checks before you start — The preview lists any problem with your configuration in one place. When a problem would stop the audit, such as a context pattern that matches no file, the Start button stays disabled until you fix it. Clearing your context selection returns the audit to automatic context.

Report

• AutoProver's own severity — Violated rules use the severity AutoProver rated them, instead of all starting at Medium. Each rated finding includes its impact, attack path, assumptions and proof of concept.
• Severity changes are disclosed — If you change a severity AutoProver assigned, the PDF says so and shows AutoProver's original rating and reasoning. The wizard marks the change and offers a Reset.
• Your triage in the PDF — AI Auditor findings you marked Valid or Acknowledged carry a status badge, and the findings summary adds a Status column. Findings marked Invalid stay out, as before.
• Your logo on the report — Choose a logo for the report by pasting a link, dragging a file in or uploading one. Without one, the report shows the repository owner's GitHub avatar in the page header and on the cover.
• Bookmarks that go to the right place — The PDF outline and the table of contents now jump to the section you click.
• Numbered lists — Numbered steps in findings start on their own line with their number.
• Smoother run picker — The run list in the Generate report wizard scrolls with the mouse wheel and on touch screens.

API

• Retries from CI no longer conflict — Retrying a launch with the same Idempotency-Key and a freshly minted CI token now returns the original run instead of a conflict error.
• Keys follow their creator — An API key stops working as soon as its creator leaves the organization it was created in. Existing keys whose creator could not be identified, including some older keys, were revoked. If a key stopped working, create a new one from the API page.
• A guide to creating keys — The documentation includes a step-by-step "Create an API Key" guide with screenshots.
• Roomier key dialog — The Generate API Key dialog gives its expiration and permission settings more space.

Billing

• Your company name on invoices — Checkout for plans, top-ups and Enterprise asks for your business name and billing address and accepts a tax ID, so your invoices carry your company's name.
• Enterprise credits each month — Externally billed Enterprise agreements add their commitment to your balance at acceptance and then on each monthly anniversary, until the full commitment has been credited.
• Confirm before ending Enterprise — "Cancel at term" now asks for confirmation, states the term end date, and reminds you that the cancellation can be undone until then.
• Accurate Enterprise details — The Enterprise discount is shown only while the agreement is active, and plan details show the next payment and the term end date correctly when a cancellation is scheduled.
• More reliable Enterprise billing — Payments made with Stripe credit or a credit note count toward the commitment, and agreements ended in Stripe end in the app right away.

Other

Improvements

• A new homepage — The Certora AutoProver homepage has been redesigned, with an interactive hero and animated walkthroughs from intent to specification to proof. Visitors who prefer reduced motion get a static page.
• Back where you left off — Signing in or opening the dashboard takes you to the organization you last worked in, instead of the one with the largest plan or balance.
• Organizations stay put — Fixed an issue where organizations and their runs could briefly disappear and reappear after AutoProver or AutoFuzzer runs.
• Security and reliability were improved, and bugs were patched.