This blog details the discovery of a critical pool-draining vulnerability in SushiSwap’s Trident protocol. By establishing a key invariant and using automated formal verification, researchers uncovered a flaw in the burn-single operation that could have allowed an attacker to drain liquidity.

This blog post revisits the infamous Popsicle Finance bug, which resulted in a $20MM loss by exploiting a flaw in the token transfer mechanism. Using the Certora Prover for formal verification, we explain how the error—in which the transfer function failed to update profit-tracking variables—allowed attackers to boost a collaborator’s profit share illegitimately.