foundry-evm-symbolic

foundry-evm-symbolic is Foundry's native symbolic EVM executor. It powers forge test --symbolic and is intended to make symbolic tests feel like normal Forge tests: write Solidity, run Forge, get either a proof result or a concrete counterexample that is replayed through the normal Foundry executor before it is reported.

Most users should interact with this crate through Forge. The Rust crate is the engine that Forge calls after it has compiled contracts, run setUp, selected tests, and prepared the concrete executor backend.

Quick Start

Symbolic tests are Solidity functions named check* or prove*.

// SPDX-License-Identifier: UNLICENSED
pragma solidity ^0.8.20;

import "forge-std/Test.sol";

contract MathSymbolicTest is Test {
    function check_average(uint256 a, uint256 b) external pure {
        uint256 average = (a + b) / 2;

        // Forge should find an overflow counterexample.
        assertGe(average, a <= b ? a : b);
    }
}

Run it with:

forge test --symbolic --match-test check_average

Requirements:

• The configured solver must be available. The default solver command is z3. Install it locally with your package manager, for example brew install z3 on macOS or sudo apt-get install z3 on Ubuntu.
• check* and prove* tests are only selected when --symbolic is enabled and the contract is in a source path Forge compiles for the current project.
• A reported counterexample must replay concretely before Forge prints it as a failure.

--match-test filters function names or signatures. To filter by contract, use --match-contract:

forge test --symbolic --match-test check_average
forge test --symbolic --match-contract MathSymbolicTest

Result Semantics

Native symbolic testing is a preview feature. Results are scoped to the executor's current EVM model and the configured exploration bounds.

Symbolic testing works best for Solidity-level properties that fit the modeled EVM surface: arithmetic, storage, calldata, common call/reentrancy flows, selected cheatcodes, and bounded stateful sequences. It finds and replays concrete witnesses when it can. When a test depends on unsupported or unmodeled behavior, Forge reports the run as incomplete instead of treating the property as proven. It does not model full revm behavior, arbitrary unknown fork accounts, or cryptographic preimage/collision search.

Forge reports symbolic test outcomes as:

• PASS: every explored path finished without a feasible failure under the currently modeled semantics and configured bounds.
• FAIL with a counterexample: the solver found a failing model and Forge replayed that concrete input or invariant sequence through the normal executor.
• FAIL: incomplete symbolic execution (...): Forge could not complete the search or validate a counterexample for this run. Treat this outcome as "not established".

When --json is enabled, each symbolic test result includes a stable symbolic object in addition to the legacy test fields. The schema lives at crates/evm/symbolic/assets/symbolic-result.schema.json and records the normalized status (pass, fail_counterexample, or incomplete), incomplete reason kind, effective bounds, solver identity and counters, explicit assumptions, call-trace location metadata, replay status, and counterexample payload when one exists.

When Forge materializes a replay candidate, symbolic.artifact points to a durable replay artifact written under the configured cache path. The artifact schema lives at crates/evm/symbolic/assets/symbolic-counterexample.schema.json and records the replay status, bounds, assumptions, solver metadata, optional trace reference, and concrete call data needed by downstream minimizers and exporters.

Symbolic execution can also seed coverage-guided fuzzing by concretizing non-failing fuzz-test inputs into the configured fuzz.corpus_dir:

forge test --symbolic-seed-corpus --fuzz-corpus-dir fuzz_corpus

Forge symbolically executes matching fuzz tests, reuses their normal corpus layout, and writes a successful concrete input as a seed for later fuzz runs.

Symbolic execution can import the same Foundry fuzz corpus as path-priority hints for fuzz tests:

forge test --symbolic-use-fuzz-corpus --fuzz-corpus-dir fuzz_corpus

Imported corpus entries are bounded by symbolic.corpus_seed_limit and only guide branch order; they do not prune feasible symbolic paths. JSON output records the per-test corpus directory, import counts, and seed files that matched a symbolic calldata variant under symbolic.corpus_seeds.used.

Fuzzing can also record branch frontier artifacts for later targeted symbolic follow-up:

forge test --match-test test_hard_branch --fuzz-frontier-dir fuzz_frontiers

For example, a fuzz run may pass after reaching feeMultiplier == 100 at a feeMultiplier < 100 guard; the frontier gives symbolic execution the replay calldata and comparison site needed to solve the adjacent missed branch.

