CoW Protocol Settlement Trade Amounts Respect the Limit Order
For every successful settle() trade, what the owner is charged and the receiver is paid meets the signed limit price, and the order is never filled beyond its signed amount.
CoW Protocol is a batch-auction exchange. Users sign orders off-chain: sell up to sellAmount of one token for at least buyAmount of another. Solvers compete to settle batches of these orders and choose the clearing prices and fill sizes.
The solver is not trusted with user funds. On chain, GPv2Settlement.settle computes and checks the amounts of every trade before the vault relayer pulls the users' sell tokens and the contract pays out. This case proves that computation keeps the user's limit. As long as tokens move exactly the amounts they are asked to, the owner's and receiver's balances move by exactly those amounts too. Take an order to sell 1 ETH for at least 3,000 USDC. If a partial fill of 0.25 ETH succeeds, the order's receiver is paid at least 750 USDC, and the contract never counts more than 1 ETH as filled in total. Solver prices that would break this make the trade revert.
Why It Matters
The contract turns clearing prices into amounts with integer division. Rounding the wrong way can shave a unit off every fill. Repeated over many small partial fills, a solver could then take the whole order while the user receives less than their limit. The 2021 G0 Group audit reported exactly this rounding direction as a finding, and CoW fixed it by rounding the buy amount up.
The unit of value at risk is every token a user has approved to the CoW vault relayer. The affected party is the order owner. The property matters most for partially fillable orders and for orders that appear more than once, possibly within the same batch.
How This Was Modeled and Proven
We built a source-aligned Lean model of the arithmetic and fill-counter path of computeTradeExecution, with SafeMath's exact overflow and division checks. Every simplification is listed at the top of Contract.lean. We also modeled every other function that writes an order's fill counter: invalidateOrder, freeFilledAmountStorage, and the bookkeeping at the end of swap. Lean then checks the rules for every possible input.
The first theorem covers one trade in all four branches: sell or buy order, partially fillable or fill-or-kill. It combines the on-chain price check with the rounding direction: sell orders round the buy amount up and buy orders round the sell amount down. A second theorem carries this to token balances. If each of the trade's two transfers moves exactly the amount settle hands to it, the owner's balance drops by exactly the computed sell amount in the pull and the receiver's rises by exactly the computed buy amount in the payout, so both respect the limit. Net balance changes over a whole settlement, which also runs solver interactions and other trades, are not claimed. A third theorem follows one order through every tracked lifecycle of trades, repeated uids in a batch, invalidations, storage refunds, swap fills, and unrelated activity. It shows the totals of settle trades since tracking began keep the limit price, never exceed the signed amount, and keep fees within the signed fee pro rata. For orders with a nonzero sellAmount (sell) or buyAmount (buy), the total fee never exceeds the signed fee.
The model is pinned to CoW contracts revision c07a93e3596194c5e3cf331c755a3f9f0e4a17d8. The proof contains no case-specific axioms, sorry, or admit.
Scope
Included: trades settled through settle, for sell and buy orders, partially fillable and fill-or-kill, with any solver prices and fill sizes. The fill-counter writes of invalidation, expired-order storage refunds, and swap are modeled, so the settle guarantees hold in tracked lifecycles that mix them.
Not covered: the price of swap(), the Balancer direct path. It is enforced by Balancer swap limits that we did not model, and swap fills are not counted in the proved totals. Balancer governance vote BIP-927 revoked the CoW vault relayer's Balancer Vault permissions, including swaps, on Ethereum. We also observed them revoked on Gnosis Chain, Base, and Arbitrum, so swap() reverts on those chains today.
Token behavior: by source inspection, settle passes each computed amount unchanged to the token's transfer function, the Balancer Vault, or a native ETH send, and a failed transfer reverts the whole settlement. The token and Vault code is not modeled. The balance theorem assumes each transfer moves exactly the amount it is given (see Hypotheses). Tokens that charge a fee on transfer or rebase break this and can deliver a different amount.
Fees: the fee bound holds for any signed feeAmount. The zero-fee result applies to orders signed with feeAmount = 0, which CoW's order API now requires. That is an off-chain rule, not a contract property.
Source correspondence: the deployed contract at 0x9008D19f58AAbD9eD0D60971565AA8510560ab41 is a Sourcify exact match. A normalized comparison with the pinned revision found only semantics-neutral differences: pragma range, modifier declaration syntax, uint256(-1) versus type(uint256).max, loop style, and a private helper name spelling fix. This is a source-level comparison. Solidity-to-Lean correspondence and bytecode equivalence were reviewed by hand, not mechanized.
Proof artifacts
- Contract.lean models computeTradeExecution and the other fill-counter writers, with every simplification listed at the top.
- Specs.lean defines the limit price, fill, and fee rules and the order lifecycle.
- Proofs.lean contains the reference proofs.
- Case directory contains the compile target and benchmark wiring.
- The reviewed change is in the benchmark pull request.
| Function | Theorem | Status |
|---|---|---|
| computeTradeExecution | computeTradeExecution_respects_limit_order | Proven |
| settle trade transfers | settle_trade_respects_limit_order_in_balances | Proven |
| settle order lifecycle | order_lifecycle_safety | Proven |
| settle order lifecycle | order_lifecycle_fee_cap | Proven |
| settle order lifecycle | order_lifecycle_zero_fee | Proven |
Verify it yourself
git clone https://github.com/lfglabs-dev/ethereum-verification-benchmark cd ethereum-verification-benchmark git checkout 3f600985ae55b23b27ebcb59eb0708f5c68bc9a3 lake build Benchmark.Cases.Cow.GPv2Settlement.Compile
Hypotheses
These rows separate what the proof trusts from what the contract checks. Exact premises are in Specs.lean and Proofs.lean.
assumption: tokens move exactly the requested amountDebitedExactly and CreditedExactly in Specs.lean
The owner loses exactly the amount pulled, and the receiver gains exactly the amount paid out. Token and Vault code is outside the model. Standard tokens, the Balancer Vault, and ETH behave this way; fee-on-transfer and rebasing tokens do not. Only the balance theorem relies on it.
assumption: one signed order per order idEIP-712 order hash in the uid
Each order id (uid) belongs to exactly one signed order. The id embeds the hash of the signed order, its owner, and its expiry. We trust signature recovery and hash collision resistance.
assumption: nothing else resets an order's fill countersource inspection of GPv2Settlement.sol
The contract counts how much of each order is filled, so it cannot be filled twice. Between two trades, anything can happen on Ethereum: other orders, solver calls, new blocks. The model does not include all of it, so the proof assumes none of it resets this counter. Reading the code confirms only four functions write it, and all four are modeled.
assumption: time never goes backwardsEthereum consensus
The block timestamp never decreases. This is what stops a refunded, expired order from trading again: a refund needs the order to be expired, and a trade needs it not to be.
runtime precondition: the trade succeedsGPv2Settlement.sol L349-L421
The theorems describe trades that pass every expiry, price, fill, and SafeMath check. A trade that would overflow 2^256, divide by a zero price, exceed the fill, or break the price check reverts and changes nothing.
scope exclusion: zero-amount orders in the fee capCoW contracts README, Known issues
The total fee cap only covers orders with a nonzero sellAmount (sell orders) or buyAmount (buy orders). CoW documents that an order with a zero amount can be executed repeatedly, charging its fee each time. The per-trade price rule still holds for such orders. The README advises never to sign them.