# Practical Symbolic Execution for EVM - Palina Tolmach, MakerDAO

###### tags: `2023`, `DAY2`, `DEFI`
{%hackmd @ethtaipei/ByQLufgQ2 %}

> Share your thoughts from here

### Why
* Symbolic execution is a verficiation / bug finding technique
* symbloic execution and formal verificaion are more **comprehensive** ways to test the codebae
* unit tests are important, but it is also limited in terms of the states a contract code could be in

### What
SMT solver

###
Symbloic testing
* run symbolic execution on the tests
* integrating into foundry to use `prove` as prefix and run the symblic exeuction on the tests it self

## More Detail
* https://hackmd.io/@SaferMaker/EVM-Sym-Exec

## QA Notes
* Hashing function is a bottleneck for SMT solvers
* The complexity (resoures needed) grows exponentially with the size of the code base