Forge writes one bounded artifact per fuzz test at <fuzz_frontier_dir>/<contract>/<test>/branch-frontiers.json. The artifact uses schema foundry:fuzz.branch-frontiers@v1 and records the test signature, configured record limit, and a frontiers array. Each frontier contains:

• a stable record index (id) within the artifact
• fuzz replay metadata (seed, run, worker) when available
• the concrete one-call sequence that reached the site
• the EVM comparison site (address, pc, opcode, opcode_name)
• concrete operands (lhs, rhs), the comparison result, and an operand_delta priority score interpreted according to opcode signedness
• whether the call also expanded the worker's coverage map (new_coverage), present only when edge coverage is collected via a corpus directory, edge coverage metrics, or sancov, and omitted otherwise

Frontier capture is opt-in and bounded by fuzz.frontier_limit (default 256). It reuses the fuzzer's comparison-operand inspector and does not store traces.

Symbolic execution can consume those artifacts to solve the opposite side of captured comparisons and write replay-confirmed inputs into the fuzz corpus:

forge test --match-test test_hard_branch \
  --fuzz-frontier-dir fuzz_frontiers \
  --fuzz-corpus-dir fuzz_corpus \
  --symbolic-use-fuzz-frontiers

Forge imports up to symbolic.frontier_limit records (default 256), replays the recorded one-call seed as a path-priority hint, constrains symbolic execution to flip the captured comparison result, and persists only candidates that replay with the expected concrete outcome.

To focus solver time on specific captured sites, pass frontier artifact IDs, comparison PCs, or calldata selectors:

forge test --match-test test_hard_branch \
  --fuzz-frontier-dir fuzz_frontiers \
  --fuzz-corpus-dir fuzz_corpus \
  --symbolic-use-fuzz-frontiers \
  --symbolic-frontier-ids 3,7 \
  --symbolic-frontier-pcs 128,412 \
  --symbolic-frontier-selectors 0x12345678

symbolic.frontier_ids, symbolic.frontier_pcs, and symbolic.frontier_selectors default to [], meaning any value for that dimension. Non-empty filters compose conjunctively, so the example imports only records matching one of the requested IDs, one of the requested PCs, and one of the requested selectors. Forge keeps the artifact order as the priority order after filtering, imports up to symbolic.frontier_limit records, reports how many records were imported or skipped by target filters, and warns if a requested target cannot be imported.

Hash-model caveat: PASS also assumes collision and preimage resistance for symbolic KECCAK256 and hash-like precompile terms. The executor may use equal symbolic hashes to infer equal symbolic preimages or lengths in modeled cases, and it does not search for Keccak collisions or adversarial preimages. Concrete counterexamples are still replayed before they are reported.

Symbolic exploration is bounded by configuration, including symbolic.max_depth, symbolic.max_paths, symbolic.max_solver_queries, dynamic calldata length settings, and symbolic.invariant_depth.

Incomplete can occur when exploration reaches a configured bound, the solver times out or returns unknown, a test uses unsupported EVM or cheatcode semantics, a backend error occurs, or a solver model does not replay concretely. When a solver candidate does not replay, it can still be shown as a diagnostic legacy top-level counterexample; treat it as confirmed only when symbolic.status is fail_counterexample and symbolic.replay.status is confirmed.

Current modeling notes:

• Unsupported opcodes, world-state behavior, or cheatcode forms are reported as incomplete results with an explanatory reason.
• Symbolic KECCAK256 supports common Solidity storage patterns; arbitrary symbolic hashing may require heuristics and can make a run incomplete.
• SELFDESTRUCT follows the active fork. Before Cancun it deletes the account; from Cancun onward it only deletes contracts created in the same top-level symbolic transaction, otherwise it transfers balance and halts while preserving code and storage. Cancun beneficiaries must resolve to concrete addresses; unresolved symbolic beneficiaries report incomplete.
• Counterexamples are shown only after successful concrete replay.

Writing Symbolic Tests

Stateless symbolic tests use ordinary ABI parameters. The executor creates symbolic calldata from the function ABI and explores feasible EVM paths.

Storage hooks can maintain revert-aware ghost state for raw storage accesses. Register a callback during setUp for each target and access kind:

function setUp() public {
    vm.registerSloadHook(address(vault), this.onLoad.selector);
    vm.registerSstoreHook(address(vault), this.onStore.selector);
}

