Adventures in Automated Smart Contract Testing: A Spark Is Born

TL;DR. We proved the core accounting math of Spark’s PSM3 (share price, conversions, swap quotes) against the real bytecode: sixty properties, verified for every input up to uint128. The proofs run in Echidna’s verification mode on top of hevm’s arithmetic abstraction, which is still experimental code, in review as argotorg/hevm#1075. All the verification code is in our spark-psm branch if you want to check it. What resisted exact proof got monotonicity and rounding bounds that still rule out the attacks; everything else went to a fuzzing campaign: some 80 hours and roughly 700 million executions against the repo’s own fuzz tests and eight stateful invariants. All clean, except one small bug in the invariant harness itself. Prove the core, fuzz the rest.

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.

A concrete run: to show that depositing more never mints fewer shares, an ordinary solver would compute the share quotient for two deposits and compare; the multiplication buries it. The abstract solver computes nothing: one fact orders the two sealed products, a second carries that order through the division. Two facts, no arithmetic, every pair of inputs at once. That is the whole trick: trade the exact value you can’t compute for a few relationships you can. On exactly this property, native solving is 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.

And where even that is out of reach, we say so. 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. Naming the gaps is part of the method.

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

Scope: two limits, stated up front.

① 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, 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.

Then the histories a single-transaction proof never sees. 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.

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.