feat(symbolic): add native symbolic testing#14796
Merged
Merged
Conversation
* test(symbolic): add fuzzer/standard-lib parity tests Adds 23 CI-bounded symbolic-execution parity tests against canonical benchmark corpora (Echidna, Medusa, ItyFuzz, devdacian, crytic/properties, Halmos examples, OpenZeppelin patterns) plus engine-capability checks for new opcodes. All tests gated on z3_available(); total wall ~43s in parallel. Amp-Thread-ID: https://ampcode.com/threads/T-019e3ae3-f6f9-76f0-86a0-845a6f893516 Co-authored-by: Amp <amp@ampcode.com> * test(symbolic): convert parity tests to snapbox snapshots Replaces `stdout_lossy() + contains()` assertions with `stdout_eq(str![[...]])` snapshots for all 23 symbolic parity tests. - Adds two helpers in the test module: - `assert_symbolic` redacts `[METRICS]` (paths/queries counts) and `[SENDER]` (symbolic invariant sender addresses). - `assert_symbolic_witness` adds `[CALLDATA]` and `[ARGS]` (with one level of nested scientific-notation brackets) for tests whose counterexample witnesses Z3 chooses freely. - Uses `sh_eprintln` in `skip_unless_z3!` to satisfy the disallowed-macro clippy lint. Amp-Thread-ID: https://ampcode.com/threads/T-019e3ae3-f6f9-76f0-86a0-845a6f893516 Co-authored-by: Amp <amp@ampcode.com> * test(symbolic): trim parity snapshots with ellipsis wildcards Replaces the repeated compile-header and pre-"Failing tests:" duplicated counterexample line in each snapshot with a single `...` multi-line wildcard from snapbox. Passing tests keep just `Ran 1 test for ...` and the `[PASS] ...` line; failing tests keep from `Failing tests:` to the `forge test --rerun` tip. Amp-Thread-ID: https://ampcode.com/threads/T-019e3ae3-f6f9-76f0-86a0-845a6f893516 Co-authored-by: Amp <amp@ampcode.com> * test(symbolic): split parity corpora * test(symbolic): align kevm snapshot with trim convention The split-out kevm test ended the snapshot at `Suite result: ok. ...; finished in [..]`, but the global `[ELAPSED]` redaction rewrites `finished in <n>s` to literal `[ELAPSED]`, so the assertion never matched. Replace the trailing line with the same `...` multi-line wildcard the other parity snapshots use. Amp-Thread-ID: https://ampcode.com/threads/T-019e3ae3-f6f9-76f0-86a0-845a6f893516 Co-authored-by: Amp <amp@ampcode.com> * test(symbolic): consolidate parity tests under symbolic_parity/ mod - Move the 12 `symbolic_parity_*.rs` files into a `symbolic_parity/` subdirectory with a single `mod symbolic_parity` registration. Mirrors the existing `invariant/` layout. - Re-export `assert_symbolic` and `assert_symbolic_witness` from `symbolic_parity::mod` so corpus submodules can `use super::*` instead of reaching into `crate::test_cmd::symbolic_helpers`. - Add the missing snapshot assertions for hevm, manticore, scribble, and swc. These were checking only the failure exit code; now they assert the trimmed snapbox snapshot the rest of the corpus uses. Amp-Thread-ID: https://ampcode.com/threads/T-019e3ae3-f6f9-76f0-86a0-845a6f893516 Co-authored-by: Amp <amp@ampcode.com> * fix(symbolic): make manticore parity test actually exercise the engine The previous snapshot showed: [FAIL: failed to set up invariant testing environment: No contracts to fuzz.] That's a wiring bug, not a real `Manticore`-style multi-tx exploration: the test contract held both `arm()` and `invariant_neverArmed()` in the same contract, didn't inherit `forge-std/Test`, and had no `setUp` / `targetContract` call, so the invariant runner had no fuzzable target. Split the target out into a separate `ArmTarget` contract and register it via `targetContract`. The engine now actually shrinks the symbolic sequence to a single `arm(0xfeed)` call. Amp-Thread-ID: https://ampcode.com/threads/T-019e3ae3-f6f9-76f0-86a0-845a6f893516 Co-authored-by: Amp <amp@ampcode.com> * test(symbolic): align parity tests with upstream challenges - devdacian rarely-false: port to canonical (n + 1234) % 2**80 == 0 - halmos minivat: rename trivial test to linear_smoke_parity and add canonical Fundamental Equation of DAI invariant as ignored regression (engine gap: nonlinear bv-mul symbolic*symbolic) - erc20 approve race: tighten comment to reflect hardcoded sequence Co-authored-by: grandizzy <38490174+grandizzy@users.noreply.github.com> Amp-Thread-ID: https://ampcode.com/threads/T-019e3ae3-f6f9-76f0-86a0-845a6f893516 Co-authored-by: Amp <amp@ampcode.com> * Update crates/forge/tests/cli/test_cmd/symbolic_parity/halmos.rs Co-authored-by: figtracer <me@figtracer.com> --------- Co-authored-by: Amp <amp@ampcode.com> Co-authored-by: Derek <256792747+decofe@users.noreply.github.com> Co-authored-by: figtracer <me@figtracer.com>
Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com>
* feat(symbolic): support SMT solver selection * fix: address grandizzy's comments * fix: improve symbolic solver portfolio performance * fix(symbolic): validate portfolio solver choices Amp-Thread-ID: https://ampcode.com/threads/T-019e4487-e080-741d-b8ab-62d5aa43573a Co-authored-by: Amp <amp@ampcode.com> * fix(symbolic): avoid impossible mapping storage aliases Amp-Thread-ID: https://ampcode.com/threads/T-019e4487-e080-741d-b8ab-62d5aa43573a Co-authored-by: Amp <amp@ampcode.com> * chore(symbolic): remove local solver version aliases Amp-Thread-ID: https://ampcode.com/threads/T-019e4487-e080-741d-b8ab-62d5aa43573a Co-authored-by: Amp <amp@ampcode.com> * chore(symbolic): drop versioned solver aliases Amp-Thread-ID: https://ampcode.com/threads/T-019e4487-e080-741d-b8ab-62d5aa43573a Co-authored-by: Amp <amp@ampcode.com> * test(symbolic): snapshot erc20 storage regression Amp-Thread-ID: https://ampcode.com/threads/T-019e4487-e080-741d-b8ab-62d5aa43573a Co-authored-by: Amp <amp@ampcode.com> --------- Co-authored-by: Amp <amp@ampcode.com>
* chore(symbolic): share builtin solver registry Amp-Thread-ID: https://ampcode.com/threads/T-019e4487-e080-741d-b8ab-62d5aa43573a Co-authored-by: Amp <amp@ampcode.com> * feat(symbolic): report portfolio solver outcomes Amp-Thread-ID: https://ampcode.com/threads/T-019e4487-e080-741d-b8ab-62d5aa43573a Co-authored-by: Amp <amp@ampcode.com> * feat(symbolic): warn on degraded solver portfolios Amp-Thread-ID: https://ampcode.com/threads/T-019e4487-e080-741d-b8ab-62d5aa43573a Co-authored-by: Amp <amp@ampcode.com> * chore(symbolic): fix portfolio diagnostics clippy Amp-Thread-ID: https://ampcode.com/threads/T-019e4487-e080-741d-b8ab-62d5aa43573a Co-authored-by: Amp <amp@ampcode.com> * docs(symbolic): document solver portfolio helpers --------- Co-authored-by: Amp <amp@ampcode.com>
Amp-Thread-ID: https://ampcode.com/threads/T-019e4487-e080-741d-b8ab-62d5aa43573a Co-authored-by: Amp <amp@ampcode.com>
* feat(symbolic): summarize portfolio diagnostics Amp-Thread-ID: https://ampcode.com/threads/T-019e4487-e080-741d-b8ab-62d5aa43573a Co-authored-by: Amp <amp@ampcode.com> * Address symbolic portfolio diagnostics review Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com> * Fix transaction request clippy warning Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com> * Revert "Fix transaction request clippy warning" This reverts commit 884799d. * Allow transaction request enum size lint Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com> * Disambiguate portfolio diagnostics re-export Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com> * Use enum for solver outcomes Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com> --------- Co-authored-by: Amp <amp@ampcode.com>
Defer symbolic diagnostics during progress output Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com>
Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com>
* feat(symbolic): adapt portfolio scheduling Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com> * fix(symbolic): tighten adaptive portfolio scoring Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com> * refactor(symbolic): name portfolio scheduler signals Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com> * fix(symbolic): clarify query progress limit Co-authored-by: Amp <amp@ampcode.com> Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 --------- Co-authored-by: Amp <amp@ampcode.com>
* feat(symbolic): configure exploration order Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com> * fix(symbolic): default exploration order when omitted Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com> * fix(symbolic): apply exploration order to local batches Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com> --------- Co-authored-by: Amp <amp@ampcode.com>
) Promotes scattered magic numbers and named constants spread across executor.rs, solver.rs, evm.rs, memory.rs, state.rs and precompiles.rs into a single `crates/evm/symbolic/src/consts.rs` module. All previous call-sites pick the constants up through the existing use `super::*` / `pub(crate) use consts::*` re-export chain, so no public API changes.
* refactor(symbolic): consolidate constants into a `consts` module Promotes scattered magic numbers and named constants spread across executor.rs, solver.rs, evm.rs, memory.rs, state.rs and precompiles.rs into a single `crates/evm/symbolic/src/consts.rs` module. All previous call-sites pick the constants up through the existing use `super::*` / `pub(crate) use consts::*` re-export chain, so no public API changes. * refactor(symbolic): split symbolic test file by feature Splits the monolithic symbolic.rs (~7800 lines, ~150 tests) into focused files grouped by the EVM feature they exercise: - symbolic.rs: basic flags, core behavior, arrays, invariants - symbolic_opcodes.rs: byte/signextend, shift, exp - symbolic_memory.rs: mload/mstore/sha3/log/returndatacopy/mcopy - symbolic_calls.rs: calldataload/copy, external/static/delegate/callcode - symbolic_creates.rs: create, create2, nonce, vm.expectCreate - symbolic_storage.rs: mapping, packed, ERC-20 storage, svm helpers - symbolic_precompiles.rs: hash, identity, advanced precompile coverage - symbolic_cheatcodes.rs: all vm.* cheatcode tests No test logic changes; all symbolic CLI tests are preserved. --------- Co-authored-by: Amp <amp@ampcode.com>
Co-authored-by: Amp <amp@ampcode.com> Co-authored-by: Mablr <59505383+mablr@users.noreply.github.com>
* refactor(symbolic): split executor into modules Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com> * ci: skip tempo network checks without rpc secrets Amp-Thread-ID: https://ampcode.com/threads/T-019e3bf2-923d-727e-82f5-40ca3e956694 Co-authored-by: Amp <amp@ampcode.com> * Revert "ci: skip tempo network checks without rpc secrets" This reverts commit af8e942. --------- Co-authored-by: Amp <amp@ampcode.com>
…um` (#14898) Introduces `SolverConfigError` with `EmptyCommand` and `UnterminatedQuote(char)` variants, replacing all `Result<T, String>` in the solver command-building path. Also tightens `split_quoted_args` to return the offending `char` directly instead of a pre-formatted string, letting callers own the message context.
…olic-testing # Conflicts: # crates/forge/src/result.rs # crates/forge/src/runner.rs
* test: snapshot symbolic CLI output checks * fix: satisfy clippy on symbolic test branch * Update crates/forge/tests/cli/test_cmd/symbolic_helpers.rs Co-authored-by: Mablr <59505383+mablr@users.noreply.github.com> --------- Co-authored-by: grandizzy <38490174+grandizzy@users.noreply.github.com> Co-authored-by: Mablr <59505383+mablr@users.noreply.github.com>
* feat(symbolic): add tracing to executor and solver Spans added: - `symbolic_path` (`completed_paths`, `worklist_size`): wraps each worklist iteration in `run.rs` - `symbolic_step` (`pc`, `op`): wraps each `step()` call, nested under `symbolic_path` - `jumpi_branch` (`pc`, `dest`): wraps the symbolic `JUMPI` fork block in `opcodes.rs` - `solver_query` (`query_id`, `constraint_count`, `kind`): wraps `is_sat`/`model` calls in `solver.rs` Events added: - trace per path pop and per solver query entry - debug at path/depth limit exhaustion and final safe/revert-all outcome - debug before counterexample model materialization - debug (with `constraint_count`) on invalid solver model * fix: add missing tracing spans to `execute_sequence_call`
* refactor(common): extract wallet helpers Move `derive_key_path`, `derive_private_key<W>`, `derive_private_key_with_language`, and `private_key_from_u256` from `foundry-evm-symbolic` into `foundry-common` so that both `foundry-cheatcodes` and `foundry-evm-symbolic` share a single impl. * fix: enable `mnemonic-all-languages`
grandizzy
previously approved these changes
May 29, 2026
grandizzy
left a comment
grandizzy
left a comment
Collaborator
There was a problem hiding this comment.
approving with the mention this is MVP and should be treated as such
figtracer
force-pushed
the
mattsse/native-symbolic-testing
branch
from
4dfff5a to
f7e563e
Compare
Amp-Thread-ID: https://ampcode.com/threads/T-019e645e-97a2-757f-adc7-2c765700d18d Co-authored-by: Amp <amp@ampcode.com>
…olic-testing # Conflicts: # crates/config/src/lib.rs # crates/forge/src/cmd/test/mod.rs # crates/forge/src/multi_runner.rs # crates/forge/src/runner.rs # crates/forge/tests/cli/config.rs
…olic-testing Amp-Thread-ID: https://ampcode.com/threads/T-019e8dcf-7563-749b-8e51-5f370b1d2052 Co-authored-by: Amp <amp@ampcode.com>
# Conflicts: # crates/forge/src/multi_runner.rs # crates/forge/src/runner.rs
grandizzy
previously approved these changes
Jun 4, 2026
figtracer
changed the title
* try validated hard-arithmetic fallback before SMT for satisfiable is_sat queries
Result: {"status":"keep","metric":1208,"build_ms":3751,"counterexample_lines":8,"run1_ms":4219,"run2_ms":1208,"run3_ms":1196,"total_wall_ms":6677,"total_ms":1208}
* fold constant BoolExpr comparisons during construction
Result: {"status":"keep","metric":1187,"build_ms":3527,"counterexample_lines":8,"run1_ms":4476,"run2_ms":1187,"run3_ms":1182,"total_wall_ms":6894,"total_ms":1187}
* preallocate SMT query buffer based on constraint count
Result: {"status":"keep","metric":1178,"build_ms":3255,"counterexample_lines":8,"run1_ms":4767,"run2_ms":1178,"run3_ms":1171,"total_wall_ms":7166,"total_ms":1178}
* preallocate normalized solver cache-key vector
Result: {"status":"keep","metric":1175,"build_ms":4637,"counterexample_lines":8,"run1_ms":4918,"run2_ms":1174,"run3_ms":1175,"total_wall_ms":7317,"total_ms":1175}
* normalize solver constraint batches by flattening and deduplicating top-level conjuncts
Result: {"status":"keep","total_ms":1190,"build_ms":8581,"counterexample_lines":8,"run1_ms":4718,"run2_ms":1180,"run3_ms":1190,"total_wall_ms":7140,"min_ms":1180,"mean_ms":2363,"max_ms":4718,"symbolic_paths":31,"symbolic_queries":48,"symbolic_smt_queries":48,"symbolic_sat_queries":50,"symbolic_sat_cache_hits":6,"symbolic_model_queries":4,"symbolic_model_cache_hits":0,"symbolic_hard_arith_witnesses":0,"symbolic_solver_ms":714}
* Simplify repeated symbolic AND masks
* fix(forge): run symbolic-only check tests
* short-circuit direct symbolic contradictions before SMT
* reuse validated symbolic solver cache results
* fix symbolic solver fallback review issues
mablr
approved these changes
Jun 8, 2026
grandizzy
approved these changes
Jun 8, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
5 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Adds native symbolic testing to Forge behind
forge test --symbolic.This introduces a Foundry-owned symbolic EVM executor, Z3-backed solving, symbolic ABI input generation, bounded stateless
check*/prove*tests, bounded symbolic invariant sequences, Foundry config / CLI integration, and concrete replay before counterexamples are reported.Preview Semantics
This is an opt-in MVP preview, not a complete formal verification engine.
Symbolic results are scoped to the currently modeled EVM semantics and configured bounds:
PASS: no feasible failure was found in the explored, modeled state space.FAILwith counterexample: the solver found a model and Forge replayed it concretely before reporting it.FAIL: incomplete symbolic execution: the run hit an unsupported feature, solver limit, timeout, unknown result, or non-replaying model.Unsupported or unsafe-to-model behavior is intended to fail closed as
Incompleterather than silently passing.User Impact
Users can write ordinary Forge-style Solidity tests and run:
forge test --symbolic