function onLoad(address account, bytes32 slot, bytes32 value) external {
    require(msg.sender == address(vm), "only storage hook");
    // Update ghost state from the observed load.
}

function onStore(
    address account,
    bytes32 slot,
    bytes32 oldValue,
    bytes32 newValue
) external {
    require(msg.sender == address(vm), "only storage hook");
    // Update ghost state from the observed write.
}

Concrete and symbolic execution use the same callback contract. Re-registering an access kind replaces its callback for that target. Callback reverts propagate through the post-operation callback. Registration survives EVM reverts, while callback state follows the enclosing EVM context and rolls back with it. Hooks use the effective storage account, so a delegatecall is attributed to the caller's storage context. Hooks are suppressed throughout the callback's call subtree. Callback execution is hidden from mocks, expectations, recorded logs, and storage-access recording, while its EVM state writes and hook registrations are retained. Callbacks do not inherit staticness, so they can update ghost state for storage reads beneath STATICCALL; the observed target remains subject to normal static-call restrictions. The slot is the computed effective slot; mapping roots and decoded keys are not included. Callbacks are ordinary external functions, so they must authenticate msg.sender as address(vm) before updating ghost state. Registered callback selectors are excluded from default invariant targets, but explicit selector configuration can still target them. The callback runs as an ordinary call frame, so it consumes one of the 1024 protocol call-depth slots; a storage access at the maximum legal call depth that would otherwise succeed can have its callback rejected as too deep, which propagates as a failure of the storage operation.

Aggregate ghosts such as ghost = ghost - oldValue + newValue require an initialization model consistent with the ghost's starting value. Use symbolic.storage_layout = "zero_init" when the ghost starts from zero and unwritten symbolic mapping entries should be zero. With the default solidity layout, a previously unwritten symbolic key has an unknown base value, so the ghost must already account for that value. Known nonzero setup state must likewise be included in the initial ghost. These raw hooks cannot distinguish one mapping family from another without mapping-root provenance.

Mapping SSTORE hooks and ERC20 accounting

registerMappingSstoreHook can maintain a ghost aggregate for one mapping root without reacting to unrelated storage. For an ERC20 whose balances mapping is at slot zero:

function setUp() public {
    token = new Token();
    vm.registerMappingSstoreHook(address(token), bytes32(0), this.onBalanceWrite.selector);
}

function onBalanceWrite(
    address account,
    bytes32,
    bytes32 root,
    bytes32[] calldata keys,
    bytes32 oldValue,
    bytes32 newValue
) external {
    require(msg.sender == address(vm) && account == address(token));
    require(root == bytes32(0) && keys.length == 1);
    ghostSupply = ghostSupply - uint256(oldValue) + uint256(newValue);
}

With symbolic.storage_layout = "zero_init", initialize ghostSupply to zero and assert it equals totalSupply after symbolic mint, transfer, and burn operations. Allowance writes use a different root and do not affect the ghost. Both target writes and callback ghost updates roll back when the enclosing operation reverts. Mapping hooks require complete, exact 64-byte Keccak chains computed after the latest mapping-hook registration for that target in the current top-level execution. Resolution follows the complete chain to its terminal root instead of stopping at a registered intermediate hash; offsets, incomplete provenance, hashes computed before registration, and hashes from earlier top-level executions do not match. Hashes computed after registration remain usable by later calls in the same top-level execution. The contract that calls registerMappingSstoreHook receives the callback.

contract RiddleTest is Test {
    function check_riddle(uint256 x) external pure {
        uint256 sender = uint160(0x1804c8AB1F12E6bbf3894d4083f33e07309d1f38);

        unchecked {
            require(x * x < sender);
        }

        require(x > sender);
        require(x & 0x800 != 0);
        require(x & 0x10000 == 0);

        assert(false);
    }
}

In this style:

• require(...) prunes paths when the condition is false.
• vm.assume(...) also prunes paths.
• assert, forge-std assertions, and DSTest failure signals are treated as properties to disprove.
• User reverts terminate the current path. If every path reverts, Forge reports a revert-all result instead of a proof.

Dynamic ABI inputs are bounded. Use forge-config: inline annotations or foundry.toml to choose lengths.

contract BytesSymbolicTest is Test {
    /// forge-config: default.symbolic.array_lengths = [3]
    function check_bytes(bytes memory data) external pure {
        require(data.length == 3);
        if (data[0] == 0xaa && data[1] == 0xbb && data[2] == 0xcc) {
            assert(false);
        }
    }
}

