Adventures in Automated Smart Contract Testing: A Spark Is Born

It is Monday morning, and the contract in front of you has cleared three audits, ships a green invariant suite, and has held real money without incident. The easy bugs are long gone, so what do you run now to raise confidence beyond “a few billion random inputs didn’t break it”? Two techniques answer that, with opposite blind spots. Fuzzing runs the real, unmodified contract. It is assumption-free, but it samples; absence of failure is not proof. Formal verification proves a property for all inputs, but only under a model, and a wrong model proves something about a contract subtly unlike the deployed one. Together, each covers the other: the proof settles the core math for every input; the fuzzer explores what the proof left out and checks that its assumptions didn’t define the bug away.

The contract: Spark’s PSM

PSM3 is the Peg Stability Module from Spark, in the Sky (formerly MakerDAO) ecosystem. It holds three related stable assets (USDC, USDS, and yield-bearing sUSDS), lets anyone swap between them at deterministic prices, and lets liquidity providers deposit for shares whose price tracks the pool’s value as sUSDS accrues yield. Audits read the code and fuzzers sample it; neither proves the conversion math, and we know of no published formal verification of it.

Proving the core math

Strip PSM to its arithmetic and one shape appears everywhere: an amount times one quantity, divided by another, a * b / c. The share price is that shape; so are the swap quotes and deposit previews:

// src/PSM3.sol (simplified)
function convertToShares(uint256 assetValue) public view returns (uint256) {
  uint256 totalAssets_ = totalAssets();
  if (totalAssets_ != 0) return assetValue * totalShares / totalAssets_;
  return assetValue;
}

To a prover all three variables are unknown 256-bit values, and that width is the problem. An SMT solver decides bitvector arithmetic by bitblasting, expanding each operation into a Boolean circuit. Multiplying by a constant stays cheap, but multiplying two unknowns expands to a 256×256 multiplier (tens of thousands of gates), and dividing by an unknown is worse. Do both, as a * b / c does, and the solver runs forever, returns unknown, or exhausts memory. (Bounding the values doesn’t help: a require(x < 2**32) leaves the terms 256 bits wide, and the same query still times out.)

hevm’s abstract arithmetic refuses to expand exactly those operations. Instead of computing what a * b is, it treats the result as a sealed box and gives the solver a short list of facts true of every product and quotient: a product never shrinks when an input grows; a * b = b * a; a quotient never grows when the divisor does; anything times zero is zero.

That is the whole trick: trade the exact value you can’t compute for a few relationships you can. The difference is dramatic. On a typical property (depositing more never mints fewer shares), native solving comes back unknown after a two-minute timeout; the abstraction proves it in a quarter of a second. This ships as one hevm change, #1075, a two-phase SMT abstraction for symbolic multiplication, division, and modulo, which echidna’s verification mode turns on. Once that PR merges, the integration is on its way to echidna master; today it takes a custom build of both.

The trade has a precise soundness contract. A proof is real: every fact holds for ordinary arithmetic, so the proof covers a more general contract, of which the deployed one is a special case. A counterexample is not: it may hinge on a sealed value real arithmetic could never produce. So a clean run is verified, while a counterexample is downgraded to passed, never reported as a bug.

Relationships prove orderings, not magnitudes. Exact results come from cancellation lemmas tuned to the PSM’s precision scaling: x * 1e18 / 1e6 is pinned to x * 1e12, a two-step /1e9 /1e18 folds into one /1e27, and one lemma relates two sealed products differing by a constant, enough to prove that a rate move changes the pool’s value by exactly the sUSDS revaluation.

Most of the math we verify completely, against the repo’s own tests. Each property inherits the contract’s unmodified testFuzz_*; the only addition is one uniform assumption, the abstraction’s operand budget:

function prove_convertToAssets_susds(uint256 rate, uint256 amount) public {
   require(rate <= type(uint128).max && amount <= type(uint128).max);
   testFuzz_convertToAssets_susds(rate, amount);   // the repo's own fuzz test, unmodified
}

Spark’s own fuzz tests become theorems: exact values, proven for every uint128 input, against the deployed bytecode.

Where the exact value is out of reach, a weaker property still rules out the attack. A few quotes are a ceilDiv over a rate-scaled product, or divide by the symbolic pool ratio; there we prove monotonicity, the direction of the result, which is what an attacker probes:

• more in never yields less out: no underpaying by splitting or reordering a swap;
• a higher rate never inverts pricing: a rate update can’t flip a quote;
• value → shares → value never grows: the first-depositor inflation attack, ruled out.

