Breaking Changes in This Release

Important: This release introduces breaking changes that may require updates to your specs, configs, or workflows. Please review the changes below before upgrading.

Minimum Java Version Increased to 19

What changed:

The Certora Prover now requires Java Runtime Environment (JRE) version 19 or higher.

Impact:

If you use an older JRE (18 or below), the Prover will fail to start.

Action needed:

Update your Java installation to version 19 or later before running the new release.

Java installation instructions

Minimum Python Version Increased to 3.9

What changed:

Python 3.8 has reached end-of-life, and certora-cli will no longer explicitly support this version.

Impact:

If you're using Python 3.8, you may encounter compatibility issues or installation errors when using newer versions of certora-cli.

Action needed:

Upgrade your Python installation to version 3.9 or higher.

Python installation instructions

Sanity Checks Now Run by Default (Including Invariant Base Cases)

What changed:

The Prover now runs basic sanity checks by default, including checks for vacuity and trivial conditions. This change is equivalent to setting “rule_sanity”: “basic” in earlier versions.

As part of this update, we fixed a bug: the vacuity check for the base case of invariants is now properly executed. Previously, this check was silently skipped.

Impact:

Jobs may take slightly longer to run, and some rules that previously passed may now fail due to failing a sanity check. This ensures the rules are meaningful and not trivial or vacuously satisfied.

Action needed:

Review your rules and check the Rule Notification tab if you encounter new violations. We explain sanity check failures in more detail in the documentation.

Docs

New Semantics for requireInvariant

What changed:

The semantics of requireInvariant have been updated to fix an unsoundness issue. Previously, it was treated as a shortcut for require(<invariant expression>), which could incorrectly assume that the invariant holds at arbitrary points, even when that wasn’t guaranteed.

With this release, requireInvariant only assumes the invariant before a rule starts, where its truth is proven.

Impact:

This change makes invariant assumptions sound by default. If your spec relied on the old behavior, you may now see new failures or changes in results.

Action needed:

Review uses of requireInvariant and ensure it appears only where the invariant should hold before the rule begins.

Docs

Example

Solana and Soroban Verifications Must Use Dedicated Commands

What changed:

Running Solana and Soroban jobs using certoraRun is no longer supported. These targets now require their dedicated CLI entry points:

• Use certoraSolanaProver for Solana jobs
• Use certoraSorobanProver for Soroban jobs

Impact:

Attempts to run Solana or Soroban contracts using certoraRun will now result in an error.

Action needed:

Update your workflows and scripts to use the appropriate command for Solana or Soroban verification.

Default Report Links Are Now Private

What changed:

By default, all newly generated verification report links are now private, meaning they are only accessible to you. In continuous integration (CI) runs, report links will continue to be public by default to avoid breaking existing workflows.

The Verification Report UI has been updated with a dropdown menu next to the Share Link button. This menu lets you:

• Copy a private or public link
• Optionally preserve the current report view state (e.g., open tabs, scroll position, highlighted lines) when copying the link

A new url_visibility option lets you control the link type when running jobs, either via the command line or in a configuration file.

Impact:

If your current workflow relies on public links, you will now need to explicitly set url_visibility public to preserve the old behavior.

Action needed:

Update your configs or CLI commands if public links are required for your use case.

Docs

Revert Handling for CVL Functions

What changed:

CVL functions now support explicit revert behavior:

• Use the revert keyword within CVL functions to model failure scenarios.
• CVL functions can now be called with the @withrevert postfix to reason about both success and revert cases.

Impact:

Previously, the Prover did not reason about CVL functions reverting, even when used to summarize Solidity functions called with @withrevert. This led to incorrect verification results, as possible reverts in the CVL summary were silently ignored.

With this update, the Prover checks whether a CVL function may revert, and rules that previously passed may now fail due to missing revert modeling.

Action needed:

If you call a Solidity function with @withrevert and summarize it with a CVL function, make sure the CVL function properly accounts for both success and failure paths. Use the revert keyword as needed to accurately capture revert conditions.

Docs

Example

Deprecated CLI Options Removed

What changed:

Several CLI options that previously printed warnings are no longer supported. These options were gradually phased out and, in most cases, replaced by newer alternatives. If you encounter errors after upgrading, check your config files or scripts for unsupported flags and replace them accordingly.

You can find the full list of supported CLI options in the docs.

Docs

adaptiveSolverConfig false Replaced by backendStrategy singlerace

What changed:

The Prover no longer accepts the -adaptiveSolverConfig false option as a prover_arg. It has been replaced by a new option: -backendStrategy singlerace.

Impact:

Using the old option will now result in an error.

Action needed:

Update your configuration file prover_args to use -backendStrategy singlerace instead.

New Prover Updates

CVL Specification Formatter

A new command-line tool is now available to format CVL specification files. You can run it from the terminal with:

certoraCVLFormatter <SPEC_FILE> --overwrite

This automatically reformats your CVL code for consistency and readability.

The formatter is also available as a VSCode extension.

Docs

Re-Routing Summaries

You can now summarize internal functions that take storage parameters by rerouting the call to a custom Solidity function. This unlocks new use cases where expression summaries weren’t previously possible.

Docs

Example

Transient Storage Hooks

CVL now supports hooks on transient storage fields, enabling precise reasoning about reads (TLOAD) and writes (TSTORE). You can define hooks with named storage variables for these opcodes and access the corresponding fields directly in CVL, just like regular storage fields.

Note: ALLTSTORE and ALLTLOAD hooks are only supported when storage splitting is disabled, which is consistent with regular storage hook behavior.

Docs

Example

Foundry Remappings Support

You can now use Foundry’s built-in remapping resolution when compiling contracts. The Prover automatically runs forge remappings to collect all package mappings defined in your foundry.toml and its dependencies. This feature is active when packages is not explicitly provided, allowing for simpler setups and better compatibility with Foundry-based projects.

Docs

Example

Upgrade to Version 8.1.0

Access these updates by ensuring your software is up-to-date with the latest version. To upgrade to v8.1.0, simply run pip install --upgrade certora-cli.

As always, we welcome and appreciate your feedback.