Introducing the Certora Sui Prover

The new certoraSuiProver command brings formal verification to Sui smart contracts. It uses CVLM (Certora Verification Language for Move), which is embedded in Move, unlike CVL for Solidity. See our documentation for detailed examples on compiling and running the Certora Sui Prover.

Docs

New Prover Updates

CVL Formatter Improvements

This release includes several improvements to our formatting engine, ensuring more consistent and predictable results across your workflows. It resolves issues related to unintended line breaks, overly aggressive empty-line removal, and unnecessary changes to existing parentheses in expressions.

Docs

Constructor Preserved Blocks For Invariants

We introduce a new kind of preserved block for the base step of invariants. For example:

preserved constructor() with (env e) {
    require e.block.timestamp != 0;
}

This allows stating assumptions before the constructor code is executed when checking the base step of an invariant. 

Docs

Upgrade to Version 8.5.1

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

As always, we welcome and appreciate your feedback.