Superfluid CFA Realtime-Balance Conservation

Superfluid's Constant Flow Agreement (CFA) is the part of the protocol that manages one-to-one token streams. We proved this accounting rule for covered flow creations, updates, ordinary deletions by the sender, and one receiver callback that deletes its own flow. The proof covers CFA accounting, not pools, claims, liquidations, or every possible hook.

Why It Matters

Superfluid balances change continuously, but a flow should only move value between accounts. Creating, changing, or deleting a stream must not make value appear or disappear.

We proved that the sender and receiver changes cancel out, while the other accounts being checked remain unchanged. This stays true as time passes and for the covered one-level callback.

How This Was Modeled and Proven

We modeled the relevant create, update, and delete logic from ConstantFlowAgreementV1.sol at pinned commit 414109689d9041a8b6900b67b947f3f203c1da5d. A CFA projection is the value an account has already settled, plus the value streamed since its last update. Shared settled balances follow SuperfluidToken.sol.

Lean proves that each covered operation preserves the combined CFA projection of the sender and receiver. It also proves that every other account in the supplied list is unchanged. Together, those results preserve the list's total CFA projection, both when the operation happens and at any later modeled time.

For callbacks, we proved that one nested CFA action preserves the same accounting rule when each step is valid. A second callback level is rejected, and a failed nested action rolls the whole operation back. The pinned SelfDeletingFlowTestApp is one concrete verified example. This does not mean that every arbitrary hook contract is verified.

The case contains 22 public properties: the original 13 local and callback properties plus 9 strengthening tasks shown above. Their reference proofs compile without case-specific axioms, sorry, admit, or native_decide.

git clone https://github.com/lfglabs-dev/ethereum-verification-benchmark
cd ethereum-verification-benchmark
git checkout 88c3f45b51156dc9a4905e5f5ea0832851000eeb
lake build Benchmark.Cases.Superfluid.RealtimeBalanceConservation.Proofs

Assumptions

The first row is the external fact the theorem trusts. The second row records values checked by the modeled operation. CFA-only accounting and liquidation deletion are scope exclusions listed above. We do not assume that the excluded paths work correctly.

• Host routing is outside this proofThe proof starts after the Host has selected the operation context

  PinnedSourceState and pinnedSourcePathRelation

  Superfluid's Host chooses the token, sender, receiver, flow record, and callback app passed into CFA. The proof checks the CFA accounting after those values have been chosen. It does not prove that the Host selected or encoded them correctly; that would require a separate proof of the Host's routing and context-validation logic.

• valid runtime valuesTimestamps, flow rates, deposits, and packed values satisfy the source checks

  Executable guards and sourceAccountRelationAt

  These are conditions for a successful call, not assumptions about an excluded part of Superfluid. Invalid calls revert instead of becoming successful flow operations. For the nested callback, we separately proved that failure rolls the entire operation back.