Adventures in Automated Smart Contract Testing: Proving More of Spark's PSM with Echidna 2.4

03 Nov, 2026

TL;DR

Echidna 2.4.0 ships the arithmetic abstraction from our previous post, so the Spark PSM3 proofs no longer need a custom build. On the stock release and a 32 GB Linux server, 56 of the 60 properties verify with the same harness and the same make verify. The other four come back unknown, one of them a regression the hevm team is investigating, and three more hours of fuzzing (about 180 million calls) found no violation of any of them.

In our previous post, we proved sixty properties of Spark’s PSM3 core math with Echidna’s verification mode: share price, conversions, and swap quotes, for every input up to uint128. There was a catch. The arithmetic abstraction behind those proofs was still an open hevm pull request, so reproducing them took a custom build of both hevm and Echidna. Echidna 2.4.0 removes that step. We re-ran the same harness, with the repo’s unchanged echidna.yaml, on the release binary and a Linux server with 32 GB of RAM, to see how many of the proofs still go through.

What changed in Echidna 2.4

The arithmetic abstraction is now part of the release. hevm#1075, the two-phase abstraction for symbolic multiplication, division, and modulo, has been merged, and Echidna 2.4 turns it on in both exploration and verification (#1639, pinned in #1645). The idea is the same as last time: seal each product and quotient, and give the solver a short list of facts true of every product instead of the exact value. The list of facts grew, and there is one change to the soundness contract we described last time: a counterexample found with the sealed values is now checked again with exact multiplication, and reported only if it still fails.

