Browse all Solidity articles.
14 min read
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...
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...
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...
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...
15 min read
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...
10 min read
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...
10 min read
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
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...
8 min read
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...
7 min read
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...
10 min read
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...