New Prover Updates

Added CVL "links" Block

The new links block in CVL lets you declaratively bind contract storage variables to target contracts directly in your spec, providing a preferred alternative to the .conf file's link and struct_link fields. It supports field access, array and mapping indices (with numeric literals, to_bytesX, or contract aliases), wildcards, struct traversal, and multiple link targets per slot. All paths are fully type checked against the contract's storage layout, catching errors like unknown fields, type mismatches, and out-of-bounds indices on static arrays at compile time.

Docs

Examples

TAC Dump Improved

The HTML generated for viewing “TAC dump” diagnostics received several improvements:

• Added support for the browser’s back & forward buttons.
• When clicking on a variable, its input and output variables are also highlighted to make finding them easier.
• Added a new “Dataflow” view. In this view one can track the flow of data through a graph of variables.

Docs

Improved Semantics for "requireInvariant" with Strong Invariants

When a rule or invariant uses a requireInvariant command with a strong invariant, the invariant is re-assumed after any HAVOC in the rule/invariant. This can reduce false counterexamples after external calls due to violated (strong) invariants.

Changes to Our Github App

New Review Comment Features

• gh-review - This indicates when to add a review comment to the PR. The options are always, failure, and never. The default is always.
• gh-review-jobs - This indicates which jobs to include in the GitHub review comment. Options are all or failed. The default is all.

If gh-review is never, the status link points to a summary page like this. This link only works for public repositories; private repositories still point to the Prover job page. We also added a new extensive Troubleshooting section to the documentation.

Upgrade to Version 8.11.3

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

As always, support is available on our Discord server. We welcome and appreciate your feedback.