Everything You Wanted to Know About Symbolic Execution for Ethereum Smart Contracts (But Were Afraid to Ask)

The blog post introduces the concept of symbolic execution as a formal verification technique for smart contracts, which assigns symbolic values to input variables to explore multiple execution paths at the same time and check whether certain properties or vulnerable states can be violated.

The post explores existing bytecode-level symbolic execution tools for Ethereum smart contracts, including Manticore, Mythril, hevm, and EthBMC, and highlights their strengths and limitations through experiments.

The challenges of symbolic execution, such as state space explosion, constraint solving, interaction with the environment, and modeling memory and storage, are also discussed.