A separate bound catches what monotonicity would miss (monotone but mis-rounded): round-up and round-down never differ by more than one wei.

Despite our best efforts, eleven properties stay open, for two reasons. Three previewSwapExactOut legs resist the abstraction: their round-up (ceilDiv) quotes come back unknown within the time budget, and we have not pinned down exactly why. Eight fail on setup: they deposit through a real MockERC20 before asserting, and the mock’s keccak-mapping balance reads are intractable inside the abstracted arithmetic. Our own relational properties sidestep that wall with a modelling workaround: the symbolic harness deploys minimal tokens whose balanceOf is a single storage slot rather than a mapping, so each balance read is one clean symbolic value. That is sound here because every property reads each token at exactly one holder and never moves tokens; the deposit-driven tests as written do move them, so they go to the fuzzer.

Result: sixty properties verified, nothing falsified. Most discharge in about a second, and the whole set runs in about half an hour. In the table below, each property is either ✅ verified or ⏳ out of reach.

Limits

① Bounded to uint128. The no-overflow facts hold while products fit in 256 bits, so every proof assumes each input (and a few derived sums like totalAssets()) is at most type(uint128).max. That is about 3×10²⁰ tokens at 18 decimals, far past any real supply, but it is a real bound, so we name it.

② Quotes are proven; the swap acting on them is not. The property that matters most, an executed swap never pays out more than its quote, ranges over transfers and balances the symbolic engine can’t reach. The fuzzing campaign carries it, via the value-conservation and rounds-in-the-protocol’s-favour invariants.

Then fuzz the rest

A proof of the stateless math is narrow by design; the fuzzer takes everything around it.

The same properties come first, on the real arithmetic: echidna runs the repo’s testFuzz_* directly, with real mul and div on full uint256, covering the ⏳ rows and the whole swap/deposit/withdraw execution surface, plus nine single-transaction properties of our own (swap value-conservation, both conversion round-trips, preview monotonicity) written for what the unit suite doesn’t assert. It also independently checks the proofs: if a lemma were unsound, the prover would still say verified, but the fuzzer on the same code would not stay quiet. Across two campaigns (an eight-hour sweep of every stateless target, then a further 24 hours on the surfaces the proofs leave open) that is over 600 million single-transaction executions with zero falsifications, exercising the conversion math in both rounding directions.

Beyond the stateless properties, PSM3’s real risk is emergent: long sequences of deposits, swaps, withdrawals, and rate updates by many actors. We drive the protocol’s own handler suite and check eight invariants after every step: shares sum to the supply, the pool stays solvent, value is neither created nor destroyed, swaps round in the protocol’s favour, and at teardown every position can still be withdrawn in full. That fourth invariant is exactly the end-to-end safety the proofs left open (caveat ②). Two 24-hour campaigns, roughly 90 million transactions in all, and every invariant held.

The audits picked one invariant for us: re-reading the reports surfaced exactly one property the suite didn’t already enforce: a Cantina finding where a withdraw could round the share price down, diluting LPs. It was fixed years ago, but a fixed bug is exactly what a regression invariant should pin forever. Now it is one: the share price never falls by more than a rounding wei after any action, with a companion invariant that the sUSDS rate only accrues upward.

Building the harness caught a bug of its own: point setPocket at an address that already belongs to a liquidity provider and the two become one account: USDC withdrawals turn into no-op self-transfers while the ghost accounting still books the outflow, breaking invariant_E (pocket balance == tracked inflows − outflows). A test-setup flaw, not a contract vulnerability, but a genuine result, reported upstream as sparkdotfi/spark-psm#53.

Each leg of the argument is one command in the repo’s Makefile: make verify, make fuzz T=<Contract>, make fuzz-invariant.

The same result reads differently depending on your seat. If you build protocols, your existing fuzz suite is closer to a proof harness than you think; a uniform require plus echidna’s verification mode on hevm’s abstract arithmetic turned Spark’s own tests into theorems. If you hunt bugs, verification is a filter: a verified property is code you no longer have to re-review by hand, and running the proofs yourself on a target leaves you a shorter, sharper list of things worth reading, starting with the out-of-reach rows and the executed-swap gap above.

Prove the core; fuzz the rest. The conversion math is now a set of theorems about the deployed bytecode, everything else is fuzzed on top, and the one property an audit once found broken is an invariant that can’t quietly come back. Neither technique reaches that on its own.

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.