Join us for an in-depth workshop on the Clear framework, a cutting-edge tool designed for the formal verification of smart contracts by extracting Yul code into Lean. This workshop will explore Clear’s remarkable expressivity, enabling any pen-and-paper proof of correctness to be mechanized in Lean. Participants will learn about Clear's compositionality and abstraction, allowing scalable verification of complex smart-contracts, and its automation capabilities to streamline proof generation.