New Prover Updates

New Builtin Rules:

uncheckedOverflows

A new builtin rule, uncheckedOverflows, is available. It checks whether arithmetic operations can overflow or underflow in unchecked code. The analysis is done for each external method and each unchecked operation that is reachable from the method call.

Docs

safeCasting

A new builtin rule, safeCasting, has been added that checks whether any Solidity casting operator can be out of bounds (e.g., whether in uint16(x) , is it possible for x to be larger than 2^16-1). Analysis is done for each external method and each casting operation that is reachable from the method call.

Docs

Method Filtering With Name Only

The --method and --exclude_method flags now allow providing only the method name (without any parameter types) for EVM. If there are several overloads for this function name, all of them will be matched.

Docs

Example

New Config Option: --assume_no_casting_overflow

Newly added flag, --assume_no_casting_overflow, assumes no casting operations in Solidity are out of bounds. For example, if int16(x) is in the Solidity code, then x is assumed to be in the valid range of an int16 when this flag is used. Note that this is an underapproximation, as Solidity does not revert on such out-of-bounds values.

Docs

Changes to Our Github App

Enhancements for Continuous Integration / Development

• The GitHub action now replaces active reviews within the same configurations.
• Added GitHub Actions API support for cancelling jobs and refreshing job status. (This will require adding an additional workflow as described here.)
• Added Solana, Sui, Soroban and Vyper support.
• Improved error logging.

Upgrade to Version 8.8.0

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

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