Browse all Smart Contract Security articles.
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...
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...
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...
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...
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. For example: In Chapter 2,...
5 min read
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...
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. In this module, we’ll move beyond theory and learn...
13 min read
Certora Require, Assert, and Satisfy In the previous chapter, we learned that a specification is a piece of code written in CVL that describes the expected behavior of a smart contract. A...
10 min read
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...
4 min read
Formally verifying Initializable.sol This article describes how Certora formally verified the Initializable.sol OpenZeppelin contract. We assume the reader is already familiar with how this contract...
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 in non-payable contexts. In those examples, access...
7 min read
Testing Revert Call In Certora In this chapter, we will learn how to use method tags ( and ) and the special variable in CVL to verify expected reverts in smart contract execution. Setting Up...