Verifying an Invariant Using Ghost and Hook In any correct ERC20 implementation, the sum of all account balances must always equal the total token supply. This property should always remain true...

Formally Verifying a Counter In the previous chapter, we learned the theoretical side of formal verification, including what it is and how it works. In this module, we’ll move beyond theory and learn...

Testing Revert Call In Certora In this chapter, we will learn how to use method tags ( and ) and the special variable in CVL to verify expected reverts in smart contract execution. Setting Up...

Understanding the Spec File in Certora CVL In the last chapter, we saw that to perform formal verification using Certora Prover, we need to provide the Prover with the following key items: Smart...

Introduction to Storage Hooks and Ghosts It often becomes necessary to inspect changes at specific storage locations to prove that a property or invariant holds, especially when the storage is not...

Using Sload Hooks with Storage Mappings Introduction In the previous chapter, we demonstrated that hooks are necessary to verify properties involving changes in mapping values. The hook monitors...

SafeMint and SafeTransfer Rules in ERC-721 Introduction This chapter is the fourth part (4/5) of our code walkthrough of OpenZeppelin’s ERC-721 CVL specification and focuses on formally verifying...

Using “requireInvariant" in Rules and Invariants Up until now, we’ve either written a rule to verify specific behaviors or an invariant to verify properties that must always hold true throughout the...

Certora Require, Assert, and Satisfy In the previous chapter, we learned that a specification is a piece of code written in CVL that describes the expected behavior of a smart contract. A...

Preserved Block and Its Role in Invariant Verification An invariant is a property that must always hold true after a smart contract is deployed and throughout its execution. At first glance,...