Ensuring Gas Optimisation Correctness by Behavioural Equivalence

Gas consumption has a financial impact on executing Ethereum smart contracts, making gas optimisation an essential development concern. Although several optimisation techniques exist, applying them can alter contract behaviour, compromising correctness or introducing vulnerabilities. This work introduces a formal verification framework to ensure that gas-optimised contracts remain behaviourally equivalent to their originals. Our approach relies on the Certora Prover to mechanise correctness checking: a transformation rule is selected from our catalogue, applied to a Solidity contract, and verified in Certora. If an optimisation violates equivalence, counterexamples guide a diagnosis and correction. To support practical adoption, we compiled a catalogue of 31 gas-saving transformation rules, each featuring a formal pattern and an example alongside a Certora specification for automated verification. Building this catalogue revealed that two previously published optimisations require updates for Solidity 0.8.0 or superior. To evaluate practical applicability, we conducted a case study on the widely-adopted AAVE V3 DeFi protocol, applying our refinement-based methodology to formally prove the behavioural equivalence of optimised versions against the original. Although not fully automated, the framework is mostly mechanisable. Our results demonstrate that combining formal verification with gas-optimisation strategies is both feasible and effective for real-world smart contracts.