Formally Verify an ERC-20 Token Introduction In this chapter, we formally verify Solmate’s ERC-20 implementation, which includes the following: Standard state-changing functions: , , Standard view...

Constraining Ghosts in Invariants In the previous chapter, we saw how unconstrained ghost variables can lead to false positives. We also learned how a statement can be used to effectively constrain...

Constraining the Ghost Values in Rules In the previous chapter, we learned how ghost variables allow information to flow from hooks into rules. We also learned that: At the start of the verification...

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

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

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

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

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

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

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

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