Context: Superoptimization is a synthesis technique that, given a loop-free sequence of instructions, searches for an equivalent sequence that is optimal wrt. an objective function. Superoptimization of Ethereum smart contracts aims at minimizing the size of their bytecode and the gas consumption of executing the contract’s functions. The search for the optimal solution poses huge computational demands – as the search space to find the optimal sequence is exponential on the given size-bound – being the main challenge for superoptimization today to scale up to real, industrial software. Even if the underlying problem for finding the optimal solution is decidable, practical tools often prioritize efficiency over completeness. This means they might be implemented to find a sub-optimal solution or even time out. Objective: This work aims at leveraging superoptimization to a real setting: Ethereum blockchain. This paper proposes a neural-guided superoptimization (NGS) approach which incorporates deep neural networks using (supervised) learning into superoptimization to improve scalability by predicting: (1) if a sequence is already optimal and hence the search can be skipped; (2) the size-bound for the optimal solution in order to reduce the search space. Method: We have downloaded over 13,000 smart contracts deployed on the blockchain for training and testing the machine learning models, and a disjoint set with 100 of the smart contracts with more transactions to prove our scalability gains and impact for the Ethereum community. Results: Incorporating DNNs resulted in a 16x overall speedup (12x for gas) with only 12% optimization loss (14% for gas), or a 3-4x speedup with no optimization loss. For the 100 analyzed contracts, this approach reduced the average compilation time to 3 min per contract and achieved monetary savings of \$1.24M. Conclusions: The integration of machine learning models mitigates several limitations of traditional superoptimization by drastically reducing execution times while maintaining most of the original optimization gains.

