Engineers' Hub
Deep dives, implementation guides, research, and real-world verification insights for engineers working on complex software.
Better softwareA more open world
Formal Verification
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.
Blockchain Infrastructure
During Aave V3’s deployment on ZKsync, a severe LLVM compiler bug was discovered—one that could lead to fund loss. Learn how Certora, Aave Labs, BGD Labs, and Matter Labs traced the issue to its root cause and uncovered a hidden risk in compiler optimizations.
Blockchain Infrastructure
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.
Formal Verification
The Vyper programming language provides a clean memory and control abstraction. In comparison to Solidity, it is considered highly attractive for DeFi programming.
Formal Verification
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.
Formal Verification
Smart Contract Security
The first time that an automatic tool has found a bug in a public, open-source, Solidity library.
Smart Contract Security
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.
Blockchain Infrastructure
Certora identified and disclosed a significant optimization bug affecting Solidity compiler versions ≤0.8.14, where crucial memory operations in inline assembly could be erroneously removed, potentially impacting smart contract correctness.
Blockchain Infrastructure
Certora uncovered a Solidity compiler bug affecting inter-contract calldata validation in versions ≤0.8.13. The bug allowed malicious inputs to corrupt external calls, posing serious security risks.
Formal Verification
Smart Contract Security
This blog post revisits the infamous Popsicle Finance bug, which resulted in a $20MM loss by exploiting a flaw in the token transfer mechanism. Using the Certora Prover for formal verification, we explain how the error—in which the transfer function failed to update profit-tracking variables—allowed attackers to boost a collaborator’s profit share illegitimately.