This lecture provides a structured introduction to the verification of Ethereum smart contracts, beginning with the fundamentals of the Ethereum execution layer and progressing all the way to verification. The session consists of two parts: (1) Theoretical background: EVM execution semantics, bytecode analysis, the Solidity language, fuzzing and verification systems for the EVM. (2) Hands-on tutorial in which we will write, compile and examine a few contracts, verifying some of their properties. Overall, the goal of the two-part lecture is to gain both conceptual knowledge of the EVM, and hands-on experience with it and its associated tooling for building, examining, and verifying smart contracts.
Meant to be a hands-on lecture for Phd/Postdoc students, but also suitable for advanced undergraduates. The lecture contains slides from the hevm presentation given at various conferences, but gives a much more comprehensive introduction to the Ethereum execution layer and related tools and issues.
Brussels, Belgium, 9th of July 2025, at the 4th Summer School on Security Testing and Verification
Presentation under GPLv3 license except for PDF illustrations that are BSD licensed, marked as such in the slides.