Σ SymEx-EVM
Exhaustive symbolic execution for EVM bytecode. It proves contract invariants, synthesises concrete exploits from SMT models, and survives path explosion by merging state rather than enumerating it.
01 — the treeOne fork, and what falls out of it
The execution tree forks at the conditional jump JUMPI [0x04a2]. One branch asks whether the caller's balance covers the amount; the other does not, and reaches a CALL before the balance is written back. The engine models storage slots as uninterpreted arrays and Keccak-256 preimages as collision-resistant algebraic mappings, so it can carry that branch symbolically rather than guessing at concrete values.
When the solver returns a model, that model is not a warning. It is a concrete counter-example: a transaction sequence that reaches the sink, generated rather than described. The path above is the one it takes.
02 — the hard partThree answers to path explosion
Unconstrained symbolic execution explodes combinatorially on loops and cryptographic hashes. These are the mechanisms that keep it tractable.
| Mechanism | What it does |
|---|---|
| ITE state merging | Converging control paths are unified into conditional expressions, (ite cond pathA pathB), which removes duplicate sub-trees instead of exploring both. |
| Keccak uninterpreted functions | A symbolic hash table maps hash outputs back to preimages, bypassing the non-linear bitvector expansion that would otherwise stall the solver. |
| Concolic fuzzing seeds | Hybrid concrete execution guides exploration toward deep branches, solving path predicates dynamically when a branch turns intractable. |
03 — the backendNative Z3, or SMT-LIB2
The same reasoning engine is reachable two ways: direct C bindings for throughput, or zero-dependency SMT-LIB2 string emission where a native library cannot be shipped.
| Feature | Native Z3 (C-API) | SMT-LIB2 fallback |
|---|---|---|
| solving latency | 0.4 ms per push-pop | 18 ms per process pipe |
| dependency | linked libz3 | none — emitted text |
| use | throughput scanning | portability and audit |
git clone https://github.com/KELLERBABG/SymEx-EVM.git cd SymEx-EVM && cargo test --workspace cargo run --bin symex -- scan --target contracts/Vault.bin --solver native-z3