Formal verification of Smart Contracts has the potential to significantly improve their security and reliability. At ConsenSys, we are developing techniques for formally verifying Smart Contracts at the EVM bytecode level. Our approach is based around a formalisation of the EVM called the DafnyEVM (https://github.com/ConsenSys/evm-dafny). This is written in the Dafny programming language (https://dafny.org) which allows it to be used for formally verification. In this talk, I will illustrate how the DafnyEVM can be used to verify Smart Contracts at the bytecode level, and give an overview of how the system works.