@article{AguiarAGGHKR25,
title = {Neural-guided superoptimization in ethereum},
journal = {Information and Software Technology},
volume = {186},
pages = {107800},
year = {2025},
issn = {0950-5849},
doi = {https://doi.org/10.1016/j.infsof.2025.107800},
url = {https://www.sciencedirect.com/science/article/pii/S0950584925001399},
author = {Matheus Ara\'ujo Aguiar and Elvira Albert and Samir Genaim and Pablo Gordillo and Alejandro Hern\'andez-Cerezo and Daniel Kirchner and Albert Rubio},
pdf = {https://costa.fdi.ucm.es/papers/costa/AAGGHKR25.pdf},
abstract = {Context: Superoptimization is a synthesis technique that,
                  given a loop-free sequence of instructions, searches
                  for an equivalent sequence that is optimal wrt. an
                  objective function. Superoptimization of Ethereum
                  smart contracts aims at minimizing the size of their
                  bytecode and the gas consumption of executing the
                  contract’s functions. The search for the optimal
                  solution poses huge computational demands – as the
                  search space to find the optimal sequence is
                  exponential on the given size-bound – being the main
                  challenge for superoptimization today to scale up to
                  real, industrial software. Even if the underlying
                  problem for finding the optimal solution is
                  decidable, practical tools often prioritize
                  efficiency over completeness. This means they might
                  be implemented to find a sub-optimal solution or
                  even time out.

                  Objective: This work aims at
                  leveraging superoptimization to a real setting:
                  Ethereum blockchain. This paper proposes a
                  neural-guided superoptimization (NGS) approach which
                  incorporates deep neural networks using (supervised)
                  learning into superoptimization to improve
                  scalability by predicting: (1) if a sequence is
                  already optimal and hence the search can be skipped;
                  (2) the size-bound for the optimal solution in order
                  to reduce the search space.

                  Method: We have
                  downloaded over 13,000 smart contracts deployed on
                  the blockchain for training and testing the machine
                  learning models, and a disjoint set with 100 of the
                  smart contracts with more transactions to prove our
                  scalability gains and impact for the Ethereum
                  community.

                  Results: Incorporating DNNs resulted in
                  a 16x overall speedup (12x for gas) with only 12\%
                  optimization loss (14\% for gas), or a 3-4x speedup
                  with no optimization loss. For the 100 analyzed
                  contracts, this approach reduced the average
                  compilation time to 3 min per contract and achieved
                  monetary savings of \$1.24M.

                  Conclusions: The integration of machine learning models mitigates
                  several limitations of traditional superoptimization
                  by drastically reducing execution times while
                  maintaining most of the original optimization
                  gains.}
}

Smart contracts are programs deployed on a blockchain. They are executed for a monetary fee paid in gas, a clear optimization target for smart contract compilers. Because smart contracts are a young, fast-moving field without (manually) fine-tuned compilers, they highly benefit from automated and adaptable approaches, especially as smart contracts are effectively immutable, and as-such need a high-level of assurance. This makes them an ideal domain for applying formal methods. Super-optimization is a technique to find the best translation of a block of instructions by trying all possible sequences of instructions which produce the same result. We present a framework for super-optimizing smart contracts based on Max-SMT with two main ingredients: (1) a stack functional specification extracted from the basic blocks of a smart contract, which is simplified using rules capturing the semantics of arithmetic, bit-wise, and relational operations, and (2) the synthesis of optimized blocks, which finds, by means of an efficient SMT encoding, basic blocks with minimal gas cost whose stack functional specification is equal (modulo commutativity) to the extracted one. We implemented our framework in the tool SYRUP. Through large-scale experiments on real-world smart contracts we analyze performance improvements for different SMT encodings, as well as trade-offs between quality of optimizations and required optimization time.

@article{AlbertGHRS22,
 author    = {Elvira Albert and
               Pablo Gordillo and
               Alejandro Hern\'andez-Cerezo and
               Albert Rubio and
               Maria A. Schett},
  title     = {{Super-Optimization of Smart Contracts}},
  journal = {{ACM Transactions on Software Engineering and Methodology}},
  year      = {2022},
  volume = {31 Issue 4},
  number = {70},
  pages = {1--29}, 
  issn = {1049-331X},
  doi = {10.1145/3506800},
  url = {https://doi.org/10.1145/3506800},
abstract = { Smart contracts are programs deployed on a
                  blockchain. They are executed for a monetary fee
                  paid in gas, a clear optimization target for smart
                  contract compilers. Because smart contracts are a
                  young, fast-moving field without (manually)
                  fine-tuned compilers, they highly benefit from
                  automated and adaptable approaches, especially as
                  smart contracts are effectively immutable, and
                  as-such need a high-level of assurance. This makes
                  them an ideal domain for applying formal methods.
                  Super-optimization is a technique to find the best
                  translation of a block of instructions by trying all
                  possible sequences of instructions which produce the
                  same result.  We present a framework for
                  super-optimizing smart contracts based on Max-SMT
                  with two main ingredients: (1) a stack functional
                  specification extracted from the basic blocks of a
                  smart contract, which is simplified using rules
                  capturing the semantics of arithmetic, bit-wise, and
                  relational operations, and (2) the synthesis of
                  optimized blocks, which finds, by means of an
                  efficient SMT encoding, basic blocks with minimal
                  gas cost whose stack functional specification is
                  equal (modulo commutativity) to the extracted one.
                  We implemented our framework in the tool
                  SYRUP. Through large-scale experiments on real-world
                  smart contracts we analyze performance improvements
                  for different SMT encodings, as well as trade-offs
                  between quality of optimizations and required
                  optimization time. }
}

Given a loop-free sequence of instructions, superoptimization techniques use a constraint solver to search for an equivalent sequence that is optimal for a desired objective. The complexity of the search grows exponentially with the length of the solution being constructed, and the problem becomes intractable for large sequences of instructions. This paper presents a new approach to superoptimizing stack-bytecode via three novel components: (1) a greedy algorithm to refine the bound on the length of the optimal solution; (2) a new representation of the optimization problem as a set of weighted soft clauses in MaxSAT; (3) a series of domain-specific dominance and redundant constraints to reduce the search space for optimal solutions. We have developed a tool, named SuperStack, which can be used to find optimal code translations of modern stack-based bytecode, namely WebAssembly or Ethereum bytecode. Experimental evaluation on more than 500,000 sequences shows the proposed greedy, constraint-based and SAT combination is able to greatly increase optimization gains achieved by existing superoptimizers and reduce to at least a fourth the optimization time.

@inproceedings{AlbertGHIRS24,
  author    = {Elvira Albert and 
               Maria Garcia de la Banda and
	       Alejandro Hern{\'{a}}ndez{-}Cerezo and
	       Alexey Ignatiev and
	       Albert Rubio and
	       Peter J. Stuckey},
  title     = {{SuperStack}: {Superoptimization} of {Stack-Bytecode} via
                  {Greedy}, {Constraint-based}, and {SAT} {Techniques}},
  booktitle    = {{PLDI} '24: 45th {ACM} {SIGPLAN} International Conference on Programming
                  Language Design and Implementation, Copenhagen, Denmark, June 24-28,
                  2024},
  year         = {2024},
  publisher    = {{ACM}},
  abstract = {Given a loop-free sequence of instructions,
                  superoptimization techniques use a constraint solver
                  to search for an equivalent sequence that is optimal
                  for a desired objective. The complexity of the
                  search grows exponentially with the length of the
                  solution being constructed, and the problem becomes
                  intractable for large sequences of
                  instructions. This paper presents a new approach to
                  superoptimizing stack-bytecode via three novel
                  components: (1) a greedy algorithm to refine the
                  bound on the length of the optimal solution; (2) a
                  new representation of the optimization problem as a
                  set of weighted soft clauses in MaxSAT; (3) a series
                  of domain-specific dominance and redundant
                  constraints to reduce the search space for optimal
                  solutions. We have developed a tool, named
                  SuperStack, which can be used to find optimal code
                  translations of modern stack-based bytecode, namely
                  WebAssembly or Ethereum bytecode. Experimental
                  evaluation on more than 500,000 sequences shows the
                  proposed greedy, constraint-based and SAT
                  combination is able to greatly increase optimization
                  gains achieved by existing superoptimizers and
                  reduce to at least a fourth the optimization time.
                  }
}

Superoptimization is a compilation technique that searches for the optimal sequence of instructions semantically equivalent to a given (loop-free) initial sequence. With the advent of SMT solvers, it has been successfully applied to LLVM code (to reduce the number of instructions) and to Ethereum EVM bytecode (to reduce its gas consumption). Both applications, when proven practical, have left out memory operations and thus missed important optimization opportunities. A main challenge to superoptimization today is handling memory operations while remaining scalable. We present GASOLv2, a gas and bytes-size superoptimization tool for Ethereum smart contracts, that leverages a previous Max-SMT approach for only stack optimization to optimize also w.r.t. memory and storage. GASOLv2 can be used to optimize the size in bytes, aligned with the optimization criterion used by the Solidity compiler solc, and it can also be used to optimize gas consumption. Our experiments on 12,378 blocks from 30 randomly selected real contracts achieve gains of 16.42% in gas w.r.t. the previous version of the optimizer without memory handling, and gains of 3.28% in bytes-size over code already optimized by solc.

@inproceedings{AlbertGHR22,
  author    = {Elvira Albert and
               Pablo Gordillo and
               Alejandro Hern\'andez-Cerezo and
               Albert Rubio},
  title     = {{A} {M}ax-{SMT}  {S}uperoptimizer for {EVM}
  handling {M}emory and {S}torage},
  booktitle = {28th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2022. Proceedings},
  year      = {2022},
    publisher = {Springer},
  series	= lncs,
    doi={10.1007/978-3-030-99524-9_11},
  pages={201-219},
  volume    = {13243},
  isbn={978-3-030-99524-9},
    editor    = {Dana Fisman and
               Grigore Rosu},
  pdf = {https://costa.fdi.ucm.es/papers/costa/AlbertGHR22.pdf},
  abstract = { Superoptimization is a compilation technique that
                  searches for the optimal sequence of instructions
                  semantically equivalent to a given (loop-free)
                  initial sequence. With the advent of SMT solvers, it
                  has been successfully applied to LLVM code (to
                  reduce the number of instructions) and to Ethereum
                  EVM bytecode (to reduce its gas consumption). Both
                  applications, when proven practical, have left out
                  memory operations and thus missed important
                  optimization opportunities. A main challenge to
                  superoptimization today is handling memory
                  operations while remaining scalable. We present
                  GASOLv2, a gas and bytes-size superoptimization tool
                  for Ethereum smart contracts, that leverages a
                  previous Max-SMT approach for only stack
                  optimization to optimize also w.r.t. memory and
                  storage.  GASOLv2 can be used to optimize the size
                  in bytes, aligned with the optimization criterion
                  used by the Solidity compiler solc, and it can also
                  be used to optimize gas consumption. Our experiments
                  on 12,378 blocks from 30 randomly selected real
                  contracts achieve gains of 16.42\% in gas w.r.t. the
                  previous version of the optimizer without memory
                  handling, and gains of 3.28\% in bytes-size over
                  code already optimized by solc.}
}

@inproceedings{AlbertGHRR22,
  author    = {Elvira Albert and
               Pablo Gordillo and
               Alejandro Hern{\'{a}}ndez{-}Cerezo and
               Clara Rodr{\'{\i}}guez{-}N{\'{u}}{\~{n}}ez and
               Albert Rubio},
  title     = {Using Automated Reasoning Techniques for Enhancing the Efficiency
               and Security of (Ethereum) Smart Contracts},
  booktitle = {Automated Reasoning - 11th International Joint Conference, {IJCAR}
               2022, Haifa, Israel, August 8-10, 2022, Proceedings},
  year      = {2022},
    publisher = {Springer},
  series	= lncs,
    doi={10.1007/978-3-031-10769-6_1},
  pages={3--7},
  volume    = {13385},
  isbn={978-3-031-10769-6},
  editor    = {Jasmin Blanchette and
               Laura Kov{\'{a}}cs and
               Dirk Pattinson},
  pdf = {https://link.springer.com/content/pdf/10.1007/978-3-031-10769-6_1.pdf}
}

@TechReport{AlbertCGRR20bTR,
  author    = {Elvira Albert and
               Jes\'us Correas and
               Pablo Gordillo and
               Alejandro Hern\'andez-Cerezo and 
               Guillermo Rom\'an-D\'iez and
               Albert Rubio},
  title     = {{A}nalyzing {S}mart {C}ontracts: {F}rom {EVM} to a {S}ound {C}ontrol-{F}low {G}raph},
  year      = {2020},
  pdf = {https://costa.fdi.ucm.es/papers/costa/AlbertCGRR20bTR.pdf}
}