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...

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...

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...

Conditional Statements in CVL and Formally Verifying Parts of Solady and Solmate Introduction Some contract behaviors (properties) are inherently conditional, and using constructs like if/else in CVL...

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...

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...

Constructors in Cairo A constructor is a one-time-call function executed during contract deployment to initialize state variables, perform contract setup tasks, make cross-contract interactions and...

Cairo Components Part 1 Components in Cairo behave like abstract contracts in Solidity. They can define and work with storage, events, and functions, but they can’t be deployed on their own. The...

Access Control in Cairo Access control defines who can call specific functions or modify contract behavior. This article explains how Cairo implements access control using the macro. A Review of...

Structure of a Basic Contract This article shows how to build a deployable Cairo contract for Starknet. Starting from a simple sketch, we will gradually add features to build a working contract...