For the past three months, I got to experience (remote) life at Digital Asset, working alongside the amazing language team, and combining several passions of mine: functional programming languages, formal methods, state of the art blockchain technology and drinking coffee. In the context of this internship, I developed a formal verification tool for the Daml language. So let me now take this opportunity to answer one of the most common questions regarding Daml: “Does Daml support formal verification?” In short: Yes, it does! Though maybe not in the way you might expect, coming from other tools or languages…
Ensuring that programs are bug-free and behave according to their specification, is a central topic in computer science. In its most basic form, the programmer manually writes down a number of test cases (unit tests) to verify. Using tools like QuickCheck, this process can be largely automated, by defining a number of properties and generating values to test against automatically. However, while these approaches are great for finding bugs, neither approach can guarantee their absence.
This is where formal verification methods come in. Formal verification is commonly associated with theorem provers like Agda, Coq or Isabelle. While these proof assistants are all amazingly expressive, they unfortunately come at the expense of complexity, requiring extensive user interaction to guide the theorem prover. Type systems provide a more lightweight approach to formal verification. While being significantly less powerful than theorem provers, type systems require a much smaller time investment, and can easily be extended for extra features or additional guarantees: e.g. dependent types, linear types, refinement types (Liquid Haskell), etc. Finally, symbolic execution operates by tracking each possible path through the code, and analyzing the operations of functions on their inputs. It’s more automated than proof assistants, while providing guarantees that are hard to express using type systems.
Formal verification is an undeniably valuable tool, which is especially true for applications running on distributed ledgers, particularly in the realm of finance. However, the time and complexity cost of using off-the-shelf theorem provers is often just too high a cost to bear for most applications. Furthermore, proving properties about Daml programs would require an additional, and error-prone, translation step. For this reason, we are currently developing a static analysis tool (based on symbolic execution) for the Daml language, requiring zero user interaction, while operating nearly instantaneously and still being sufficiently expressive for important common use cases.
In order to achieve this feat, we laid out a very specific blueprint for the properties that the static analysis tool can prove: “Does choice X always preserve the total amount of field Y?” Although this might seem very restrictive, in practice it covers one of the most important questions for blockchain formal verification: “Could this smart contract model ever burn money or create money out of thin air?”
Please note that this static analysis tool is still a work in progress, and that the example below might not be representative of the final version. Despite that, let’s have a look at an example! We’ll write a simple Account template, along with a transfer choice to make a deposit from one account to another. Note that if someone tries to transfer more than they own, the choice should just do nothing.
It is clear that making a transfer between two accounts, is expected to preserve the total amount of funds. We thus added an annotation to our code, making our intentions explicit. The IDE can now spin up the static analysis tool, which analyses all possible paths throughout the choice. After passing these results to an SMT solver, the IDE presents us with an error message:
The static analysis tool is warning us that Account_Transfer does not actually satisfy our annotation. More specifically, it turns out that our code produces money out of thin air, by creating more funds than its archives. And indeed, we seem to have forgotten to archive the contract we are exercising the choice on via archive self. Adding this line to the definition of Account_Transfer, greets us with the much more friendly message:
It is important to emphasize that formal verification for Daml is still a work in progress. However, the static analysis is showing great potential, and might find its way to IDE’s near you in the near future! If you’re interested in trying out the prototype for yourself, have a look at the GitHub page for additional information.
We are exploring more ideas for how we can apply this tool in other contexts and verify even more properties of Daml programs, such as statically checking Daml’s authorization rules.
Daml has also a new learn section where you can begin to code online or try DABL here: