
AI & Automation
Introducing AutoProver: Bringing Agentic Formal Verification to Every Developer
AutoProver utilises AI agents and formal methods to automatically infer intent from your code, generate specifications, and prove the absence of bugs.

Certora Blog
Technical research and practical perspectives for financial institutions, regulators and builders.

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.

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.

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.

Blockchain Infrastructure
Certora has received a research grant from the Ethereum Foundation as part of the zkEVM Formal Verification Project to help secure critical performance optimizations in zkEVM implementations. The work focuses on formally verifying autoprecompiles—automatically generated, reusable ZK circuit components developed by Powdr Labs that significantly improve zkEVM performance.

Product & Company
Last year our security footprint expanded across new chains, languages, and infrastructure layers. Our security research team quadrupled in size. And our work drove home the importance of long-term security partnerships. The numbers here tell that story: not just what we secured in 2025, but the momentum that’s carrying Certora and DeFi as a whole into 2026.

Product & Company
Through this initiative, Certora directly contributes to Solana’s decentralization, resilience, and operational security by operating a high-assurance validator built to rigorous security and reliability standards.

AI & Automation
The new Certora AI Composer is an open-source AI coding platform that composes artificial intelligence with formal verification to make smart contract development faster and safer.

Product & Company

Product & Company
Certora has open-sourced the Certora Prover, the most advanced formal verification tool for smart contracts on Ethereum, Solana, and Stellar. Used to secure over $75B in DeFi assets, the Prover guarantees correctness by detecting all potential bugs. Start verifying your code today!

Operational Security
Safeguard is a Geth extension that monitors Ethereum protocol invariants in real time to enhance the security of DeFi systems and monitor exploits.

Smart Contract Security
Explore Quorum, the open-source tool protecting Aave, that secures DAO governance by automating verification, detecting risks, and ensuring proposals execute as intended.