Adventures in Automated Smart Contract Testing: A Spark Is Born | Gustavo Grieco: blockchain security researcher<br>Adventures in Automated Smart Contract Testing: A Spark Is Born<br>03 Jul, 2026<br>TL;DR<br>We proved the core accounting math of Spark&rsquo;s PSM3 (share price, conversions, swap quotes) against the real bytecode: sixty properties, verified for every input up to uint128, with all the code in our spark-psm branch. The proofs run in Echidna&rsquo;s verification mode on top of hevm&rsquo;s arithmetic abstraction, still experimental and in review as argotorg/hevm#1075. 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&rsquo;s own fuzz tests and eight stateful invariants. All clean, except one small bug in the invariant harness itself. Whatever your seat: if you build protocols, your fuzz suite is closer to a proof harness than you think; if you hunt bugs, every verified property is code you no longer have to re-review. Prove the core, fuzz the rest.

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 &ldquo;a few billion random inputs didn&rsquo;t break it&rdquo;? 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&rsquo;t define the bug away.<br>The contract: Spark&rsquo;s PSM<br>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&rsquo;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<br>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:<br>// src/PSM3.sol (simplified)<br>function convertToShares(uint256 assetValue) public view returns (uint256) {<br>uint256 totalAssets_ = totalAssets();<br>if (totalAssets_ != 0) return assetValue * totalShares / totalAssets_;<br>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&rsquo;t help: a require(x leaves the terms 256 bits wide, and the same query still times out.)<br>hevm&rsquo;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.<br>That is the whole trick: trade the exact value you can&rsquo;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&rsquo;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.<br>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.<br>Relationships prove orderings, not magnitudes. Exact results come from cancellation lemmas tuned to the PSM&rsquo;s precision scaling : x * 1e18 / 1e6 is pinned to x * 1e12, a...