Engineers' Hub
Deep dives, implementation guides, research, and real-world verification insights for engineers working on complex software.
Better softwareA more open world
Smart Contract Security
This article explores the formal proof of solvency in Uniswap v4, ensuring that Automated Market Makers (AMMs) always have enough funds to cover withdrawals. By leveraging mathematical invariants, SMT solvers, and precise token accounting, we demonstrate how Uniswap v4 maintains security and solvency.
Smart Contract Security
Lido Finance, a leader in liquid staking, recently introduced a dual governance system to protect user funds and boost DAO security. However, any innovation carries risks and bugs in Lido’s governance would ripple across DeFi. This post details the design review process for Lido's governance system, outlining the challenges, bugs discovered, and solutions implemented to ensure the security and robustness of the protocol.
Smart Contract Security
Learn the best practices for writing secure Uniswap v4 hooks to prevent vulnerabilities and enhance DeFi security. Follow expert guidelines to safeguard your smart contracts.
Smart Contract Security
Discover critical security findings from Uniswap v4’s audits by Certora, OpenZeppelin, Trail of Bits, and Spearbit. Learn how vulnerabilities like double counting on CELO and tick price invariant violations were uncovered and mitigated to strengthen DeFi security.
Smart Contract Security
Explore Uniswap v4's innovative features and the associated security challenges. Learn how threat modeling identifies attack vectors and safeguards DeFi protocols.
Smart Contract Security
Discover how formal verification caught a sneaky vulnerability in integration of Ethereum's upcoming Electra upgrade that slipped past traditional audits, and what it means for one of crypto's hottest protocols.
Smart Contract Security
Certora recently raised the bar for DeFi security by formally verifying a key property of the Euler V2 Vault implementation. In this post we talk about how formal verification can offer strong assurance about DeFi protocols, find rare bugs unknown to developers, and even involve specifications that are simpler to understand than exploits.
Smart Contract Security
The first time that an automatic tool has found a bug in a public, open-source, Solidity library.
Smart Contract Security
On May 10th, the Silo team informed us about a critical vulnerability that had been reported by an external researcher and fixed a few days before. We conducted a thorough investigation and manual review of the issue, the fix, and the rest of the code base.
Smart Contract Security
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.
Smart Contract Security
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.