Browse all Smart Contract Security articles.
26 min read
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...
6 min read
Native Solana: Essential Security Checks In our previous native Solana tutorials, we skipped security checks to keep examples short and focused on the core topics. In this tutorial, we'll cover...
15 min read
Introduction to Storage Hooks and Ghosts It often becomes necessary to inspect changes at specific storage locations to prove that a property or invariant holds, especially when the storage is not...
6 min read
Using Sload Hooks with Storage Mappings Introduction In the previous chapter, we demonstrated that hooks are necessary to verify properties involving changes in mapping values. The hook monitors...
8 min read
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...
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...
17 min read
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,...
12 min read
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,...
9 min read
Persistent Ghosts Introduction In previous chapters, we used ghost variables (via hooks) to record storage values and quantities that were not explicitly tracked in smart contracts — for example, the...
13 min read
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...
17 min read
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...
13 min read
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...