What is it about?
Smart contracts are programs that run on the Ethereum blockchain and handle things like payments, loans and token exchanges automatically. Every time one of these programs runs, its users pay a fee called "gas", so developers try to rewrite their code to make it cheaper. The problem is that these rewrites can accidentally change what the program does, which can introduce bugs or security holes in systems that manage real money. We built a method that uses mathematical proof, carried out by an automated tool called the Certora Prover, to confirm that a cheaper version of a contract behaves exactly like the original: same results, same errors, same records and same handling of funds. We also assembled a public catalogue of 31 cost-saving rewrites, each with an example and a ready-to-use proof specification.
Featured Image
Photo by Shubham Dhage on Unsplash
Why is it important?
Gas optimisations are usually shared as examples with no guarantee that they are safe. While building our catalogue, we found that two optimisations previously published in the research literature no longer preserve behaviour in current versions of Solidity, the main language for Ethereum contracts, and we proposed corrected versions that we proved safe. We also applied our method to Aave V3, one of the largest lending protocols in decentralised finance. We proved that the optimisations from a professional gas audit kept the code's behaviour intact, and then went further: our own optimised version saved more than the audit on 8 of the 9 components we studied, and every version was proven equivalent to the original. This shows that saving money and guaranteeing correctness can go together, even in real-world, high-value code.
Perspectives
This work started from a simple question: when we make a smart contract cheaper, how can we be sure we haven't broken it? It was striking to discover that even optimisations published in the literature could quietly fail after the language evolved, which convinced me that verification should be part of optimisation, not an afterthought. Applying the method to a real protocol like Aave V3 was the most challenging and rewarding part, because it showed the approach works beyond toy examples. The paper presents the method as mechanisable, and we are already working on automating much of it, so that developers can optimise and verify their contracts with far less effort.
Manoel Villarim
Universidade Federal de Pernambuco
Read the Original
This page is a summary of: Ensuring Gas Optimisation Correctness by Behavioural Equivalence, ACM Transactions on Software Engineering and Methodology, November 2026, ACM (Association for Computing Machinery),
DOI: 10.1145/3859488.
You can read the full text:
Contributors
The following have contributed to this page
