2025-06-12 –, 9 - Workshop
Fuzzing and Formal Methods are often seen as competing approaches to smart contract security. In this hands-on workshop, we combine insights from both, allowing participants to build a minimal EVM/Solidity smart contract fuzzer in Python within 25 minutes. We also explore critical questions such as:
- How can we measure the success of our fuzzing campaign?
- Is the number of runs a reliable coverage metric?
- What alternative metrics could provide deeper insights?
- Why is naive input generation insufficient for smart contracts?
- How can we improve input generation to achieve better coverage?
Participants will gain practical experience building a fuzzer while learning key concepts in smart contract fuzzing, guided by a Formal Methods-informed approach.
Technical Requirements:
- Python + pip installed (alternatively, a VSCode devcontainer will be provided)
- Basic understanding of Solidity and the EVM
This workshop is designed for developers, security researchers, and smart contract auditors interested in better understanding fuzzing as a technique for automated vulnerability discovery. While fuzzing is increasingly used in smart contract security, its evaluation is often ad-hoc, with "number of runs" being a common but misleading coverage metric.
We take a more rigorous approach, applying a Formal Methods mindset to assess fuzzing campaigns more effectively.
Participants will:
- Build an EVM fuzzer from scratch in Python within 25 minutes.
- Understand core fuzzing principles and why naive metrics can mislead.
- Explore advanced coverage metrics for fuzzing.
- Implement practical improvements to enhance fuzzer performance.
- Gain deeper technical insights into Solidity and the EVM.
By the end of the session, attendees will:
- Gain foundational skills to design effective fuzzing campaigns.
- Accurately assess the effectiveness of fuzzing.
- Make informed choices regarding fuzzing or formal verification-based security audits.
Dr. Thomas Pani is a Web3 Security Researcher at blltprf.xyz with experience in the Ethereum, Cosmos, and Stellar ecosystems. He holds a PhD in Computer Science from TU Wien and has collaborated on notable security projects, including grants for consensus protocol verification from the Ethereum Foundation, the development of runtime monitoring tools for the Stellar Development Foundation, and work on the Quint specification language and the Apalache model checker for TLA+. He enjoys turning rigorous academic insights into practical solutions that actually help secure today's blockchain ecosystems.