Smart Contract Security
Technical Analysis
The Tectonic Exploit: A $120.4M Collateral Inflation Attack
Read article
Certora Blog
Technical research and practical perspectives for financial institutions, regulators and builders.
Selected by the Certora team
Formal Verification
Formal verification checks whether code satisfies precisely stated properties within a defined model and set of assumptions. This guide explains what that means for smart contracts, how it complements testing and human audits, and what a verification engagement involves. A flaw found in Solana’s SPL Stake Pool shows how a property can expose a consequential edge case before deployment.
Smart Contract Security
The Tectonic exploit combined exchange-rate manipulation with TONIC price manipulation to inflate collateral and borrow approximately $120.4M across nine markets. This analysis breaks down the exploit, the property verified by Certora Prover, and how the accounting issue can be prevented.
Product & Company
Certora is extending AutoProver to Rust and building native formal verification support for Solana programs. AutoProver uses AI agents to analyze code, generate candidate properties and investigate failures, while Certora’s prover determines whether those properties hold. The open-source work builds on Certora’s existing verification experience across the Solana ecosystem, with an initial release targeted around Solana Breakpoint in November 2026.
AI & Automation
AutoProver utilises AI agents and formal methods to automatically infer intent from your code, generate specifications, and prove the absence of bugs.
Institutional Finance
Certora has received a grant from the Canton Development Fund to develop a new open-source static analysis tool for Daml smart contracts on the Canton Network. The tooling will help developers and financial institutions analyze cross-package contract interactions, improve visibility into authority delegation and privacy implications, and strengthen security assurance for multi-party blockchain applications before deployment.
Product & Company
We have released Certora Prover Version 8.13.0 that includes new features for EVM, Solana, and Soroban.
Operational Security
The recent theft from the KelpDAO bridge highlights the critical risk of using 1-of-1 security configurations. Moving forward, bridge security requires enforcing multi-DVN quorums and monitoring all infrastructure components to prevent catastrophic single points of failure.
Smart Contract Security
Cross-chain swaps depend on more than bug fixes. This post explores how Certora's security review of 1inch's commit–reveal mechanism helped harden timing windows, deposit infrastructure, and fee configuration — so users can swap across chains with confidence.
Product & Company
We have released Certora Prover Version 8.11.3 that includes new features.
Smart Contract Security
Together, Aave and Certora demonstrate what is possible when security is treated not as a checkbox but as a core design principle.
Operational Security
The Compound Finance website was manipulated to redirect to a phishing site hosting a lookalike service. Our industry is learning daily that while the on-chain threat persists, the off-chain threat is formidable and growing.
Product & Company
This partnership reflects a shared commitment to building a secure, resilient, and developer-first ecosystem, as well as ensuring that Sui-based protocols can scale with confidence as adoption grows.
