Symbolic Execution for Smart Contracts: Exploring Every Path Without Executing Any

Fuzzing tests millions of inputs but might miss the one that triggers a bug. Static analysis approximates behavior but can’t prove absence of vulnerabilities. Symbolic execution takes a different approach: instead of running code with specific values, it runs code with symbols—variables that represent all possible values simultaneously—and at each branch, explores both directions.

The result is systematic coverage of every execution path, paired with a constraint solver that can produce the exact inputs needed to reach any particular state.

How Symbolic Execution Works

In concrete execution, input = 42 determines a single execution path. In symbolic execution, input = α (a symbolic variable) means both branches of any conditional on α are explored:

Concrete:
    input = 42
    if (input > 100):
        do_something()   // not executed
    else:
        do_other()       // executed

Symbolic:
    input = α
    if (α > 100):
        do_something()   // path constraint: α > 100
    else:
        do_other()       // path constraint: α ≤ 100
    // both paths explored

Each path accumulates a set of constraints—conditions that must be true for execution to follow that path. When a potential vulnerability is found on a given path, the constraints can be handed to an SMT solver to produce concrete inputs that actually trigger it.

The Symbolic EVM State

A symbolic execution engine maintains symbolic versions of all EVM state components:

Stack:   [α, β + 5, 0x1234]
         (symbolic, expression, concrete)

Storage:
    slot[0]: δ
    slot[keccak(ε, 0)]: balance_of_ε

Path Constraints:
    α > 0
    β < 1000
    γ == keccak256(α)

Each opcode updates this state. Arithmetic operations build up symbolic expressions:

def symbolic_execute(opcode, state):
    if opcode == 'ADD':
        a = state.stack.pop()
        b = state.stack.pop()
        state.stack.push(symbolic_add(a, b))

    elif opcode == 'JUMPI':
        dest = state.stack.pop()
        cond = state.stack.pop()

        # fork: explore both branches
        true_state = state.clone()
        true_state.add_constraint(cond != 0)
        true_state.pc = dest

        false_state = state.clone()
        false_state.add_constraint(cond == 0)
        false_state.pc = state.pc + 1

        return [true_state, false_state]

The JUMPI case is where the path count doubles. A function with 10 conditional branches can produce up to 1,024 distinct paths.

Constraint Solving with SMT

Path constraints are solved using SMT (Satisfiability Modulo Theories) solvers. Given a set of constraints, the solver either finds a satisfying assignment (concrete values that meet all conditions) or proves that no such assignment exists:

from z3 import *

α = BitVec('alpha', 256)  # 256-bit EVM word
β = BitVec('beta', 256)

solver = Solver()
solver.add(α > 0)
solver.add(β < 1000)
solver.add(α + β == 500)

if solver.check() == sat:
    model = solver.model()
    # α = 400, β = 100 (or any valid solution)

For EVM analysis, the relevant SMT theories are:

• BitVector theory: 256-bit arithmetic, overflow semantics, bitwise operations
• Array theory: memory and storage as arrays with symbolic indices
• Uninterpreted functions: model keccak256 (can’t solve it, but can reason about its properties)

Finding Vulnerabilities

The core technique is expressing vulnerability conditions as reachability queries: can the constraint solver find inputs that make a specific opcode sequence reachable?

Reentrancy: can we reach CALL on line N before the SSTORE that updates the balance?

def check_reentrancy(symbolic_trace):
    for i, (state, opcode) in enumerate(symbolic_trace):
        if opcode == 'CALL':
            for j in range(i + 1, len(symbolic_trace)):
                if symbolic_trace[j][1] == 'SSTORE':
                    slot = symbolic_trace[j][0].stack[-2]
                    if was_read_before(slot, symbolic_trace[:i]):
                        return True, state.path_constraints
    return False, None

Integer overflow: can arithmetic wrap around?

def check_overflow(state, operation, operands):
    if operation == 'ADD':
        a, b = operands
        result = a + b
        overflow_constraint = And(
            ULT(result, a),      # result < a means overflow
            state.path_constraints
        )
        solver = Solver()
        solver.add(overflow_constraint)
        if solver.check() == sat:
            return {'vulnerability': 'integer_overflow', 'inputs': solver.model()}

Access control bypass: can a non-owner caller reach a privileged function?

def check_access_control(symbolic_states, privileged_operations):
    for state in symbolic_states:
        if state.current_opcode in privileged_operations:
            bypass_constraint = And(
                state.path_constraints,
                state.caller != state.storage['owner']
            )
            solver = Solver()
            solver.add(bypass_constraint)
            if solver.check() == sat:
                return {
                    'vulnerability': 'access_control_bypass',
                    'malicious_caller': solver.model()[state.caller]
                }

When the solver finds a satisfying model, it returns concrete values—an actual address, an actual amount—that would trigger the vulnerability. This is the practical output: not just “this path might be vulnerable” but “call this function with these exact arguments.”

