New Prover Update

Improved Invariant Base Case Expressiveness

This release includes a change to the modeling of invariant base cases, allowing it to cover more deployment situations. Previously, the storage of all contracts in the scene was assumed to be zeroed, corresponding to freshly deploying the whole scene. Now, only the storage of the currentContract is zeroed, all other contracts are assumed to be in arbitrary states.

To express assumptions about the deployment scenario, the preserved constructor block can be used. It is applied on the invariant base case and now allows making assumptions about the state of other contracts in the scene. 

Note that this change may require adjusting CVL specs to add such assumptions. As the scenario checked by default is now more general than before, previously verified specs may show new counterexamples.

The previous behavior can be retained via a new prover_args flag -allContractsZeroedForInvariantBaseCase true if desired.

Upgrade to Version 8.6.3

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

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