The solver also gets more memory. Until 2.4, Echidna inherited a fixed 1 GB limit per solver process from hevm, which hevm enforces only on Linux. Several of the harder swapExactOut proofs need more than that, which is why we ran the full set on a large-memory machine last time. Echidna 2.4 makes the limit configurable with symExecSolverMemory and defaults it to 16 GB (#1642), and those proofs now go through on the 32 GB server.

Results

Result: 56 of 60 properties verified, nothing falsified. Most still discharge in about a second. The swapExactOut proofs that needed the extra memory take between one and five minutes each, and a few USDC conversions now take about fifty seconds.

Four properties that verified last time come back unknown with 2.4.0. An unknown is not a counterexample: the solver ran out of time without finding a proof or a violation.

swapExactOut_susdsToUsds hits the 300-second per-query timeout twice.
previewSwapExactOut_usdsToSUsds and previewSwapExactOut_susdsToUsds, the two bounds that keep a round-up quote within one wei of the exact price, run for over two hours without an answer.
roundtrip_usds_susds is a regression. It checks that swapping USDS into sUSDS and back never returns more than you put in:

out  = x · 1e27 / rate        // USDS to sUSDS, rounded down
back = out · rate / 1e27      // sUSDS to USDS, rounded down
assert back ≤ x

The lemmas this proof needs are in hevm’s catalogue, but the abstraction in Echidna 2.4 does not apply them to this query, so the solver times out. The hevm team is investigating.

In the table below, each property is either ✅ verified or ⏳ unknown with Echidna 2.4.0. We did not retry the eleven properties that were out of reach last time.

Limits
① Still bounded to uint128. Every proof keeps the same operand bound as last time, about 3×10²⁰ tokens at 18 decimals.
② Same harness, same bytecode. The results come from the symbolic-conversion-proofs branch, unchanged since the previous post. We measured each time from the moment Echidna logged that it started a property to the moment it started the next one.

Full per-property results: 56 verified, 4 unknown

Result	Property	Contract	Time	Notes
✅	`convertToAssets_susds`	`PSMConvertToAssetsTests`	<1 s
✅	`convertToAssets_usdc`	`PSMConvertToAssetsTests`	<1 s
✅	`convertToAssets_usds`	`PSMConvertToAssetsTests`	1 s
✅	`convertToAssetValue_noValue`	`PSMConvertToAssetValueTests`	<1 s
✅	`convertToShares_noValue`	`PSMConvertToSharesTests`	<1 s
✅	`convertToShares_susds_noValue`	`PSMConvertToSharesWithSUsdsTests`	<1 s
✅	`convertToShares_usdc_noValue`	`PSMConvertToSharesWithUsdcTests`	48 s
✅	`convertToShares_usds_noValue`	`PSMConvertToSharesWithUsdsTests`	<1 s
✅	`getSUsdsValue_roundDown_rate_monotonic`	`ProveGetters`	<1 s
✅	`getSUsdsValue_roundUp_monotonic`	`ProveGetters`	1 s
✅	`getSUsdsValue_roundUp_rate_monotonic`	`ProveGetters`	2 s
✅	`getAssetValue`	`PSMHarnessTests`	<1 s
✅	`getSUsdsValue`	`PSMHarnessTests`	<1 s
✅	`getUsdcValue`	`PSMHarnessTests`	<1 s
✅	`getUsdsValue`	`PSMHarnessTests`	<1 s
✅	`previewDeposit_susds_firstDeposit`	`PSMPreviewDeposit_SuccessTests`	<1 s
✅	`previewDeposit_usdc_firstDeposit`	`PSMPreviewDeposit_SuccessTests`	48 s
✅	`previewDeposit_usds_firstDeposit`	`PSMPreviewDeposit_SuccessTests`	<1 s
✅	`assetValue_backing_monotonic`	`ProveRealPSM3`	2 s
✅	`assetValue_monotonic`	`ProveRealPSM3`	<1 s
✅	`convertToAssets_susds_monotonic`	`ProveRealPSM3`	2.2 min
✅	`convertToAssets_usdc_monotonic`	`ProveRealPSM3`	4 s
✅	`convertToAssets_usds_eq_value`	`ProveRealPSM3`	<1 s
✅	`pd_susds_firstdeposit_mono`	`ProveRealPSM3`	<1 s
✅	`pd_usdc_firstdeposit_mono`	`ProveRealPSM3`	<1 s
✅	`pd_usds_firstdeposit_mono`	`ProveRealPSM3`	<1 s
✅	`roundtrip_no_inflation`	`ProveRealPSM3`	<1 s
✅	`roundtrip_shares`	`ProveRealPSM3`	<1 s
✅	`shares_anti_monotonic_assets`	`ProveRealPSM3`	1 s
✅	`shares_monotonic`	`ProveRealPSM3`	<1 s
✅	`shares_no_inflation`	`ProveRealPSM3`	<1 s
✅	`totalAssets_exact`	`ProveRealPSM3`	<1 s
✅	`convertToShares_totalValue_eq_totalShares`	`ProveRealPSM3`	<1 s	`convertToShares(totalAssets()) == totalShares`
✅	`convertToAssetValue_totalShares_eq_totalAssets`	`ProveRealPSM3`	<1 s	dual of the above
✅	`totalAssets_rateIncrease_valueChange`	`ProveRealPSM3`	<1 s	value-change identity (telescoping lemma)
✅	`rounding_susdsValue_tight`	`ProveRounding`	1 s
✅	`previewSwapExactIn_susdsToUsdc`	`PSMPreviewSwapExactIn_SUsdsAssetInTests`	<1 s
✅	`previewSwapExactIn_susdsToUsds`	`PSMPreviewSwapExactIn_SUsdsAssetInTests`	<1 s
✅	`previewSwapExactIn_usdcToSUsds`	`PSMPreviewSwapExactIn_USDCAssetInTests`	<1 s
✅	`previewSwapExactIn_usdcToUsds`	`PSMPreviewSwapExactIn_USDCAssetInTests`	59 s
✅	`previewSwapExactIn_usdsToSUsds`	`PSMPreviewSwapExactIn_UsdsAssetInTests`	<1 s
✅	`previewSwapExactIn_usdsToUsdc`	`PSMPreviewSwapExactIn_UsdsAssetInTests`	1 s
✅	`previewSwapExactOut_usdsToUsdc`	`PSMPreviewSwapExactOut_UsdsAssetInTests`	47 s
⏳	`previewSwapExactOut_usdsToSUsds`	`PSMPreviewSwapExactOut_UsdsAssetInTests`	2 h 11 min	round-up within 1 wei; solver timeout
⏳	`previewSwapExactOut_susdsToUsds`	`PSMPreviewSwapExactOut_SUsdsAssetInTests`	2 h 26 min	round-up within 1 wei; solver timeout
⏳	`roundtrip_usds_susds`	`ProveSwapPreviews`	10.0 min	regression, under investigation
✅	`swapExactIn_susdsToUsdc_rate_increasing`	`ProveSwapPreviews`	<1 s
✅	`swapExactIn_susdsToUsds_rate_increasing`	`ProveSwapPreviews`	<1 s
✅	`swapExactIn_usdcToSUsds_rate_decreasing`	`ProveSwapPreviews`	70 s
✅	`swapExactIn_usdsToSUsds_rate_decreasing`	`ProveSwapPreviews`	7 s
✅	`swapExactOut_susdsToUsdc`	`ProveSwapPreviews`	2.1 min
✅	`swapExactOut_susdsToUsdc_rate_decreasing`	`ProveSwapPreviews`	2.5 min
⏳	`swapExactOut_susdsToUsds`	`ProveSwapPreviews`	10.0 min	solver timeout
✅	`swapExactOut_susdsToUsds_rate_decreasing`	`ProveSwapPreviews`	111 s
✅	`swapExactOut_usdcToSUsds`	`ProveSwapPreviews`	109 s
✅	`swapExactOut_usdcToSUsds_rate_increasing`	`ProveSwapPreviews`	3.6 min
✅	`swapExactOut_usdcToUsds`	`ProveSwapPreviews`	<1 s
✅	`swapExactOut_usdsToSUsds`	`ProveSwapPreviews`	4.0 min
✅	`swapExactOut_usdsToSUsds_rate_increasing`	`ProveSwapPreviews`	4.6 min
✅	`swapExactOut_usdsToUsdc`	`ProveSwapPreviews`	<1 s

Then fuzz what is left

An unknown says nothing either way, so we pointed Echidna 2.4.0’s fuzzer at the four prove_* functions themselves: same input bounds, same assertions, one transaction per call, and calls restricted to the target functions. Three campaigns of three hours each:

Property	Calls	Result
`swapExactOut_susdsToUsds`	52.3M (shared with the next row)	No violation
`roundtrip_usds_susds`	52.3M (shared with the previous row)	No violation
`previewSwapExactOut_usdsToSUsds`	62.4M	No violation
`previewSwapExactOut_susdsToUsds`	65.2M	No violation

Echidna’s coverage report confirms that the campaigns reached the assertions of the first two properties. The last two call Spark’s own testFuzz_* tests, which check the bound with forge-std’s assertLe. That compiles to a cheatcode that reverts with assertion failed, and Echidna’s assertion mode treats that revert as a failure, so a violated bound would have been reported.

About 180 million calls, zero violations. That is not a proof, so the four properties stay in the fuzzing campaign, next to the 600 million single-transaction executions from last time.

Try it yourself

Install Echidna 2.4.0, put bitwuzla on your PATH, and run make verify in our spark-psm branch. The Makefile and test/symbolic/echidna.yaml are the same as last time.

We also packaged the workflow for coding agents. fizz is an agent skill that builds and runs a fuzzing suite for a protocol, and it now has an optional step, off by default, that uses Echidna 2.4’s verification mode. It picks the stateless math a proof can cover (conversions, previews, quotes), writes a separate prove_* harness for it, runs the proofs, and reports only verified results as proven, together with the input bounds each proof assumes. Stateful properties stay in the fuzzing campaign. The skill’s symbolic verification guide can also be read on its own: when to attempt a proof, the harness patterns we used here, the uint128 operand bound, when a single-slot token model is sound, and how to read each result.

Prove the core; fuzz the rest, now with a stock Echidna release.

Oh, Just One More Thing

If you notice anything in this blog post that is incorrect, imprecise, or potentially misleading, please feel free to contact me for clarification. And a thank-you: this post was funded by the recent donation round on Giveth for Echidna; work like this is possible because of everyone who contributed. And a big thanks to the hevm team for their hard work on the arithmetic abstraction and for getting it merged; none of these proofs would run on a stock Echidna without it.

#Echidna #Formal-Verification #Symbolic-Execution #Fuzzing #Hevm