The Hard Parts of EVM Analysis

Keccak256. Storage slots for mappings are computed as keccak256(key ++ slot_index). The solver can’t invert keccak256—that would break cryptography. The workaround is to model keccak as an uninterpreted function: treat it as a black box that maps inputs to outputs, add constraints that encode known properties (different inputs produce different outputs), and add any known concrete hash values:

keccak = Function('keccak', BitVecSort(512), BitVecSort(256))

# collision-freeness: if inputs differ, outputs differ
for (i1, o1), (i2, o2) in known_hashes:
    solver.add(Implies(i1 != i2, o1 != o2))

# add known concrete mappings
solver.add(keccak(concat(user, 0)) == known_slot)

This allows reasoning about relative relationships between slots without solving the hash itself.

Dynamic jumps. The function dispatcher computes jump destinations at runtime based on the function selector in calldata. To handle this, the engine finds all valid JUMPDEST locations in the bytecode and tries each one:

def resolve_dynamic_jump(state):
    dest = state.stack[-1]
    if is_concrete(dest):
        return [dest]

    valid_dests = find_all_jumpdests(bytecode)
    results = []
    for valid_dest in valid_dests:
        solver = Solver()
        solver.add(state.path_constraints)
        solver.add(dest == valid_dest)
        if solver.check() == sat:
            results.append(valid_dest)
    return results

Loops. Unbounded loops cause path counts to grow without bound. Practical approaches: bound the loop to a fixed number of iterations (sound but incomplete), summarize the loop’s effect symbolically (if the pattern is recognizable), or widen—after N iterations, over-approximate the possible state to a broad constraint and continue.

Path explosion. Even without loops, the number of paths grows exponentially with the number of conditional branches. A 50-function contract can have millions of paths. Mitigations include state merging (combine similar states into one state with disjunctive constraints), function summaries (pre-compute a function’s preconditions and postconditions so it doesn’t need to be re-analyzed every time it’s called), and directed exploration (prioritize paths that are closer to the code under scrutiny).

Concolic Execution

Concolic execution blends concrete and symbolic: run concretely for speed, collect constraints symbolically for exploration, then negate constraints to generate new inputs for unexplored paths:

def concolic_execution(contract, initial_input):
    explored_paths = set()
    worklist = [initial_input]

    while worklist:
        input = worklist.pop()
        trace = execute_with_constraints(contract, input)
        explored_paths.add(trace.path_hash)

        for i, constraint in enumerate(trace.constraints):
            # keep constraints [0..i-1], negate constraint[i]
            new_constraints = trace.constraints[:i] + [Not(constraint)]
            solver = Solver()
            solver.add(And(new_constraints))

            if solver.check() == sat:
                new_input = solver.model()
                if hash(new_input) not in explored_paths:
                    worklist.append(new_input)

Compared to pure symbolic execution, concolic is faster for known paths (concrete execution is much cheaper than maintaining symbolic state through every instruction). Compared to pure fuzzing, concolic is systematic—it guarantees coverage of all paths within the resource budget rather than hoping random mutation reaches everything.

Practical Tools

Several mature tools implement symbolic execution for EVM contracts:

Mythril analyzes Solidity source or bytecode and reports findings with SWC IDs and bytecode offsets:

myth analyze --execution-timeout 300 --strategy bfs contract.sol

Manticore provides a Python API for scripted analysis:

from manticore.ethereum import ManticoreEVM

m = ManticoreEVM()
owner = m.create_account(balance=1000)
contract = m.solidity_create_contract('contract.sol', owner=owner)

sym_data = m.make_symbolic_buffer(64)
m.transaction(
    caller=m.create_account(),
    address=contract,
    value=m.make_symbolic_value(),
    data=sym_data
)

HEVM (from DappTools/Foundry) runs symbolic execution at the bytecode level with direct control over which arguments are symbolic:

hevm symbolic --code <bytecode> \
    --sig "transfer(address,uint256)" \
    --arg 0x1234...      # concrete first arg
    --arg "<symbolic>"   # symbolic second arg

Where Symbolic Execution Fits

Symbolic execution sits between static analysis and fuzzing in the precision-speed tradeoff:

Technique	Coverage	Precision	Speed
Static analysis	All paths	Approximate	Fast
Symbolic execution	All paths (resource-bounded)	Exact	Slow
Fuzzing	Sampled paths	Exact	Fast

The combination that works well in practice: static analysis to identify suspicious functions quickly, targeted symbolic execution to prove or disprove specific vulnerability hypotheses for flagged code, and fuzzing to explore complex multi-step interactions that neither technique handles well alone.

Symbolic execution’s distinctive value is the proof: when it says “this path is unreachable under any input,” that’s a stronger statement than “I tested a million inputs and didn’t find it.” And when it says “this overflow is reachable,” it hands you the exact inputs to reproduce it.