Kirchner, DanielAlbert Albiol, Elvira MaríaGenaim, SamirMartín Martín, Enrique2026-02-272026-02-272023-07-17Albert, E., Genaim, S., Kirchner, D., Martin-Martin, E. (2023). Formally Verified EVM Block-Optimizations. In: Enea, C., Lal, A. (eds) Computer Aided Verification. CAV 2023. Lecture Notes in Computer Science, vol 13966. Springer, Cham. https://doi.org/10.1007/978-3-031-37709-9_9978303137708297830313770990302-97431611-334910.1007/978-3-031-37709-9_9https://hdl.handle.net/20.500.14352/133537The efficiency and the security of smart contracts are their two fundamental properties, but might come at odds: the use of optimizers to enhance efficiency may introduce bugs and compromise security. Our focus is on EVM (Ethereum Virtual Machine) block-optimizations, which enhance the efficiency of jump-free blocks of opcodes by eliminating, reordering and even changing the original opcodes. We reconcile efficiency and security by providing the verification technology to formally prove the correctness of EVM block-optimizations on smart contracts using the Coq proof assistant. This amounts to the challenging problem of proving semantic equivalence of two blocks of EVM instructions, which is realized by means of three novel Coq components: a symbolic execution engine which can execute an EVM block and produce a symbolic state; a number of simplification lemmas which transform a symbolic state into an equivalent one; and a checker of symbolic states to compare the symbolic states produced for the two EVM blocks under comparison.engAttribution 4.0 Internationalhttp://creativecommons.org/licenses/by/4.0/conference paperhttps://doi.org/10.1007/978-3-031-37709-9_9open accessCoqEthereum Virtual MachineSmart ContractsOptimizationTheorem ProvingLenguajes de programación1203.17 Informática