Dromos MetaDEX Allocation Conservation

Invariant

In the MetaDEX root-ledger model, each voting position's chain allocations always sum to its committed voting power.

Dromos Labs' MetaDEX builds on Aerodrome and Velodrome: users lock tokens for voting power that directs liquidity incentives. Its root Voter records how each position's voting power is partitioned across chains. The Dromos Labs team selected this conservation rule to check that the partition neither undercounts nor overcounts the total.

Why It Matters

Suppose a position has 100 units committed: 60 on one chain and 40 in the CHAIN0 holding bucket. Moving 20 out of CHAIN0 should leave 80 on that chain and 20 in the bucket, still totaling 100. Crediting the chain without debiting the bucket would record 120. Debiting without crediting would record 80.

The conserved ledger amounts are raw allocated AERO principal, not time-decaying voting weight or emitted rewards. This ledger records allocations; it does not pay out tokens. A mismatch would make the position's partition disagree with its total commitment. The proof rules out that mismatch in the modeled ledger; it does not prove incentive payouts, token solvency or voting-power valuation.

How This Was Modeled and Proven

We recreated the relevant Voter and AllocationLogicLibrary ledger operations in Verity, defined the rule precisely, and used Lean to check it across all permitted modeled inputs. The proof follows the actual amount writes, commitment updates and chain-set operations, rather than assuming a balanced result.

Every ledger write changes exactly one chain's amount, so we first prove a small building block: what a single change does to the total. It covers adding a chain to the list, removing one, and the swap-and-pop trick (the last chain takes the removed chain's slot), including updating that chain's recorded position. We then chain these blocks together across any number of loop iterations and returns from other chains. The result: starting from an empty ledger, every successful modeled transaction leaves the sum equal to the committed amount.

Scope

Covered

All 8 functions that write the voting ledger (listed in the table below). They are the only writers, checked by reading the pinned source.
Any number of chains, loop iterations and returns from other chains.
CHAIN0 (the holding bucket, not a real chain) and TOKEN0 (the special key burn uses). The sum covers every chain with a nonzero amount, including chain key 0.

Not covered

Points, slope schedules and emissions updates. The model leaves them untouched.
Gauge and adapter code, cross-chain transport, fees, events and token transfers.
Rewards, solvency, voting-power value and whole-protocol safety.
Replay protection. A repeated partial return can credit the remaining amount again; the sum still balances, but we do not claim it is prevented.
A machine-checked Solidity-to-Lean translation, and compiler or bytecode correctness. The match was reviewed by hand, and the model can accept some executions the source would reject (signed point arithmetic, casts).

Pinned versions: Dromos source 0058bd9b1d49b0fb0a6d130dd51886b2c64e3d99, benchmark 77c8a71f90f3e4aadb1440bcbbe01470c8974f1e. Neither is a deployment attestation.

Proof artifacts

Contract.lean: executable ledger and full simplification ledger.
Specs.lean: allocationConserved, all-chain interpretation, initialization and reachability.
SetProofs.lean and AssignmentProofs.lean: concrete set and one-cell replacement proofs.
Proofs.lean: operation preservation and transaction_conservation.
No case-local domain axiom or unfinished proof is used. Dependency printing reports only the standard Lean foundations propext, Classical.choice and Quot.sound.
Regression.lean: finite execution tests, distinct from the universal theorem. Generated agent tasks are intentional placeholders, not reference proofs.

Each theorem is proven and machine-checked in Lean on the model, our Lean version of the Solidity ledger code. Its match with the real contract was reviewed by hand.

Function	Theorem	Status
allocateChains	allocate_chains_preserves	Proven
allocate	allocate_preserves	Proven
burn (TOKEN0)	burn_preserves	Proven
rebalanceChain0	rebalance_preserves	Proven
processDeallocation	process_deallocation_preserves	Proven
emergencyDeallocate	emergency_preserves	Proven
parkOnChain0	park_preserves	Proven
clearToken	clear_token_preserves	Proven
Authenticated return sequences	dispatch_returns_preserves	Proven
Nonwriter ledger projection with returns	nonwriter_preserves	Proven
Every reachable modeled transaction	transaction_conservation	Proven

Verify it yourself

Check the pinned reference proof, not the generated task:

git clone https://github.com/lfglabs-dev/ethereum-verification-benchmark
cd ethereum-verification-benchmark
git checkout 77c8a71f90f3e4aadb1440bcbbe01470c8974f1e
LEAN_NUM_THREADS=1 timeout 170 lake build Benchmark.Cases.Dromos.AllocationConservation.Proofs

This targeted proof build passed under bounded execution with the repository's pinned Lean 4.31.0 and Verity revision. Full-repository baseline and post-authoring builds remain incomplete: bounded runs timed out or hit the aggregate-memory safety stop. The full repository is not reported green. In a 4 GiB worker, run heavy commands sequentially with an aggregate-RSS guard below 2700 MiB; do not raise the worker limit.

Hypotheses

Lean checks this without any case-specific axiom. The only premise is the starting state. Exact predicates are in Specs.lean.

premise: the ledger starts empty
initializedLedger and Reachable
The proof begins at a freshly deployed contract, with no chains, no amounts and nothing committed, and follows every successful transaction from there. For a new deployment this costs nothing, because Solidity storage starts at zero. It would not cover a contract migrated over existing state.

Learn More

More case studies

KPK Shares Settlement Accounting

A successful kpkShares settlement batch processes each eligible request at most once and accounts exactly for its fees, shares and asset transfers.

for

Railnet Queue Nominal Conservation

No matter how many partial redemptions happen, or in what order, the queue never records paying out more than it recorded receiving.

for

CoW Protocol Settlement Trade Amounts Respect the Limit Order

The amounts GPv2Settlement computes for settle-path trades respect the signed limit price after rounding and never overfill the order.

for