Smart contracts are distributed applications on blockchains that implement advanced financial instruments, such as decentralized exchanges or autonomous organizations (DAOs). Their financial nature makes smart contracts an attractive attack target, as demonstrated by numerous exploits on popular contracts resulting in economic damage of millions of dollars. Unfortunately, vulnerability assessment that is sound and insightful for smart contracts is a formidable challenge because contracts execute low-level bytecode in a largely unknown and potentially hostile execution environment. This talk offers an introduction to smart contract verification. To this end, I present HoRStify, the first automated analyzer for dependency properties of Ethereum smart contracts based on sound static analysis. Afterward, I introduce the blockchain-specific security risk of frontrunning and discuss ideas on how to verify its absence.