Formally Verifying WebAssembly
Smart contracts are designed to carry out financial transactions involving millions of dollars. Bugs in these programs are known to have severe consequences. Naturally, formal verification plays a critical role in this domain. In this blog, we present Certora’s recent efforts towards formally verifying Wasm bytecode.
Certora recently raised the bar for DeFi security by formally verifying a key property of the Euler V2 Vault implementation. In this post we talk about how formal verification can offer strong assurance about DeFi protocols, find rare bugs unknown to developers, and even involve specifications that are simpler to understand than exploits.
The Certora team recently finished reviewing token extensions on Solana utilizing our in-depth formal verification tools.
This article is for students with a math or computer science background interested in learning more about decentralized finance (DeFi), developing analytical skills, and earning lucrative income by helping secure software.
Formal verification contests offer a measurable and effective approach to increasing code security by combining the depth of formal verification with the breadth of the community. Learn how you can leverage formal verification to get better results from audit competitions.
Prover version 7.3.0 is out! This update aims to enhance your user experience and address some minor bugs reported by our users.
Certora today announced its engagement with Solana Foundation to review and formally verify the code underlying token extensions on Solana, the new program-level token features that natively extend token functionality.
In this post (the sequel to “How to optimize your gas consumption without getting REKT”), we focus our attention on Solidity/Yul libraries that realize the mathematical and economic computations that lie at the heart of the DeFi world, and explain why equivalence checking is a potent tool in the hands of developers and auditors who wish to work on such code.
Developing a DeFi product is an engineering problem of deceptive depth — it is easy to write a smart contract in Solidity that (mostly) does what you want, but it is hard to do it well.
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.
In the previous post, we showed how to prove the correctness of Mint operation which is part of the basic functionality of both the SPL Token. In this post, we show how the Solana Certora Prover (SCP) can be used to find bugs in the confidentiality extension of the SPL Token.
The Vyper programming language provides a clean memory and control abstraction. In comparison to Solidity, it is considered highly attractive for DeFi programming.
In our previous post, we described our new verification tool for Solana contracts. In this post, we show the verifier in action on SPL Token 2022, a widely-used Solana application. In the next post, we will show how to find bugs in the confidential extension of SPL Token 2022.
In a series of posts, we shall discuss our efforts to formally verify Solana smart contracts. We have developed a new in-house verification tool that takes Solana contracts written in Rust together with a specification and automatically proves that the specification holds.
The first time that an automatic tool has found a bug in a public, open-source, Solidity library.
On May 10th, the Silo team informed us about a critical vulnerability that had been reported by an external researcher and fixed a few days before. We conducted a thorough investigation and manual review of the issue, the fix, and the rest of the code base.
In this blog, we discuss our efforts to apply mutation testing in the context of automated verification.
Since its earliest days, the Certora Prover has been a powerful tool for finding bugs and ensuring code security in the smart contracts which make up Web3 applications. Writing specifications using the Certora Verification Language (CVL), our customers and Certora’s own personnel have been able to bring the tremendous power of formal verification to bear on projects large and small throughout the Ethereum space.
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 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.
