Blog
The technical content top engineers rely on to level up.
9 min read
Native Solana: Program Entry and Execution
Native Solana: Program Entry and Execution All through this series, we've used the Anchor framework to build Solana programs. This tutorial teaches you how to write them in native Rust without...
12 min read
Switchboard
Switchboard On-chain programs can’t access off-chain data directly. They rely on oracles to bring in information such as asset prices, event outcomes, or API responses. Without these oracles,...
17 min read
Preserved Block and Its Role in Invariant Verification
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,...
9 min read
SafeMint and SafeTransfer Rules in ERC-721
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...
13 min read
Using “requireInvariant" in Rules and Invariants
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...
10 min read
Verifying an Invariant Using Ghost and Hook
Verifying an Invariant Using Ghost and Hook In any correct ERC20 implementation, the sum of all account balances must always equal the total token supply. This property should always remain true...
12 min read
Partially Parametric Rules for ERC-721
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...
10 min read
Constraining Ghosts in Invariants
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...
17 min read
Loops in CVL: Path Explosion and Loop Unrolling
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...
14 min read
Invariants for ERC-721
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...
12 min read
Introduction to Invariants in Certora
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,...
10 min read
Mint and Burn Rules for ERC-721
Mint and Burn Rules for ERC-721 Introduction ERC-721 is the Ethereum standard for non-fungible tokens, widely used to represent digital property. Like any form of property, it revolves around supply...