Dynamic leaves are traversed in deterministic ABI pre-order. Lengths resolve in this order:

1. symbolic.dynamic_lengths, keyed by ABI argument name or generated symbolic name such as calldata_0.
2. symbolic.default_array_lengths for arrays, or symbolic.default_bytes_lengths for bytes and string.
3. The legacy positional symbolic.array_lengths, applied to the next dynamic leaf that was not matched by a named or type-specific default.
4. symbolic.default_dynamic_length.

Length-set config fields accept Halmos-style arrays and expand into separate symbolic calldata shapes. For nested dynamic values, Foundry explores the cross product implied by the selected outer lengths. Eager calldata expansion is capped by the effective symbolic path width (symbolic.width / symbolic.max_paths). Extra positional array_lengths entries are rejected as config errors.

Pending symbolic paths are explored in breadth-first order by default. Set symbolic.exploration_order = "dfs" to use depth-first ordering instead. This only changes which queued path is explored next; it does not change path limits, solver query limits, or solver portfolio scheduling.

Supported ABI shapes include:

• integers, booleans, addresses, fixed bytes, and dynamic bytes
• strings, constrained to printable ASCII for model extraction
• fixed and dynamic arrays
• tuples and structs, represented through ABI tuples

Stateful Symbolic Invariants

When --symbolic is enabled, invariant* and statefulFuzz* functions use a bounded symbolic call sequence instead of the normal invariant fuzzer.

contract CounterInvariant is Test {
    Counter counter;

    function setUp() public {
        counter = new Counter();
        targetContract(address(counter));
    }

    /// forge-config: default.symbolic.invariant_depth = 4
    function invariant_counterNeverFive() public view {
        assertTrue(counter.value() != 5);
    }
}

Forge reuses its invariant target discovery for target contracts, selectors, and senders. The symbolic executor chooses a bounded sequence from that discovered set, generates symbolic arguments with the same ABI model used for stateless tests, preserves symbolic world state between calls, and replays a concrete sequence before reporting a counterexample.

Some invariant harnesses deploy dependency contracts in setUp, then rely on those dependencies having satisfiable environment state during the campaign. For example, a lending invariant may call an ERC20 mock for balances and allowances, or an oracle mock for a price, without exposing target functions that write those values first. In that case the dependency storage remains the concrete state produced by setUp, and symbolic execution can only explore paths reachable from that concrete dependency state.

Use Foundry's existing vm.setArbitraryStorage(address) cheatcode to mark those environment dependency contracts as symbolic storage targets:

function setUp() public {
    loanToken = new ERC20Mock();
    collateralToken = new ERC20Mock();
    oracle = new OracleMock();

    vm.setArbitraryStorage(address(loanToken));
    vm.setArbitraryStorage(address(collateralToken));
    vm.setArbitraryStorage(address(oracle));

    targetContract(address(this));
}

If the harness imports a smaller Hevm interface that does not expose this cheatcode, declare a local interface with setArbitraryStorage(address) and cast it to address(vm).

Keep this scoped to external dependencies that model the environment, such as token balances, token allowances, and oracle prices. Do not blanket-mark the invariant harness or protocol state as arbitrary; that can create unreachable states and counterexamples that concrete replay rejects.

Replay currently materializes only concrete storage slots observed during symbolic execution. Dependency storage keyed by symbolic calldata is still explored symbolically, but it can replay-filter to Incomplete or mismatch instead of a confirmed counterexample if the required slot is not concrete.

Configuration

The primary configuration path is native Foundry config.

[profile.default.symbolic]
solver = "z3"
# Optional exact command. When set, this overrides `solver`.
# solver_command = "z3 -in -smt2"
# Optional solver names or commands to race in parallel. Ignored when
# `solver_command` is set. Entries with spaces/quotes/backslashes are parsed as
# argv strings, not shell snippets.
# solver_portfolio = ["yices", "z3"]
timeout = 30
max_depth = 10000
max_paths = 1024
exploration_order = "bfs"
max_solver_queries = 10000
default_dynamic_length = 2
max_dynamic_length = 256
array_lengths = []
dynamic_lengths = {}
default_array_lengths = []
default_bytes_lengths = []
max_calldata_bytes = 4096
invariant_depth = 10
frontier_ids = []
frontier_pcs = []
frontier_selectors = []
symbolic_call_targets = false
dump_smt = false
storage_layout = "solidity"

