Two of these three tools answer the same question. The third one does not, and that is the part worth paying for.
Slither and Aderyn read your contract and look for shapes they recognise. Echidna executes your contract a hundred thousand times and tries to break a rule you wrote yourself. The first two find nothing that is not already in a detector list. The third finds nothing you did not assert.
Feature tables do not make that concrete, so I put all three in front of the same contract with eight deliberate defects in it, one at a time, and recorded what each one said. It is the same method I used to separate unit, fuzz and invariant tests: inject a defect, run everything, and let the tools sort themselves out.
The short version: Slither found four of the eight, Aderyn three, Echidna four. No two of them overlap completely, and the three defects that were nothing but wrong arithmetic were invisible to both static analysers. The Foundry test suite that was already in the repository caught seven.
One contract, eight defects
The subject is a staking pool: deposit a token, accrue rewards at a fixed pool-wide rate, claim, withdraw, and an owner-only rescue path for ETH sent by mistake. It is 104 lines of Solidity. It is small enough to read and large enough to get wrong in interesting ways.
// examples/articles/slither-vs-aderyn-vs-echidna-which-smart-contract-tools-do-i-need/src/StakingPool.sol
/// @notice Move the reward index forward to the current block.
function accrue() public {
uint256 elapsed = block.timestamp - lastAccrual;
if (elapsed == 0) return;
lastAccrual = block.timestamp;
if (totalStaked == 0) return;
uint256 emitted = elapsed * rewardRate;
if (emitted > rewardBudget) emitted = rewardBudget;
rewardBudget -= emitted;
accRewardPerShare += (emitted * PRECISION) / totalStaked;
}
Eight variants exist, each one that file with exactly one textual substitution applied. Five of them are defects with a name — the kind that appears in an audit checklist and in a detector list:
| Defect | What changes |
|---|---|
| D1 | claim() pays the reward before writing rewardDebt, so a token callback can claim it again |
| D2 | onlyOwner compares tx.origin instead of msg.sender |
| D3 | stake() drops the boolean that transferFrom returns |
| D4 | the ETH rescue drops the success flag of its raw call |
| D5 | the reward index divides before scaling: (emitted / totalStaked) * PRECISION |
The other three are not patterns at all. They are arithmetic that is simply wrong:
| Defect | What changes |
|---|---|
| D6 | unstake() stops decrementing totalStaked |
| D7 | emergencyWithdraw() stops clearing stakeOf[msg.sender] |
| D8 | stake() stops resetting rewardDebt |
Each variant is generated as a throwaway project under tmp/, so the control file is never edited in place and an interrupted run cannot leave a mutant on disk. The harness refuses to start if the control's hash has moved.
Every defect is a real bug, not a stylistic complaint. Each one breaks at least one test that existed before the defect was written — the suite was written against the contract's intended behaviour, not against the mutations.
What ran, against what
Five layers ran against all nine versions of the contract:
forge test, unit and fuzz tests — eleven tests, one of them a 256-run fuzz testforge test, the invariant campaign — four properties, 64 runs at depth 64, so 4,096 calls per property- Slither 0.11.6,
slither . --filter-paths "test/|node_modules/" - Aderyn 0.6.8,
aderyn . --src src - Echidna 2.3.3 in property mode,
testLimit: 100000,seqLen: 100, fixed seed
Foundry is 1.5.1, solc is pinned to 0.8.30 with the optimizer on at 200 runs, and crytic-compile is 0.4.2. Slither is installed into a Python 3.12 virtualenv; Aderyn and Echidna are release tarballs extracted under /tmp, so nothing here touches the machine's own toolchain. The machine is an Apple M3 Pro, 12 logical CPUs, 36 GiB, Darwin 25.5.0 on arm64.
The whole matrix ran twice. All 45 cells agreed across the two passes, including the finding counts and the names of the failing properties.
The three tools read different things from the same file. Timings are medians over all nine versions of the contract across both passes.
The result
Green means the layer reported the injected defect. Identical in both passes.
As a table:
| Defect | forge test unit + fuzz |
forge test invariant |
Slither 0.11.6 | Aderyn 0.6.8 | Echidna 2.3.3 |
|---|---|---|---|---|---|
| D1 reentrancy | no | yes | yes | no | yes |
D2 tx.origin auth |
yes | no | no | yes | no |
| D3 unchecked ERC-20 return | yes | no | yes | yes | no |
| D4 unchecked low-level call | yes | no | yes | yes | no |
| D5 divide before multiply | yes | no | yes | no | no |
D6 totalStaked not reduced |
yes | yes | no | no | yes |
| D7 position not cleared | yes | yes | no | no | yes |
D8 rewardDebt not reset |
yes | yes | no | no | yes |
Three things fall out of that.
The two static analysers do not substitute for each other. Slither caught D1 and D5; Aderyn caught D2. Running both was the only way to get all five pattern defects, and neither one alone got more than four.
Neither static analyser saw D6, D7 or D8, and that is not a defect in either tool. There is no pattern to recognise. totalStaked -= amount is missing, and a line that is not there does not match anything.
Echidna and the Foundry invariant campaign returned exactly the same verdict on all eight defects, down to which named property broke. More on that below, because it is the part of the comparison that changes what you should install.
Correct code is not a quiet result
The control is the unmodified contract. It passes fifteen Foundry tests and all four Echidna properties. The static analysers do not treat it as clean.
Slither reported 16 findings over 102 detectors: four Medium, eleven Low, one Informational. Aderyn reported 14 instances over 88 detectors: one High and thirteen Low.
Both flagged the same thing at High or Medium, and they were right to. fund() calls transferFrom and then writes rewardBudget += amount, which is a state change after an external call:
// examples/articles/slither-vs-aderyn-vs-echidna-which-smart-contract-tools-do-i-need/src/StakingPool.sol
/// @notice Anyone may top up the reward budget.
function fund(uint256 amount) external {
if (amount == 0) revert ZeroAmount();
accrue();
bool received = token.transferFrom(msg.sender, address(this), amount);
if (!received) revert TransferFailed();
rewardBudget += amount;
}
Whether that is exploitable depends on whether the staking token can call back, which depends on which token the pool was deployed with — something neither tool can see. Aderyn calls it High severity. Slither calls it Medium and names the cross-function reentrancy it would enable. Both are reporting a real ordering, and both are leaving the judgment to you.
The rest is noise on correct code. Seven of Slither's sixteen are reentrancy-events, which fires whenever an event is emitted after a transfer. Four are timestamp, and three of those are about comparing a uint256 reward amount to zero rather than about time at all. Eleven of Aderyn's fourteen are state-change-without-event and unsafe-erc20-operation, the latter firing on every transfer and transferFrom in the file.
For context, forge lint on the same source reports seven diagnostics, all of them naming conventions and modifier size.
Trail of Bits' own program-analysis guide, which is the best short statement of how these tools are meant to fit together, describes Slither's false-alarm rate as "low" and Echidna's as "none". On this contract that ordering held exactly — Echidna raised nothing on correct code — but "low" still meant sixteen findings on 104 lines that had nothing wrong with them. That is the number that decides whether a team keeps running the tool.
Why each miss happened
Three of the misses looked like missing detectors and were not. Both tools ship the detector in question:
- Slither has
tx-originand it did not fire on D2 - Aderyn has
division-before-multiplicationand it did not fire on D5 - Aderyn has
reentrancy-state-change, fired it on the control, and did not fire it again on D1
So I wrote the same three defects several ways each in a single probe file and ran both tools over it.
// examples/articles/slither-vs-aderyn-vs-echidna-which-smart-contract-tools-do-i-need/probes/Phrasings.sol
modifier onlyOriginOwner() {
if (tx.origin != owner) revert NotOwner();
_;
}
function guardedByModifier() external onlyOriginOwner {
acc += 1;
}
function ifCustomError() external view {
if (tx.origin != owner) revert NotOwner();
}
The results are unambiguous.
| Phrasing | Slither | Aderyn |
|---|---|---|
tx.origin inside a modifier |
no | yes |
tx.origin in a function body, if + custom error |
yes | yes |
tx.origin in a function body, if + revert string |
yes | yes |
require(tx.origin == owner) |
yes | yes |
require(!(tx.origin != owner)) |
yes | yes |
(a / b) * c |
yes | no |
a / b * c |
yes | yes |
| division and multiplication in two statements | yes | no |
| state write after a call in the same function | yes | yes |
| state write after a call made by a private helper | yes | no |
Slither found tx.origin in four of the five places it appears and missed exactly one: the modifier. That is the one place a real contract puts it. OpenZeppelin's Ownable wraps the owner check in a modifier onlyOwner(), and so does everything that copies it.
Aderyn's division detector matched a / b * c and neither (a / b) * c nor the two-statement form. Adding parentheses hides it. Its reentrancy detector matched a state write after a call in the same function and not after a call made through a private helper, which is why it saw fund() and not the injected claim().
That is the useful way to read a static analyser's detector list. A detector is a pattern, and the question is never "does the tool cover reentrancy" but "does the tool cover reentrancy written the way I write it". Both tools are open about being pattern matchers; neither is going to tell you which phrasings it matches. A probe file takes twenty minutes and answers it for your own codebase.
What Echidna found, and what it cost
Echidna needs properties. Before it can say anything at all, you write them.
// examples/articles/slither-vs-aderyn-vs-echidna-which-smart-contract-tools-do-i-need/test/PoolProperties.sol
/// P1: the pool's own total agrees with the sum of the positions it tracks.
function echidna_totalStakedMatchesSumOfStakes() public view returns (bool) {
return pool.totalStaked() == sumOfStakes();
}
/// P2: the pool always holds at least the principal it owes.
function echidna_poolHoldsAtLeastThePrincipal() public view returns (bool) {
return token.balanceOf(address(pool)) >= pool.totalStaked();
}
/// P3: no account gets more principal back than it put in.
function echidna_principalOutNeverExceedsPrincipalIn() public view returns (bool) {
return principalOut <= principalIn;
}
/// P4: rewards handed out never exceed rewards released from the budget.
function echidna_rewardsNeverExceedEmission() public view returns (bool) {
return rewardsPaid() <= int256(emitted());
}
Those four lines of predicate are the easy part. Around them sit the harness that deploys the pool, three actor contracts so that msg.sender differs between positions, ghost counters that track principal in and out, and bounded action wrappers so a random uint256 becomes a stake somebody can actually afford. That comes to 112 lines of Solidity against a 104-line contract, and the actors needed a specific design decision: the token notifies its recipient, and the actor re-enters claim() once when it is paid.
// examples/articles/slither-vs-aderyn-vs-echidna-which-smart-contract-tools-do-i-need/test/PoolActor.sol
function onTokensReceived(address, uint256) external {
if (reentering) return;
reentering = true;
try pool.claim() {} catch {}
reentering = false;
}
Without those six lines, Echidna does not catch D1. The reentrant path does not exist in the harness, so no sequence of calls reaches it. That is the honest shape of the tradeoff: a fuzzer explores the state machine you built for it, and an assumption you left out of the harness is an assumption it will never question.
With them, it found D1, D6, D7 and D8, and the counterexamples are small. This is the full output for D7, the variant where emergencyWithdraw() stops clearing the position:
echidna_totalStakedMatchesSumOfStakes: failed!💥
Reason: ReturnFalse
Call sequence:
PoolProperties.stake(0,1)
PoolProperties.emergencyWithdraw(0)
Stake one wei, withdraw it, and the pool's own total no longer matches the position it still thinks you hold. Two calls, arguments of 0 and 1. Nothing about that needs interpreting.
Echidna against Foundry's own invariant runner
The comparison that actually decides whether you install Echidna is not against Slither. It is against the invariant runner you already have.
So I wrote the Foundry campaign to assert the same four properties over the same three actor contracts, with the only difference being that Foundry advances the clock with a cheatcode where Echidna varies the block timestamp itself. The shape of that harness — bounded handlers, ghost counters, actors that are their own contracts — is the one I described in writing useful invariant tests in Foundry.
The two engines agreed on every defect, and on every property.
| Defect | Properties Echidna broke | Invariants Foundry broke |
|---|---|---|
| D1 | poolHoldsAtLeastThePrincipal, rewardsNeverExceedEmission |
the same two |
| D6 | totalStakedMatchesSumOfStakes, poolHoldsAtLeastThePrincipal |
the same two |
| D7 | all three of the above | the same three |
| D8 | poolHoldsAtLeastThePrincipal, rewardsNeverExceedEmission |
the same two |
Echidna spent just over 100,000 calls per variant to get there. Foundry spent 4,096 per property. Neither budget was the binding constraint; these defects break on the second or third call.
The one place they differ is triage. Both shrink the failing sequence to two to five calls. Only Echidna shrinks the arguments. Foundry's shrunk sequence for the same D7 failure is four calls carrying values like 188761063236431826885024299680960098228084573266989535263471, which is a perfectly valid counterexample and a worse thing to read at the top of a failing CI log.
This is where I would be careful about generalising. One contract, one property set, two engines that happen to agree. It does not show that Echidna's generation strategy is equivalent to Foundry's on a harder state machine. What it does show is that on a property set you can write in an afternoon, the tool you already have got the same answer, and the second tool's contribution was a more readable counterexample.
Echidna ships a foundry test mode that discovers invariant_-prefixed Solidity tests, which sounds like it would make this a one-line experiment. It is not a drop-in.
Pointed at the same StakingPoolInvariantTest at three fixed seeds and 20,000 calls each, --test-mode foundry discovered all four invariant functions and reported all four as passing — on the control, and on D7, where the position is never cleared and the Foundry runner breaks three of those same four. It does not honour StdInvariant.targetContract, so with the test contract as its only entry point there is nothing state-changing left to call.
Adding --all-contracts gives it entry points and then it fails on correct code: in three runs out of three against the control it broke at least one property, because the handler and the mock token become directly reachable and the ghost counters behind those properties only mean anything when the handler is driving.
The overlap between the two engines is real at the level of properties. It is not there at the level of harnesses, and rewriting the harness is most of those 112 lines.
Echidna can report a green run having executed nothing
This is the one to know about before you put Echidna in front of anything.
The fixture originally set bytecode_hash = "none" in foundry.toml, which is a normal thing to do when you want reproducible artifacts. Against that build, Echidna 2.3.3 crashed all four workers with Set.elemAt: index out of range — and then printed every property as passing, reported Total calls: 0, and exited 0.
Eight lines reproduce it:
// examples/articles/slither-vs-aderyn-vs-echidna-which-smart-contract-tools-do-i-need/probes/ImmutableCrash.sol
contract Imm {
Inner public immutable inner;
constructor() {
inner = new Inner();
}
function bump() public {
inner.bump();
}
function echidna_lt100() public view returns (bool) {
return inner.x() < 100;
}
}
The 2x2 is clean:
| Target contract | bytecode_hash |
Workers crashed | Calls | Property | Exit code |
|---|---|---|---|---|---|
immutable |
none |
4 | 0 | passing | 0 |
immutable |
ipfs |
0 | 404 | failed | 1 |
| mutable | none |
0 | 505 | failed | 1 |
| mutable | ipfs |
0 | 404 | failed | 1 |
Only the first row misbehaves, and it misbehaves in the worst available direction. A CI job that checks the exit code goes green having fuzzed nothing. The fix is either to drop immutable from the Echidna target contract or to leave the metadata hash at its default, which is what this fixture now does — but the lesson generalises past this particular bug. Assert on the call count, not on the exit code.
Setup effort, measured
| Slither 0.11.6 | Aderyn 0.6.8 | Echidna 2.3.3 | |
|---|---|---|---|
| Install | 47 Python packages in a virtualenv | one binary from a release tarball | one binary, plus crytic-compile |
| On disk | 50 MB | 20 MB | 137 MB |
| Needs the project to compile | yes, runs forge clean and forge build itself |
no | yes, through crytic-compile |
| Solidity you write first | none | none | 112 lines |
| Median run on this contract | 360 ms | 190 ms | 18.5 s |
| Exit code on the control | 255 | 0 | 0 |
| Exit code on every defective variant | 255 | 0 | 1 when a property broke |
Aderyn is the one that needs nothing. Its README promises it "runs without need for any configuration" on Foundry and Hardhat projects, and it undersells itself: it parses Solidity on its own, with no compiler and no build directory. I pointed it at two loose .sol files in an empty directory with no foundry.toml and it produced the same five issue groups. That is a genuinely different operating model from Slither, which deletes your build and recompiles the project before it will say anything, and it is most of why it runs in half the time.
The exit codes are the part that matters for CI, and neither static analyser's is usable as shipped. Slither exits 255 on the clean contract, because sixteen informational and low findings are still findings; only --fail-none returns 0. Aderyn exits 0 with a High-severity finding on the table, --highs-only does not change that, and version 0.6.8 has no flag that does. One is always red and the other is always green. Both need a wrapper that reads the JSON report and decides for itself, which is the same conclusion I reached about static analysis in a Solidity CI pipeline.
One more dependency is worth naming. Echidna's README says it is "powered by Slither", and it means it literally. Run Echidna with crytic-compile on the path but no slither binary and it prints:
WARNING: slither not found. Echidna uses Slither (https://github.com/crytic/slither) to perform source analysis, which makes fuzzing more effective. You should install it with 'pip3 install slither-analyzer --user'
It runs anyway. But the fuzzer's own recommended setup includes the static analyser, which is a fair answer to any framing that treats the two as alternatives.
What I would actually run
Start with what you already have. forge lint needs no installation and caught three of the eight — D3, D4 and D5 — on Foundry 1.5.1. The Foundry test suite caught seven of the eight, and the invariant campaign caught the same four Echidna did. When I ran one contract through a nine-gate release ladder, the thing missing from that matrix was static analysis; this is the measurement that fills the gap.
Add both static analysers next. They cost nothing to run — under a second between them — and they were the only layers that reported D1 and D2 without a test or a property having to be written first. Running only one leaves a hole, and which hole depends on which one you drop.
Turn the noise down on the day you add them, before the sixteen-findings-on-clean-code problem turns the step into one everybody skips. Slither takes --exclude reentrancy-events,timestamp on the command line, which brings the control from 16 findings to 5. Aderyn takes a [detectors] exclude list in the aderyn.toml that aderyn init writes; excluding unsafe-erc20-operation and state-change-without-event leaves 3 instances from 86 detectors. Put the exclusion list in the repository, with a comment for each entry saying why.
Echidna I would reach for second, not first, and for a specific reason rather than a general one: a second engine over properties you have already written in Foundry, when the contract is valuable enough that a disagreement between two fuzzers is worth knowing about. Its counterexamples are meaningfully easier to read. It did not find anything here that the invariant runner in the repository did not.
And the thing none of them replace is the properties themselves. The three defects that were pure arithmetic — a missing decrement, a position that is never cleared, a debt that is never reset — were invisible to 190 detectors between the two static analysers, and obvious within two calls to anything that checked whether the pool's books balanced. Writing that check down is the work. Which engine runs it is a smaller decision than it looks.
What this does not show
One contract, 104 lines, one property set, one machine, one release of each tool. The defect set is eight injections I chose, and choosing them is a judgment about what typical bugs look like, not a sample of anything.
The counts are not scores. "Slither found four and Aderyn three" is a fact about these eight defects; a different eight would order them differently, and D2 alone would have flipped the ranking if I had written the tx.origin check in a function body instead of a modifier — which is exactly the point of the phrasing probe.
Aderyn's release cadence deserves a note. Version 0.6.8 is from January 2026 and the repository was still being pushed to in September; whatever has landed on the development branch since is not in the binary I measured.
The Foundry and Echidna campaigns used fixed seeds and both passes agreed, but fuzzing verdicts near the edge are not reproducible from a seed in general, and none of these defects was near the edge. A harder bug would need the campaign repeated many times before any of these cells could be quoted as a verdict rather than as one observation.
The harness, the fixture, the mutation catalogue and every raw result are in examples/articles/slither-vs-aderyn-vs-echidna-which-smart-contract-tools-do-i-need/.