The HEVM Symbolic Simulation Framework

Mate Soos
Tuesday |12th December 2023 | 11.00 AM – 12.00 PM
New CC Building 1st floor CC109

In realm of digital finance, a decade-long revolution has reshaped financial systems. Amidst this upheaval, substantial research investments focus on validating digital contracts — complex programs managing billion-dollar transactions. The sakes are high, where even a minor bug can cause irreversible losses, sometimes reaching hundreds of millions of USD [1]. Hence, verifying the correctness of these contracts is paramount. In this talk, we will discuss the details of the HEVM symbolic execution framework [2] that can be used to verify properties of digital contracts written in EVM bytecode, the most popular digital contract execution framework.

 [1] Explore real-world examples at

 [2] Dive into the HEVM framework at


Online Meeting link (for those who cannot join in person): Webex link

Meeting number: 2515 059 6247

Meeting password: AHeeYm8X3M5

Speaker Biography

Mate Soos obtained his PhD from INRIA in 2009 and has since been working both in academia and industry on formal verification, breaking lightweight cryptographic primitives, and IT security. He is the author of the SAT solver CryptoMiniSat, and has worked with Kuldeep Meel on the model counters ApproxMC and Ganak, as well as the almost-uniform sampler CMSGgen, and the probabilistically approximate sampler UniGen. He has also helped reverse engineer and break the lightweight ciphers HiTag2 and Megamos, among others, through a combination of SAT solving, algebraic cryptanalysis, GPGPU, and FPGA programming. He is currently employed by the Ethereum Foundation to work on Formal Methods tooling for the Ethereum ecosystem, and regularly does research at the National University of Singapore on formal methods.