The same values can be set inline with NatSpec:

/// forge-config: default.symbolic.timeout = 120
/// forge-config: default.symbolic.array_lengths = [2, 4]
/// forge-config: default.symbolic.dynamic_lengths = { data = [3] }
/// forge-config: default.symbolic.default_bytes_lengths = [8]
/// forge-config: default.symbolic.exploration_order = "dfs"
/// forge-config: default.symbolic.invariant_depth = 6
function check_with_bounds(bytes memory data, uint256[] memory b) external {
    // ...
}

Common CLI and environment overrides:

forge test --symbolic
forge test --symbolic --symbolic-solver yices
forge test --symbolic --symbolic-solver cvc5
forge test --symbolic --symbolic-solver bitwuzla
forge test --symbolic --symbolic-solver-command "z3 -in -smt2"
forge test --symbolic --symbolic-solver-portfolio yices,z3
forge test --symbolic --symbolic-timeout 120
forge test --symbolic --symbolic-array-lengths 2,4
forge test --symbolic --symbolic-invariant-depth 6
forge test --symbolic --symbolic-call-targets
forge test --symbolic --symbolic-dump-smt

FOUNDRY_SYMBOLIC=true forge test
FOUNDRY_SYMBOLIC_SOLVER=z3 forge test --symbolic
FOUNDRY_SYMBOLIC_SOLVER_COMMAND="z3 -in -smt2" forge test --symbolic
FOUNDRY_SYMBOLIC_SOLVER_PORTFOLIO="yices,z3" forge test --symbolic
FOUNDRY_SYMBOLIC_TIMEOUT=120 forge test --symbolic

Known solver names are z3, yices, cvc5, cvc5-int, bitwuzla, and bitwuzla-abs. Unknown symbolic.solver values are treated as z3-compatible executables and are invoked with -in -smt2 to preserve the old symbolic.solver = "/path/to/z3" behavior. Use symbolic.solver_command for non-z3-compatible command lines or wrapper tools.

symbolic.solver_portfolio runs solvers in configured order with staged starts: the first entry starts immediately, the second starts shortly after if the query is still unresolved, and later entries are treated as rescue solvers. If a solver finishes without a decisive result and no other solver is running, the next pending entry starts immediately. The first sat response wins after its model is validated for model-producing queries. unsat responses are used only after all configured solvers that were needed to rule out sat have finished, and unknown results only win if no configured solver returns a decisive response. A nonempty symbolic.solver_command overrides both symbolic.solver_portfolio and symbolic.solver; otherwise a nonempty portfolio overrides symbolic.solver. Portfolio entries without whitespace, quotes, or backslashes are resolved like symbolic.solver values. Entries with whitespace, quotes, or backslashes are split into argv parts like symbolic.solver_command; they are not executed through a shell. For latency-sensitive local runs, start with a small portfolio such as ["yices", "z3"]. Broader portfolios can help on solver-diverse workloads but can still use more CPU and be slower when one fast solver already handles most queries. --symbolic-dump-smt prints each solver's configured order and launch delay with the per-query portfolio outcomes so solver mixes can be compared without changing execution semantics. It also prints an aggregate portfolio summary at the end of the run, for example:

--- symbolic solver portfolio summary ---
queries: 48
solver runs: 64
rescue solver runs: 0
not-started solver runs: 32
non-primary wins: 0
rescue wins: 0
cancelled after winner: 0
invalid models: 0
solver errors: 0
winner counts:
  yices-smt2 --bvconst-in-decimal: 48
launch counts:
  yices-smt2 --bvconst-in-decimal: 48
  z3 -in -smt2: 16
outcome counts:
  not-started: 32
  sat-valid: 32
  unsat: 32

Forge warns when a configured portfolio is degraded because one or more solver entries are not available, but it still uses the entries that can be invoked.

Security note: symbolic.solver_command, custom symbolic.solver values, and custom or command-like symbolic.solver_portfolio entries execute local programs when symbolic tests run. This also applies when these values come from inline forge-config: or translated legacy @custom:halmos annotations. Review solver settings before running symbolic tests from untrusted projects. Timeouts and portfolio cancellation terminate only the direct solver child process. Wrapper commands should forward termination to any subprocesses they spawn so descendant solvers do not outlive the cancelled query.

Halmos-style annotations are accepted as compatibility input and translated into the same internal config:

