Solidity

Loops are one of the most common programming constructs, but they remain challenging to reason about in formal verification.

This chapter is the final part (5/5) of the code walkthrough of OpenZeppelin’s ERC-721 CVL specification which formally verifies the following rules.

In previous chapters, we explored how CVL invariants work: properties that must hold throughout all contract execution.

In the previous chapter, we demonstrated that Sstore hooks are necessary to verify properties involving changes in mapping values.

In the previous chapter, we learned how ghost variables allow information to flow from hooks into rules.

An invariant is a property that must always hold true after a smart contract is deployed and throughout its execution.

It often becomes necessary to inspect changes at specific storage locations to prove that a property or invariant holds, especially when the storage is…

In the previous chapter, we saw how unconstrained ghost variables can lead to false positives.

Until now, in previous chapters, we have written rules to verify the behavior of specific methods and their impact on a contract’s state.

The implication operator is frequently used as a substitute for the if statement since it is cleaner.

The biconditional operator enables us to assert if-and-only-if relationships between boolean values.

In this chapter, we will learn how to use method tags (@withrevert and @norevert) and the special variable lastReverted in CVL to verify expected reverts…