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
Certora researchers identified a high-severity soundness vulnerability in gnark’s fake GLV scalar multiplication. An unconstrained prover-supplied point could enable forged ECDSA signatures in circuits using P-256, P-384 or the STARK curve. Fixed in gnark v0.16.4.
Smart Contract Security
How zero-fill matching, deferred cleanup, and atomic rollback combined to disrupt order-book matching, and how Aftermath addressed it.
Smart Contract Security
Smart Contract Security
This article presents two complementary methodologies for threat modeling: Certora's "4 A's" framework and the STRIDE framework. Soroban smart contracts teams who invest in this essential process early will lay the groundwork for security, resulting in simpler architecture, fewer bugs, and faster audits.
Smart Contract Security
We provide a roadmap for Stellar smart contract builders to prepare for a security audit through the Soroban Security Audit Bank. By designing for security, writing clean & tool-friendly Rust code, rigorously testing, and running security tools beforehand, projects can be well-prepared. Be audit-ready so your project gets a faster, deeper, and more valuable security review.
Smart Contract Security
How to design Solidity smart contracts that are easier to formally verify.
Smart Contract Security
Lending protocols may appear simple, but their safety depends on how every operation interacts across the system. In this deep dive, we show how Certora approached the formal verification of Suilend by proving end-to-end properties like solvency, account health consistency, and liquidation profitability.
Smart Contract Security
On November 3, 2025, Balancer suffered an incident in which attackers manipulated internal vault logic to drain liquidity across multiple blockchains. The breach underscores the importance of prioritizing security even for mature protocols with multiple audits, and it raises urgent questions about composability, operational controls, and the evolving threat-landscape in Web3. Here is Certora’s analysis of the incident, as well as a detailed timeline of events.
Smart Contract Security
Our experience formally verifying Rust smart contracts for Soroban and Solana has helped us identify what makes a Rust smart contract easy or difficult to verify. This blog post shares five best practices distilled from our observations to help Web3 developers write Rust smart contracts that are not only secure and readable, but also verifiable.
Smart Contract Security
Our engineers identified and corrected a subtle but significant issue in infiniFi's redemption logic through rigorous formal verification, ensuring fairness and trustworthiness. The team ensured that users are treated consistently and predictably under all conditions.
Smart Contract Security
This blog post demonstrates how formal verification with Certora Prover complements traditional fuzz testing by identifying critical edge cases in Uniswap v4. By translating fuzz tests into robust Certora Verification Language (CVL) rules, our approach uncovered subtle vulnerabilities, particularly involving malicious hooks
Smart Contract Security
In recent years, tiny rounding mistakes, often as small as 1 wei, have cost DeFi protocols over $100 million. Because the EVM only handles integers, every division forces a round‑up or round‑down decision, creating subtle gaps that attackers can exploit at scale. Learn how formal verification tools can systematically prove your contracts’ invariants and reveal hidden rounding bugs before they go live.