Prover Version 8.11.3
Announcing new CVL features, better diagnostics, and improvements for CI/CD
Author:
Shane RunquistThe 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.
The HTML generated for viewing “TAC dump” diagnostics received several improvements:
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.
Jaroslav Bendík, PhD
Yoav Elmalem
Johannes Späth, PhDgh-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.
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.