A Formalization of the Yul Language and Some Verified Yul Code Transformations

July 25, 2025 · The Ethereal · 🏛 International Workshop on the ACL2 Theorem Prover and Its Applications

🔮 THE ETHEREAL: The Ethereal
Pure theory — exists on a plane beyond code

"No code URL or promise found in abstract"

Evidence collected by the PWNC Scanner

Authors Alessandro Coglio, Eric McCarthy arXiv ID 2507.19012 Category cs.LO: Logic in CS Cross-listed cs.PL Citations 0 Venue International Workshop on the ACL2 Theorem Prover and Its Applications Last Checked 5 months ago
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.
Community shame:
Not yet rated
📄 View on arXiv 🌐 View on ar5iv 📑 PDF 🎉 Report Code Found
Community Contributions

Found the code? Know the venue? Think something is wrong? Let us know!

📜 Similar Papers

In the same crypt — Logic in CS