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

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

Transfer and Approval Rules for ERC-721 Introduction This chapter continues as the third part (3/5) of our code walkthrough of OpenZeppelin’s ERC-721 CVL specification and focuses on token transfer...

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

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

Introduction to Invariants in Certora Up until now, we’ve focused on verifying the behavior of individual methods or sequences of methods — ensuring that a specific function call or set of calls,...

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

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

Formally Verify Solady WETH Introduction ETH, widely used in DeFi for swaps, liquidity provision, staking, and collateral, needs an ERC-20-compatible version so protocols can interact with it through...

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