Solidity
Browse all Solidity articles.
6 min read
Formally Verifying Address Balance
In the previous chapter, we covered how to reason about environment-dependent functions in CVL by focusing on msg.sender in non-payable contexts.
4 min read
Formally verifying Initializable.sol
This article describes how Certora formally verified the Initializable.sol OpenZeppelin contract.
8 min read
Introduction to Parametric Rules
Until now, in previous chapters, we have written rules to verify the behavior of specific methods and their impact on a contract’s state.
6 min read
Formally Verifying Ownable.sol
Ownable is an abstract contract that provides owner-based access control.
8 min read
Introduction to Method Properties
In the previous chapter, we learned about parametric rules, which allow us to formally verify properties that are expected to hold regardless of which…
5 min read
Testing msg.sender and msg.value in CVL
In this chapter, we introduce the env variable in CVL, which enables us to make rules for functions that depend on msg.sender, msg.value, and other…
7 min read
Testing Revert Call In Certora
In this chapter, we will learn how to use method tags (@withrevert and @norevert) and the special variable lastReverted in CVL to verify expected reverts…
9 min read
Conditional Statements in CVL and Formally Verifying Parts of Solady and Solmate
Some contract behaviors (properties) are inherently conditional, and using constructs like if/else in CVL is one way to capture conditional behavior…
10 min read
Implication Operator
The implication operator is frequently used as a substitute for the if statement since it is cleaner.
6 min read
Formally Verifying a Counter
In the previous chapter, we learned the theoretical side of formal verification, including what it is and how it works.
4 min read
Formally Verifying Nonces.Sol in OpenZeppelin
Nonces, which stands for "number used once" are used in digital signature schemes to prevent replay attacks.
9 min read
Constructors in Cairo
A constructor is a one-time-call function executed during contract deployment to initialize state variables, perform contract setup tasks, make…