Awesome Advanced Smart Contracts Testing and Verification

A curated collection of tools, frameworks, and resources for testing and verifying Solidity smart contracts. Meant to be used by blockchain developers and security researchers as a knowledge source.

Contents

• Tools
• Fuzzing
  • Property-based Fuzz Testing
  • Differential Fuzz Testing
• Formal Verification
• Mutation Testing
• Branching Tree Technique
• Contribute

Tools

Arsenal of fuzzing and verification tools, tailor-made for probing and dissecting the inner workings of smart contracts.

• Foundry | Ethereum development framework written in Rust
• Echinda | Ethereum smart contract Property-based fuzzer
• Medusa | Property-based fuzzer based on Echidna written in go
• ItyFuzz | EVM and MoveVM hybrid fuzzer that combines symbolic execution and fuzzing
• Fuzz-utils | Tool for generating Foundry unit tests from smart contract fuzzer failed properties
• Maat | Dynamic Symbolic Execution and Binary Analysis framework
• Optik | Echidna + Maat coupling for coverage analysis driven Fuzzing
• Etheno | JSON RPC multiplexer, analysis tool wrapper, test integration tool
• Certora Prover | Formal verification Tool
• Halmos | Symbolic testing tool for EVM smart contracts
• Simbolik | Solidity smart contract symbolic debugger
• Kontrol | Formal verification with KEVM and Foundry
• Dafny-EVM | functional specification of the Ethereum Virtual Machine in Dafny
• Pyrometer | symbolic execution, abstract interpretation, and static analysis
• Gambit | Solidity mutation system
• Vertigo-rs | Ethereum smart contract mutation testing framework
• Bulloak | Solidity test generator based on the Branching Tree Technique

Fuzzing

Fuzzing or fuzz testing is an automated software testing technique that involves providing invalid, unexpected, or randomly generated data as inputs to a computer program.

• Fuzzing Labs @Pat_Ventuzelo ETHCC5 Fuzzing talk
• Trail of Bits Fuzzing Workshop (10 hours Workshop)
• @vn_martinez_ Mastering Fuzzing (seminar materials)
• @dacian Exploiting Precision Loss via Fuzz Testing
• Foundry Book Fuzz Testing
• @paco0x Kyber Network exploit reproduction with Fuzzing

Property-based Fuzz Testing

Property-based testing aims to identify and test invariants. Invariants are conditions expressions that should always hold true over the course of a fuzzing campaign. Invariants are about properties of the system as a whole, rather than specific reactions to specific inputs.

• Trail of Bits pre-defined invariants
• Trail of Bits Echidna Tutorials
• Gustavo Grieco - Spearbit: Echidna Workshop
• @agfviggiano Advanced Fuzzing Techniques: An eBTC Case Study
• @agfviggiano OpenSense Invariant Testing Workshop
• @agfviggiano How to How to write (good) invariants?
• RareSkills invariant testing in foundry
• @horsefacts Invariant Testing WETH With Foundry
• Patrick Collins Fuzz | Invariant Tests
• Hybrid fuzzing: Sharpening the spikes of Echidna
• Foundry Book Invariant Testing
• Perimetersec Public Fuzzing Campaigns List
• Public Use of Echidna

Differential Fuzz Testing

Differential testing is used to ensure identical behavior between two or more implementations of equivalent code. Useful if you are upgrading/updating code, or have written a more optimized version but you want to verify congruence among implementations.

• @annascarrol Solidity Summit 2023 - Differential Testing with Foundry by Anna Carroll (link 2)
• Differential Test | Testing with Foundry
• Foundry Book differential testing
• Seaport | Discussion #809 Understanding the "DifferentialTest" test contract
• Murky Merkle Tree DifferentialTests.t.sol
• EnbangWu Differential Fuzzing of solidity Fixed-point libraries
• Using Halmos to Formally Verify Solady's FixedPointMathLib

Formal Verification

Formal Verification is an approach to assessing the correctness of software by checking whether a formal model of the program matches the formal specification. Unlike testing, formal verification can verify a smart contract's execution satisfies a formal specification for all executions without needing to execute it with sample data.

• Certora prover documentation
• Certora ERC4626 TrustX 2023 workshop
• Certora Formal Verification of Openzeppelin contracts
• WilfredTA formal-methods-curriculum
• Everything You Wanted to Know About Symbolic Execution for Ethereum Smart Contracts
• The Easy Way To Quit (Concrete) Testing
• 0xkarmacoma Beyond Fuzzing: Symbolic Testing in Practice Solidity Summit 2023 (X thread)
• runtime verification The Symbolic Solidity Debugger TrustX 2023
• jellopaper.org KEVM: Semantics of EVM in K

Mutation Testing

Mutation testing is a technique for evaluating and improving test suites. The key idea is to introduce faults, called mutants, to the program under test and measure a test suite’s ability to detect these mutants.

• Chandrakana Nandi, How Good Is Your Formal Specification? Mutation Testing To The Rescue! Solidity Summit 2023
• Certora Gambit: Mutation Generator for Solidity Docs

Branching Tree Technique

Specification framework for writing structured Solidity tests.

• @PaulRBerg Branching Tree Technique
• @PaulRberg Solidity Summit 2023 Branching Tree Technique
• PaulRBerg/btt-examples

Contribute

Contributions welcome! Read the contribution guidelines first.