Smart contract developers face a bevy of potential pitfalls that traditional web2 methodologies and tools are unequipped to handle. For example, reentrancy and flash loan vulnerabilities have enabled many attacks on various exchanges, and even simple functional correctness bugs can lead to costly attacks. This talk will discuss how developers can avoid these vulnerabilities in their projects, both with manual reasoning and by using tools developed by Veridise.