A concolic tracer for the EVM. It runs your contracts for real in revm, with real state and real cheatcodes. Next to every value it keeps a symbolic expression over the inputs, and it records every branch condition. Then it flips a branch nobody has taken, asks an SMT solver (z3 or bitwuzla) for inputs that take it, and runs again.
Fuzzers guess, and they rarely hit x == 0x5eed1e55, a narrow arithmetic window or a chain of requires.
Symbolic tools reason about every path from the start, and they stall in deep protocols. concolity sits between the
two: it runs as fast as a fuzzer and solves one branch at a time.
Branches are reported in Solidity, by line and AST node, through sol-debug's source maps (the Foundry runner, a crate of this repository). Every solved input is a call sequence that replays in the debugger and becomes a Foundry test. It also runs on Huff and on bare bytecode, where it reports by pc.
The design follows the ConcolicTracer of The Fuzzing Book,
moved from Python values into the EVM interpreter. It works on bytecode; source maps and the AST only add names.
Start with docs/USAGE.md (every command, what each outcome means, what it catches today). The Claude Code skill is skills/concolity/SKILL.md; findings in the editor through solidity-language-server are designed in docs/LSP.md.
Read ARCHITECTURE.md, DESIGN.md, ROADMAP.md (the rest of the toolkit), COMMON_SOLIDITY_BUG.md (the bug classes, and which tool catches each), HUNTING.md (the hunting log: leads, bytecode oracles, fidelity lessons), and the first case study: Async Swap's unreachable guards.
Status: the EVM model runs (EVM-MODEL.md): revm executes, every opcode's result gets its symbolic term, every step is checked against revm, and z3 solves flipped branches. On the book's triangle every branch flips to an input that takes the other side. Next: the trace tree, so it explores on its own.
cargo install --path . # `concolity` in ~/.cargo/bin; brew install z3 for explore
cargo test --release # needs z3 on PATH
concolity coverage <project> [--skip <path part>] [--include src/] [--fuzz-runs 32] [--fast]
[--lcov lcov.info] [--bindings] [--against-forge forge-test.json]
- solc with the project's own settings (optimizer included), so it measures the bytecode that ships. forge
coverage recompiles with the optimizer off.
--fastdoes the same, for speed. - In parallel batches. solc uses one core, and on a real suite its cost is in the test files: on
asyncswap/contracts,
src/alone takes 1.8 s, one test file 4.7 s, and all 125 together 70 s. So the test files are split into one batch per core. Each worker compiles its batch and runs the test contracts its files define. Only what's needed is requested:evm.deployedBytecode.opcodesalone cost about 20 s of 97. - Cached in
~/.cache/formalmind/solc/, per batch, keyed by every.solfile, so an unchanged rerun skips solc. - The tests run in revm, on sol-debug's runner and cheatcodes. Each test, and each fuzz run, starts from the state
after
setUp. - Lines as forge counts them: where each statement starts, and function headers for entry code. JUMPI
sides count every conditional jump in the shipped bytecode, including overflow checks, call-failure checks and
&&/||. forge's "% Branches" counts source branches, so the two differ on purpose. - Bindings first. Every call site, and what ran at its target. A call into an account with no code at a fixed address is missing bytecode: whatever is behind that call is unreachable, and the code didn't choose that. Sites whose empty targets came from the inputs (a fuzzed ERC-1271 signer, a fuzzed token) are listed apart.
--against-forgetakesforge test --jsonoutput for the same suite and lists every test where the two verdicts differ. forge is the oracle, so each one is a runner bug until shown otherwise.
On asyncswap/contracts at 3295d4d (125 test files, 850 tests, optimizer_runs = 43_690, 10 cores):
| forge coverage | concolity coverage | |
|---|---|---|
| time | 65 s | 48 s cold, 29 s with the cache |
| lines | 99.90% (966 / 967) | 99.9% (931 / 932): the 35 fewer lines are code the optimizer removes |
| what it measures | unoptimized build | the optimized bytecode that ships |
verdicts against forge test |
– | 836 of 836 identical, 0 disagreements |
Skipped, with the reason in the report: invariant campaigns (invariant_*, no campaign runner yet), forks inside
tests (createFork: forge forks the live chain there), and tests foundry.toml's match_test / no_match_test
filters exclude. expectCall is accepted but not checked. A failing fuzz test reports its counterexample as --arg
values for concolity debug.
The 48 disagreements on the way to 0 were all runner bugs, found by --against-forge and diagnosed with
concolity debug. The biggest one: forge runs each of a test contract's top-level calls as its own transaction, so
transient storage is cleared between them (Async Swap's pending-match slot, set while placing an order, survived into
matchBook). That one rule fixed 39 tests.
foundry's testdata/default/cheats (v1.8.6, one or more files per cheatcode) is the reference suite: forge 1.8.6's
verdicts on it are the oracle, compared with --against-forge. On 2026-10-24: 520 tests pass here (forge: 812
pass, 16 fail, 10 skip of 838), with 298 disagreements left. State diffs (startStateDiffRecording,
stopAndReturnStateDiff, getStateDiff(Json), named and decoded from the storage layout) match all 34 of forge's
tests. What remains, largest first: arbitrary storage, Ed25519 keys, EIP-7702 delegations,
dumpState, broadcastRawTransaction / executeTransaction, mapping storage hooks, the expectRevert count and
reverter variants, blob hashes, getChain, and chain-specific cheatcodes (Tempo, Monad).
concolity debug <project> <test file> Contract::test [summary|lines|revert|writes|step] [--n N] [--var x] [--function f] [--text]
JSON answers about one run (sol-debug's agent module):
summary: outcome, decoded revert, calls, named writes, missing bytecode;lines: the Solidity lines that ran, with their effects.--textprints the simple line view people read;revert: where, through which calls, and the comparison that failed, with its operands;writes: storage writes by variable;step --n N: one step in full.
Part of Formal Mind.
MIT