A Formalization of the Yul Language and Some Verified Yul Code Transformations
Logic in Computer Science
2025-07-28 v1 Programming Languages
Abstract
Yul is an intermediate language used in the compilation of the Solidity programming language for Ethereum smart contracts. The compiler applies customizable sequences of transformations to Yul code. To help ensure the correctness of these transformations and their sequencing, we used the ACL2 theorem prover to develop a formalization of the syntax and semantics of Yul, proofs relating static and dynamic semantics, a formalization of some Yul code transformations, and correctness proofs for these transformations.
Cite
@article{arxiv.2507.19012,
title = {A Formalization of the Yul Language and Some Verified Yul Code Transformations},
author = {Alessandro Coglio and Eric McCarthy},
journal= {arXiv preprint arXiv:2507.19012},
year = {2025}
}
Comments
In Proceedings ACL2 2025, arXiv:2507.18567