Blockchain protocols, including Bitcoin and Ethereum, allow for programmable transactions that determine for whom, when, and how funds can be redeemed. This lets users create “smart contracts” where conditions and obligations for transactions are enforced by the protocol itself. Unfortunately, hundreds of millions of dollars worth of Ethereum funds have already been lost due to programming errors in smart contracts. Ultimately, smart contracts will need to securely manage the irreversible transfer of millions of dollars worth of funds using custom, one-shot contracts, that are executed in the adversarial environment of the public internet. To achieve this, we are developing Simplicity, a new programming language designed for blockchains. Using the Coq proof assistant, we have developed both functional and operational formal semantics for our combinator-based language. We intend to use the VST to prove our C interpreter meets our formal semantics. Our goal is to use Deep Specifications to ensure smart contracts meet their design specifications and are executed correctly by the actual machine code that implements their protocols. Details about Simplicity can be found at https://arxiv.org/abs/1711.03028 or https://blockstream.com/simplicity.pdf.