Smart Contract Security
Technical Case Study
When Cleanup Creates a Liveness Risk
How zero-fill matching, deferred cleanup, and atomic rollback combined to disrupt order-book matching, and how Aftermath addressed it.
Read article
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
How zero-fill matching, deferred cleanup, and atomic rollback combined to disrupt order-book matching, and how Aftermath addressed it.
Blockchain Infrastructure
Certora and powdr developed a verifier that checks whether autoprecompile optimizations preserve program behavior. Across Keccak and Reth workloads, it proved more than 98% of 6,627 circuit-equivalence checks automatically.
AI & Automation
Certora compared AutoProver’s independently generated Aave v4 Hub specification with a human-authored verification engagement. AutoProver discovered and proved substantial solvency and accounting properties, but the comparison also revealed why generated coverage must be paired with expert analysis of protocol intent and economic safety.
Smart Contract Security
Blockchain Infrastructure
Certora verified the security of Solana's core upgrade from SPL Token to the optimized P-Token program. We used the Certora Solana Prover to prove their equivalence, ensuring that P-Token is a safe drop-in replacement.
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.
Product & Company
We explain the vulnerabilities in our first DeFi hacking challenge and announce a relaunch of the contest with a twist: Capture the Funds - Endless CTF!
Operational Security
Operating a Solana validator under the Solana Foundation Delegation Program requires fast, reliable, and secure infrastructure decisions. Rather than adopting heavyweight monitoring frameworks, we chose a deliberately minimalist approach grounded in Unix principles. This article explains the tradeoffs behind that decision.
Product & Company
Certora presents its first community contests for securing Soroban smart contracts written in Rust. We partnered with Code4rena and Cantina to crowdsource security analysis of the Blend v2 and Aquarius protocols for the Stellar blockchain.
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
Kamino Lending partnered with Certora's formal verification to identify and resolve a subtle rounding issue in its Solana-based lending protocol, proactively securing it against potential future exploits.