Solidity

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 Sstore Hooks with Storage Mappings Introduction In the chapter “Introduction to Storage Hooks And Ghosts”, we covered storage hooks and ghosts with simple storage variables. We showed that...

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

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

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

Mint and Burn Rules for ERC-721 Introduction ERC-721 is the Ethereum standard for non-fungible tokens, widely used to represent digital property. Like any form of property, it revolves around supply...

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