/// @custom:halmos --array-lengths 2,4 --width 32 --depth 256
function check_legacy(bytes memory a, bytes memory b) external {
    // ...
}

Supported compatibility flags are:

• --array-lengths
• --loop
• --width
• --depth
• --invariant-depth
• --solver-timeout
• --solver-timeout-branching
• --solver-timeout-assertion
• --solver
• --solver-command

Native forge-config: values win when both native and compatibility annotations set the same symbolic option.

SVM Compatibility Helpers

The executor recognizes a Halmos-style symbolic VM helper address:

address constant SVM_ADDRESS = address(0xF3993A62377BCd56AE39D773740A5390411E8BC9);

interface Svm {
    function createUint256(string calldata name) external returns (uint256);
    function createInt256(string calldata name) external returns (int256);
    function createBytes32(string calldata name) external returns (bytes32);
    function createAddress(string calldata name) external returns (address);
    function createBool(string calldata name) external returns (bool);
    function createBytes(string calldata name) external returns (bytes memory);
    function createBytes(uint256 length, string calldata name) external returns (bytes memory);
    function createString(string calldata name) external returns (string memory);
    function createString(uint256 length, string calldata name) external returns (string memory);
    function createBytes4(string calldata name) external returns (bytes4);
    function createCalldata(string calldata name) external returns (bytes memory);
    function enableSymbolicStorage(address target) external;
    function setArbitraryStorage(address target) external;
    function snapshotStorage(address target) external returns (uint256);
    function snapshotState() external returns (uint256);
}

Forge also treats several vm.random* cheatcodes as symbolic value creators when running symbolically. Dynamic byte and string creators use the same dynamic ABI bounds as function arguments.

How It Works

Forge drives the symbolic executor in these stages:

1. Compile and deploy contracts with the normal Foundry flow.
2. Execute setUp concretely, including fork-backed setup when the Forge executor is forked.
3. Classify check* and prove* functions as stateless symbolic tests, and invariant* or statefulFuzz* functions as symbolic invariant tests when --symbolic is enabled.
4. Build symbolic calldata from the Alloy ABI type model.
5. Execute bytecode in a standalone symbolic EVM, reading concrete code and setup state from the Foundry executor backend.
6. Store mutations in a symbolic world overlay instead of mutating the concrete executor.
7. Query the solver for branch feasibility and model extraction.
8. Replay any candidate counterexample through the concrete Foundry executor before reporting it.

The symbolic EVM is intentionally separate from revm's concrete interpreter. It uses Foundry and revm data structures for bytecode, accounts, environment, and backend reads, but symbolic execution needs its own expression values, memory, storage, call frames, path constraints, and solver integration.

Important internal pieces:

• SymbolicExecutor owns configuration and the solver backend.
• SymbolicRunInput describes one deployed test contract function to explore.
• SymbolicInvariantRunInput describes one bounded invariant sequence run.
• SymbolicRunResult and SymbolicInvariantRunResult return safe, counterexample, or incomplete outcomes.
• SymbolicWorld overlays balances, nonce, code, persistent storage, transient storage, logs, returndata, snapshots, and account lifecycle changes.
• CallFrame tracks address, code address, storage address, caller, call value, static context, calldata, stack, memory, and returndata.
• SymbolicSolver is the small internal trait used by the default SMT-LIB subprocess backend, which resolves named solvers (z3, cvc5, yices, bitwuzla, etc.) into solver-specific argv via solver_commands_for_config.

EVM And World Semantics

The executor models byte-precise calldata, memory, returndata, logs, storage, and symbolic storage keys. Supported behavior includes:

• arithmetic and bitwise operations, including symbolic-safe EXP, SIGNEXTEND, BYTE, shifts, and checked wrapping behavior
• CALLDATALOAD, CALLDATACOPY, CODECOPY, EXTCODECOPY, RETURNDATACOPY, MCOPY, MLOAD, MSTORE, and MSTORE8
• CALL, STATICCALL, DELEGATECALL, CALLCODE, CREATE, and CREATE2
• concrete and bounded symbolic call targets over known deployed contracts
• symbolic calldata and returndata across call frames
• SLOAD, SSTORE, TLOAD, and TSTORE with concrete or symbolic keys
• symbolic KECCAK256 terms for Solidity mapping and dynamic-array storage patterns
• concrete code and storage read from the normal Foundry setup backend, including fork-backed setup state
• balances, value transfer, nonce lifecycle, code hash, account existence, and pre-Cancun SELFDESTRUCT
• common concrete-input precompile cases
• block and transaction environment reads and supported environment cheatcodes

