Product & Company
Announcement
Certora Expands AutoProver to Rust and Adds Native Solana Support
Read article
Certora Blog
Technical research and practical perspectives for financial institutions, regulators and builders.
Selected by the Certora team
Smart Contract Security
AAVE started in 2017, which in the world of DeFi, a domain that has been popular since only 2017, is considered OG. Aave, or in its former name ETHLend, started as a P2P lending protocol, but later transformed into a liquidity pool-based protocol in early 2020. Back then, Certora, a small company with major talent and advanced-yet-unripe technology, aspired to enhance the security of an innovative protocol that prioritizes safeguarding against breaches.
Formal Verification
Formal verification uses mathematical models and computer algorithms to prove or disprove the correctness of the system’s design with respect to formal specifications expressed as properties.
Formal Verification
Formal verification improves software security by finding bugs and mathematically proving their absence via mathematical methods. Smart contracts are perfect applications for formal verification because bugs are costly, the code is typically small or modular, and it evolves over time.
