Digital Asset builds distributed-ledger and smart-contract technology for enterprise applications. Two key promises of this technology are significantly lower operational costs and increased auditability. Key techniques to realize these promises are the representation of contracts as code and immutable, authenticated data-structures. However, these techniques also do require significantly higher correctness guarantees from both contract specifications and ledger implementations. At Digital Asset, we provide these correctness guarantees by systematically applying formal methods.

In this talk, I’ll give insights into one such application of formal methods. More precisely, I’ll explain how we use Isabelle/HOL to provide a verified implementation of the interpreter for DAML, our smart-contract language. The goal of this talk is to show how one can leverage Isabelle/HOL as a combined implementation and verification environment for core algorithms.