Smart Contract Security
Technical Analysis
The Payy Exploit: A $1.92M Forged ZK Proof Attack
Read article
Certora Blog
Technical research and practical perspectives for financial institutions, regulators and builders.
Selected by the Certora team
Smart Contract Security
Smart Contract Security
Formal Verification
Smart Contract Security
On September 24, 2026, Payy lost $1.92 million in USDC after forged zero-knowledge proofs passed its verifier. This analysis reconstructs the Barretenberg soundness bug, the fix released 73 days before the exploit, and a Lean model demonstrating the missing constraint.
Smart Contract Security
Auditing Stellar smart contracts requires understanding both application logic and Soroban’s execution model. Drawing on Certora’s audit findings, this article examines authorization, storage lifetime, cross-contract calls, asset accounting, and cross-chain messaging. It shows how inconsistencies between components can strand transfers or prevent message execution, and explains which invariants teams should define before an audit.
Smart Contract Security
The Bitget hack resulted in approximately $387.5 million in stolen assets after attackers exploited a zero-day in a third-party security product and compromised Bitget’s wallet infrastructure. Rather than stealing private keys, the attackers forged withdrawal requests that Bitget’s own signing system accepted as legitimate, allowing valid signatures over unauthorized transfers.
Formal Verification
Formal verification, testing, and smart contract audits address different questions about protocol security. This guide compares the risks each method can uncover, the limits of a clean result, and how to combine them throughout development, launch, and upgrades. Real protocol examples show why coverage depends on review scope, tested inputs, stated properties, and model assumptions.
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.