Blog
The technical content top engineers rely on to level up.
9 min read
Persistent Ghosts
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...
14 min read
Invariants for ERC-721
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...
8 min read
Constraining the Ghost Values in Rules
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...
12 min read
Partially Parametric Rules for ERC-721
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...
8 min read
Transfer and Approval Rules for ERC-721
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...
17 min read
Preserved Block and Its Role in Invariant Verification
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,...
13 min read
Using “requireInvariant" in Rules and Invariants
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...
10 min read
Mint and Burn Rules for ERC-721
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...
5 min read
Testing msg.sender and msg.value in CVL
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...
8 min read
Introduction to Method Properties
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...
10 min read
Introduction to Formal Verification
Introduction to Formal Verification Formal verification is the process of mathematically proving a program adheres to a specification. This article introduces conceptually how formal verification...
7 min read
Understanding the Spec File in Certora CVL
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...