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 this 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 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.

All proofs are verified by Lean 4's kernel and are provided in Proofs.lean. If any step were wrong, the code would not compile.

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

Proof status

All 18 theorems are proven. Proofs.lean is sorry-free.

Assumptions

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 abstractionproofAccepted: Bool

  Cryptographic guarantee (OpenZeppelin MerkleProof)

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

• Single-round specializationmodel covers one 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 elidedstate accounting only

  OpenZeppelin SafeERC20

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

• msg.sender authenticitycaller identity

  EVM guarantee

  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.