The bug that compiled, and the fix.

The bytes, not the source

One key, two layouts.

Both implementations mark their liquidity functions with the same reentrancy key, @nonreentrant('lock'), which asks the compiler for one lock shared by all of them. Vyper 0.2.15, 0.2.16 and 0.3.0 instead reserved a separate lock slot for every decorated function. The vulnerable implementation was deployed on 26 July 2021, less than three days after Vyper 0.2.15 was published.

The theorems locate both guards of the vulnerable implementation in its deployed bytes. Its remove_liquidity reads the total supply, sends ether to the receiver, and only afterwards writes the reduced supply back — so a callback that enters add_liquidity, finding that function’s own lock free, mints against a pool that is only half updated.

A violation, from deployment

The attack, executed.

On every covered fork, Jaune runs eight messages in sequence from a world holding only a funded creator without code, each settling without error. The first executes the implementation’s preserved creation input; the next six create a forwarder, initialize the pool, create a token and an attacker contract, approve the pool and add liquidity, leaving a sound LP ledger: a supply of 2,000, all held by the attacker. The eighth is the attack.

attacker ──► pool.remove_liquidity      slot 2: 0 → 1; reads totalSupply = 2,000
               └─ ether to attacker ──► attacker ──► pool.add_liquidity
                                          slot 0 free: enters the body, mints 106,
                                          balanceOf[attacker] = 2,106
             remove_liquidity resumes: burns 200, writes back totalSupply = 2,000 − 200
 result:     totalSupply = 1,800  <  balanceOf[attacker] = 1,906

The outer call writes back a supply it read before the callback, which erases the 106 tokens minted during the callback from the supply but not from the attacker’s balance (vminus_reachable_capstone). A second form states the same violation for every world that agrees with the reached one on the 14 storage slots and 6 accounts the attack reads (vminus_reach_violation).

The same corruption also happens inside an admitted transaction, from a separate synthetic state: on every covered fork, processTransaction accepts a fixed signed type-2 transaction carrying 16,043,200 gas, every admission check — signature recovery included — discharged by kernel evaluation and only room in the block assumed. The two results concern different worlds and do not compose, and neither replays the historical transactions, which ran under Shanghai, a fork Jaune does not implement. By LlamaRisk’s estimates, attackers extracted about $37 million from the three pools that forward to this implementation.

Safety, in every execution

The fix, proved.

For the fixed implementation, Blanc proves that the lock excludes. In any execution, whatever its outcome, while a frame of the pool is inside one of its five mutating guarded functions and has not released the lock, no frame below it enters any of the seven guarded functions of that pool — whatever code the frames in between run.

theorem vplus_exclusion {sevm : Sevm} {pre : Devm} {out : Execution}
    (R : Exec 0 sevm pre out) (hfork : CoveredFork sevm.benvStat.fork) {P : Adr}
    (hP : pre.getCode P = forwarderCode curvePlainImpl847e ∨ pre.getCode P = code)
    (hI : pre.getCode curvePlainImpl847e = code)
    (hroot : sevm.currentTarget = P → sevm.code = pre.getCode P)
    (hash : lockL.HashAvoidIn P R)
    {F h c : Exec.Deriv} (hF : F ∈ Exec.rawFrameRoots R)
    (active : ActiveRel P F h) (spawn : Spawns h c)
    {G : Exec.Deriv} (hG : G ∈ Exec.rawFrameRoots c.exc) :
    ¬ lockL.Enters P G

No premise mentions callbacks, reentry, or the value of the lock as a callee sees it: exclusion is derived, not assumed. The one hash premise, hash, is that no Keccak-256 digest the pool computes in that execution equals 0, the lock’s slot. R is an execution of any outcome — a reverted frame has still run — which is why the proof needs the certificate cursor of the method. The theorem holds for the implementation called directly and through the stETH-ng forwarder (hP), for messages, for transactions without EIP-7702 authorizations, and for every execution recorded in a configured history, given for each that the pool’s and the implementation’s code is installed, that its first frame runs the code stored there, and that its hashes avoid the lock’s slot.

On a covered fork, a frame that runs this code from its first instruction, with hashes that avoid the lock’s slot, also never executes DELEGATECALL, CALLCODE, CREATE, CREATE2 or SELFDESTRUCT; its only external calls are CALL and STATICCALL (lock_no_forbidden).

Statements that can fail

Not vacuous: the lock, seen refusing.

An exclusion theorem whose antecedent never holds would say nothing. Three executed witnesses, each on every covered fork, show this one does. The strongest mirrors the attack. Nine messages from the same creator-only world deploy, initialize and fund the pool; in the ninth, remove_liquidity holds the shared lock while it sends 100 wei to a receiver whose code attempts add_liquidity through the forwarder. That frame reads the held lock and reverts without reaching a guarded function; the outer call commits with the ledger still sound — supply and the creator’s balance both 1,800 — and the exclusion theorem is instantiated on this very execution with all of its premises proved (vplus_reachable_capstone).

Two older witnesses, from synthetic states, refuse a read-only reentry into get_virtual_price() and a mutating reentry through the stETH-ng forwarder.

A second pass over the certificate

How a lock is checked.

The fixed pool’s bytes are first read through a certificate like every other artifact. A second Boolean pass then runs over that certificate, with the lock’s state at join points supplied by a 444-line untrusted annotator. The kernel decides that every guarded function body is reached only after the lock was found free, that every mutating body starts with the lock held, and that inside one only release points write the lock’s slot. A soundness theorem, proved along the cursor, connects the pass to every frame that runs the code from program counter 0 on a covered fork, provided the hashes the frame computes avoid the lock’s slot.

Stated, so it is not inferred

Not claimed.

• A controlled experiment on the fix: the two implementations’ sources differ in other ways too, and the vulnerable result is a concrete violation, not the formal negation of the fixed one’s theorem.
• That admitted transactions reach the executions from deployment: those are sequences of messages, with implementations placed at their addresses as supplied creation targets and synthetic token, attacker, receiver and clone-deployer code. That transactions can produce equivalent messages is argued, not proved.
• Anything about unguarded functions, reentry after the lock is released, pricing, or the pool’s economics; liveness; transactions carrying EIP-7702 authorizations.
• A replay of the historical attack.

The claim map’s sections on the fixed and vulnerable implementations list every theorem with its premises, file and line. To our knowledge, neither implementation has had a machine-checked treatment before.