Smart Contract Security
Insights
Auditing Smart Contracts on Canton Network
Read article
Certora Blog
Technical research and practical perspectives for financial institutions, regulators and builders.
Selected by the Certora team
Formal Verification
A vulnerability in the Soroban SDK caused equivalent cryptographic values to compare as different, potentially allowing double withdrawals in affected contracts. This case study explores CVE-2026-32322, shows how Certora's Sunbeam Prover reproduces the issue with a simple formal verification rule, and explains what developers should check when using affected SDK versions.
Smart Contract Security
A practical look at Solana program security, from authorization and Token-2022 integrations to oracle checks and accounting invariants, illustrated by findings from Certora audits.
Smart Contract Security
A guide to auditing Daml smart contracts on Canton, from authorization and privacy to contract references, accounting invariants, settlement and topology.
Formal Verification
We examine four ways formally verified systems can fail: incorrect specifications, flawed assumptions, mismatches between verified models and deployed code, and bugs in verification tools themselves. Through real-world examples, we explain how to identify these risks and what to check before relying on a formal verification proof.
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.