Solidity

Library call on Starknet A library call executes the logic of a declared contract class in the context and storage of the contract that invokes it. This is similar to Solidity’s but uses class hashes...

Hash Functions on Starknet Solidity relies on keccak-256 as its primary hash function to derive deterministic identifiers from arbitrary data such as computing function selectors or computing storage...

Syscalls in Starknet In Solidity, low-level operations like reading/writing to storage, contract to contract calls, or sending messages are performed directly through inline assembly using Yul...

Using “requireInvariant" in Rules and Invariants Up until now, we’ve either written a rule to verify specific behaviors or an invariant to verify properties that must always hold true throughout the...

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

Preserved Block and Its Role in Invariant Verification An invariant is a property that must always hold true after a smart contract is deployed and throughout its execution. At first glance,...

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

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

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

Invariants for ERC-721 Introduction In previous chapters, we explored how CVL invariants work: properties that must hold throughout all contract execution. Invariants can function as preconditions in...

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

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