Unsupported symbolic constructs return an incomplete result with a Stuck reason instead of silently proving the property.

Known limitations

Unsupported constructs report Incomplete rather than a proof. Some supported semantics are bounded or approximate; in those cases, PASS only applies to the modeled semantics and configured bounds.

Known incomplete, bounded, or approximate surfaces include:

Exact failure messages are preserved in the test output, for example unsupported symbolic execution feature: GAS/gasleft() not modeled.

For real-world bug-shaped examples that exercise the current modeled surface, see the community-maintained symbolic-bug-suite. Those examples are written so a successful symbolic run reports a concrete counterexample.

Cheatcodes

Symbolic tests run through a symbolic cheatcode handler for the subset that can be modeled safely. The supported surface includes:

• vm.assume, vm.bound, vm.skip, vm.assumeNoRevert
• forge-std and DSTest assertion/failure signals
• warp, roll, fee, chainId, difficulty, coinbase, blockhash helpers
• deal, store, load, etch, getCode, getDeployedCode
• prank, startPrank, stopPrank
• addr, sign, deriveKey, rememberKey, rememberKeys
• env*, envOr*, envExists
• ffi, gated by Forge's existing --ffi setting
• console calls as no-ops
• logs and expectations such as recordLogs, getRecordedLogs, expectEmit
• call expectations and mocks for supported concrete and symbolic forms
• snapshots and state/storage helper calls used by symbolic tests

If a cheatcode is not modeled, the executor reports an incomplete symbolic run with a clear unsupported-feature reason.

Troubleshooting

No tests found for a check* or prove* function

check* and prove* are symbolic entrypoints, not normal Forge tests. They are discovered only when symbolic mode is enabled:

forge test --symbolic --match-test check_my_property

If Forge still prints No tests found in project! Forge looks for functions that start with test, check the following:

1. The binary was built from a revision that includes native symbolic test discovery. forge test --help should list --symbolic options, and the source should include the check* / prove* symbolic entrypoint path.

2. The file is under the current project's configured test or source paths and is compiled by this forge test invocation. A file outside the project, or outside the active profile's src / test paths, can compile in another project but will not be discovered here.

3. --match-test filters function names/signatures. Use --match-contract for contract names:

   shCopy

   forge test --symbolic --match-contract MySymbolicTest
   

PASS is surprising

First check whether the property depends on one of the known limitations above. A PASS is scoped to the current symbolic model and configured bounds; it does not cover skipped dynamic lengths, deeper invariant sequences, larger loop bounds, unmodeled gas behavior, arbitrary unknown external code, or cryptographic preimage/collision properties. If the property should have a counterexample within the modeled surface, reduce the example and try raising symbolic.max_paths, symbolic.max_depth, symbolic.max_solver_queries, or the relevant dynamic length / invariant depth settings.

Incomplete is not a proof

An incomplete run means the executor stopped before establishing safety or replaying a counterexample. To continue, adjust bounds, simplify the property, avoid the unsupported construct, or file a minimal repro for a missing model.

Results

At the crate boundary, symbolic execution returns:

• Safe: all explored paths completed without a feasible failure.
• Counterexample: the solver found a model for a failing path. Forge must replay this before reporting it to the user.
• Incomplete: execution stopped before a proof or replayed counterexample.

Incomplete runs carry a stop reason:

• Stuck: unsupported symbolic construct or configured width/depth/query limit.
• RevertAll: every explored path ended in an ordinary revert.
• Timeout: solver timeout or solver unknown.
• Error: backend, ABI, bytecode, or solver process failure.

Development Checks

Useful checks while changing this crate:

cargo fmt --check
cargo check -p foundry-evm-symbolic
cargo test -p foundry-evm-symbolic
cargo check -p forge
cargo test -p forge --test cli test_cmd::symbolic -- --nocapture
SYMBOLIC_CONFORMANCE=1 cargo test -p forge --test cli symbolic_conformance -- --nocapture
SYMBOLIC_LIMITS=1 cargo test -p forge --test cli symbolic_limits -- --nocapture

The conformance and limits suites are gated because they require Z3 and exercise broader, slower symbolic behavior. The limits suite intentionally checks resource boundaries such as path width, execution depth, calldata budgets, hard arithmetic, and invariant sequence depth.