StreamRecoveryClaim Accounting Invariants

The StreamRecoveryClaim contract is a Merkle-proof-based distribution system for recovering USDC and WETH to ~40 users affected by the Stream Trading incident on Trevee Earn's vaults on Sonic chain. An admin snapshots affected users' vault balances, computes each user's pro-rata share, builds a Merkle tree with leaves (address, shareWad), and stores only the root onchain.

Users sign an EIP-712 liability waiver, then call claimUsdc or claimWeth. The contract verifies the Merkle proof against the stored root, computes amount = shareWad × roundTotal / 1e18, checks accounting bounds, and pays out. claimBoth calls both sequentially.

Why It Matters

This contract distributes recovery funds to victims of an exploit. A bug in the claim logic could let someone extract more than their entitlement, claim twice, or drain the round pool, taking funds that belong to other victims. The stakes are not abstract: every dollar overclaimed is a dollar another affected user does not receive.

How This Was Modeled and Proven

The claim functions were modeled in Verity from the Solidity StreamRecoveryClaim.sol implementation. Merkle verification is abstracted as a boolean witness and token transfers are elided; the proofs focus on accounting correctness.

The Lean model maps ten storage slots: round totals, claimed counters, allocated counters, round-active flag, per-user waiver and claim flags, split across USDC and WETH. Each function mutates this state differently:

• claimUsdc: verifies the Merkle proof, computes the payout, increments roundUsdcClaimed, decrements totalUsdcAllocated, marks the user as claimed
• claimWeth: symmetric to claimUsdc on the WETH slots
• claimBoth: calls claimUsdc then claimWeth sequentially. The cross-token independence proof shows this composition is safe: USDC accounting does not interfere with WETH accounting

How do you prove the books stay balanced? You show that every successful claim increases roundClaimed and decreases totalAllocated by exactly the same amount, so their sum is conserved. Combined with the solvency bound (roundClaimed ≤ roundTotal), this guarantees no value is created or destroyed and the round pot is never overdrawn.

git clone https://github.com/lfglabs-dev/verity-benchmark
cd verity-benchmark
lake build Benchmark.Cases.PaladinVotes.StreamRecoveryClaimUsdc.Compile

Hypotheses

The proofs use zero axioms. The only trust assumption is the Merkle proof abstraction. All other conditions are consumed in exactly the form the contract enforces them.

• Merkle proof check is trusted

  Cryptographic guarantee (OpenZeppelin MerkleProof)

  Merkle verification is modeled as a boolean witness, proofAccepted: Bool. This is the one real trust assumption: we assume the Merkle tree correctly binds (msg.sender, shareWad) to the stored root. That is a cryptographic guarantee from OpenZeppelin's MerkleProof library, not a contract-level concern.

• model covers a single round

  Scope decision

  The model covers one round. Multi-round batching (claimMultipleUsdc) is out of scope. The per-round accounting properties hold identically for each round.

• token transfers are not modeled

  OpenZeppelin SafeERC20

  The model verifies state accounting only, not ERC20 transfer execution. SafeERC20 correctness is trusted from OpenZeppelin.

• msg.sender is the real caller

  EVM guarantee

  The model assumes the caller identity in msg.sender is authentic. This is an EVM-level guarantee, not a contract-level concern.

View specs in LeanView proofs in Lean

Learn More

Sonic Earn Recovery System, the upstream contract repository.

What is a formal proof? A short explanation for non-specialists.