- 0xkarmacoma Formal verification to the people Thread
- 3 Myths of Formal Verification
- 5 Myths about Formally Verifying Smart Contracts
- A Guide To formal Verification of Smart contracts
- Awesome Halmos
- Awesome Symbolic Execution
- Certora Documentation
- Certora Tutorials
- daejunpark halmos usage Thread
- Decompiling Vyper Programs for Formal Verification
- Enhancing Smart Contract Security with Certora’s Formal Verification
- ERC20-K: Formal Executable Specification of ERC20
- ERC777-K: Formal Executable Specification of ERC777
- Ethereum Formal Verification
- Everything You Wanted to Know About Symbolic Execution for Ethereum Smart Contracts
- EVM Symbolic Execution
- Finding Bugs in Formal Specifications
- Formal Methods for DeFi Developers
- Formal Verification Basics: The Science of Ensuring System Integrity
- Formal Verification Made Easy with SMTChecker
- Formal Verification of ERC20 Contracts
- Formal Verification of Smart Contracts: Equivalence Checking of Uniswap Library
- Formally Verifying Finality in Gasper:
- Formally Verifying Loops: Part 1 & 2
- Formally Verifying WETH
- Gambit: A Solidity Mutation Testing Tool for Formal Verification
- Guide To Formal Verification Video
- How Formal Verification of Smart Contracts Works
- Implementing stateful invariant testing with Halmos
- k-uniswap-v2
- MIT Symbolic Execution Video
- Morpho Certora Tutorials
- patrickalphac Formal Verification & Symbolic Execution Thread
- Preventing reentrancy bugs — another use case for formal verification
- Preventing reentrancy bugs — another use case for formal verification
- Quint - A modern and executable specification language
- Quint - Protocol Specifications Made Executable
- Quint presentation at Gateway to Cosmos
- Quint specification examples
- Scaling Formal Verification to Find Bugs in Complex Smart Contract Systems Video
- Shift Left: Formal Verification First, Not Last!
- Smart Contract Formal Verification
- Smashing bugs using Certora Prover
- SMTChecker and SMT Solvers: Exploring Formal Verification One Step at a Time
- SMTChecker: The Game Changer in Smart Contracts Verification and Security
- Solana Formal Verification: A Case Study
- Solana Verification Part 1: Formal Verification of Solana Smart Contracts
- Specification and model checking of BFT consensus by Matter Labs
- Specification and Model-checking of the ZKsync Governance Protocol
- Stopping DeFi Bugs at Scale
- Symbolic testing with Halmos
- Testing and Formal Verification for Web3 Smart Contract Security
- The Easy Way To Quit (Concrete) Testing
- Using Formal Verification on ZK Systems
- Verification of Remco's full 256x256 bit multiplication
- Warning: Code Can Be Explosive
- Z3 Docs
- zachobront Solady FixedPointMathLib testing Thread