Review Reports You Can Share and Verify

What's New

Certora AutoProver 3.1.2 introduces Report. Turn completed AI Auditor, AutoFuzzer and AutoProver runs of one repository into a single Certora-branded "Review of" PDF, preview it in your browser, share it with a link you control, and let anyone confirm that a copy is genuine. AI Auditor moves Normal mode and automatic context selection to GPT 6.1 Sol, and large or long-running audits are more reliable. Successful AutoProver and AutoFuzzer runs no longer wait at "Billing pending".

Report

One PDF Across Engines

• Combine the runs you already have — Pick up to one completed AI Auditor, AutoFuzzer and AutoProver run of the same repository, and Report turns them into one "Review of <repository>" PDF. Nothing new needs to be launched.
• Review findings before you generate — A three-step wizard shows every finding in one list. AI Auditor findings keep the severity you triaged, and findings you marked invalid stay out. Give each AutoFuzzer and AutoProver violated property a severity, Medium by default, or leave it out.
• Runs on different commits — Selected runs do not have to share a commit. The wizard warns you, and the PDF shows the commit each engine ran on.
• One findings list, one results section per engine — Findings from every engine are sorted by severity and labeled with the engine that reported them, followed by a results section for each engine you selected. Engines you did not select are never mentioned.
• Still produced when one engine is missing — If one engine's results cannot be loaded, its section is left out and the rest of the report is generated, with a warning in your history.
• Keep reports current — Regenerate after triaging findings, or change the runs and severities and generate again. Each generation gets a new version number. Any member can archive a report, and organization admins and owners can delete one after confirming.

Preview and Share

• Preview in the browser — Open a generated report without downloading it first.
• Share a link instead of a file — Create a link to a report for anyone outside your organization, with an optional password of at least 8 characters.
• Stay in control of the link — Turn a link off at any time, or regenerate it so the previous address stops working immediately.
• A clear page for recipients — People you share with read the report in their browser, are asked for the password when one is set, and are told plainly when a link has been turned off.

Verify a Report

• Check that a PDF is genuine — Drop a PDF on the Report page to confirm it is an exact, unmodified copy of a report generated by Certora, and see the date it was issued.
• Changed copies do not pass — A PDF that was edited, or generated before verification was available, is reported as unable to be authenticated rather than verified.

Clearer PDFs

• Jump straight to a finding — Each entry in the findings summary links to the finding it describes.
• Formulas that render — Mathematical operators, arrows, Greek letters and subscripts in findings now appear correctly instead of turning into question marks.
• Long names stay readable — Long file paths and identifiers wrap cleanly instead of running off the page, and page headers and footers keep long repository names and titles tidy.
• Updated About section — The About Certora section at the end of every report has been refreshed.

AI Auditor

GPT 6.1 Sol in Normal Mode

• A newer reviewer — GPT 6.1 Sol replaces GPT 6 Sol in Normal mode, reviewing alongside Claude Opus 5.5 and Kimi K3, with GPT 6 Luna supporting the lighter steps of a run.
• Smarter automatic context — The step that selects supporting source and dependencies for your chosen scope now runs on GPT 6.1 Sol in both Normal and Frontier modes.
• Same price, cheaper repeated context — GPT 6.1 Sol costs the same per token as GPT 6 Sol, and context repeated within a run is priced at a lower cached rate. Your estimate reflects this automatically.
• Nothing to change on your side — The update applies to runs launched from the dashboard, the GitHub Action, the public API, and the Codex and Claude Code plugins.

More Reliable Audits

• Large repositories stay within model limits — Planning now sizes each part of an audit for how the models actually count tokens, so very large codebases are split into more focused parts instead of failing late in the review. Estimates for these audits include the extra parts.
• Long audits ride out provider hiccups — A brief outage at a model provider no longer ends an audit that has been running for hours. The review waits it out and keeps the work it has already finished.
• Diff audits start as approved — Diff audits prepared in the dashboard without additional instructions now launch with their approved preview instead of stopping at the first step.

Other

Improvements

• Billing settles on time — Successful AutoProver and AutoFuzzer runs are billed as soon as they finish instead of staying at "Billing pending".
• Smoother navigation — Moving between pages from the sidebar is smoother, and Report and Memory show a loading placeholder while they open.
• A guide for Report — The documentation now includes a Report guide covering how to generate, update and archive reports.
• Security and reliability were improved, and bugs were patched.