Conditional Statements in CVL and Formally Verifying Parts of Solady and Solmate Introduction Some contract behaviors (properties) are inherently conditional, and using constructs like if/else in CVL...

Overflow and Mathint In CVL, the type represents unbounded integers, unlike Solidity’s fixed-size types such as . It performs arithmetic without overflow or underflow, which allows reasoning based on...

Introduction to Method Properties Introduction In the previous chapter, we learned about parametric rules, which allow us to formally verify properties that are expected to hold regardless of which...

Formally verifying Initializable.sol This article describes how Certora formally verified the Initializable.sol OpenZeppelin contract. We assume the reader is already familiar with how this contract...

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 msg.sender and msg.value in CVL Introduction In this chapter, we introduce the variable in CVL, which enables us to make rules for functions that depend on , , and other global variables in...

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...

Biconditional Operator Introduction The biconditional operator enables us to assert if-and-only-if relationships between boolean values. Implication () states that if condition P is satisfied, then Q...

Introduction to Parametric Rules Until now, in previous chapters, we have written rules to verify the behavior of specific methods and their impact on a contract’s state. For example: In Chapter 2,...

Implication Operator Introduction The implication operator is frequently used as a substitute for the statement since it is cleaner. Consider the following example: a function that takes two unsigned...

Formally Verifying Nonces.Sol in OpenZeppelin Nonces, which stands for "number used once" are used in digital signature schemes to prevent replay attacks. For the purposes of this article, we assume...

Formally Verifying Address Balance In the previous chapter, we covered how to reason about environment-dependent functions in CVL by focusing on in non-payable contexts. In those examples, access...