Many compilation stages of smart contracts on the Ethereum blockchain have been transitioned to the intermediate language YUL. Tasks such as smart contract optimization and bytecode generation are—or will soon be—performed directly at the YUL level in the compilers for the higher-level languages such as Solidity. In this paper, we develop a formal semantics of YUL programs in Rocq, suitable for verification, which allows formal reasoning at the level of YUL code or generation tools processing YUL programs. Our semantics is expressive enough to be the basis for formal verification tools, and simple enough to make the development of such tools feasible. In order to prove its adequacy for verification, we develop in Rocq a checker (and associated soundness proofs), based on our semantics, able to verify the results of the liveness analysis stage of the official Solidity compiler solc, which opens the door towards formally verified Ethereum’s smart contracts compilation. Experiments on more than 1,500 smart contracts show that we are able to automatically verify solc’s liveness analysis results in negligible time.