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

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

Loops in CVL: Path Explosion and Loop Unrolling Loops are one of the most common programming constructs, but they remain challenging to reason about in formal verification. While a loop in Solidity...

Introduction to Invariants in Certora Up until now, we’ve focused on verifying the behavior of individual methods or sequences of methods — ensuring that a specific function call or set of calls,...

Formally Verify Solady WETH Introduction ETH, widely used in DeFi for swaps, liquidity provision, staking, and collateral, needs an ERC-20-compatible version so protocols can interact with it through...

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

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

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

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

Cairo for Solidity Developers Cairo is a Rust-inspired language that compiles to bytecode, which runs on the Cairo Virtual Machine. The Cairo virtual machine is a zero-knowledge virtual machine...