The technical content top engineers rely on to level up.
17 min read
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,...
9 min read
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...
12 min read
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...
13 min read
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...
12 min read
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,...
9 min read
Persistent Ghosts Introduction In previous chapters, we used ghost variables (via hooks) to record storage values and quantities that were not explicitly tracked in smart contracts — for example, the...
10 min read
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...
8 min read
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...
17 min read
Loops in CVL: Path Explosion and Loop Unrolling Loops are one of the most common programming constructs, but they remain challenging to reason about in formal verification. While a loop in Solidity...
8 min read
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...
7 min read
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...
14 min read
Invariants for ERC-721 Introduction In previous chapters, we explored how CVL invariants work: properties that must hold throughout all contract execution. Invariants can function as preconditions in...