Engineering isabelle formal verification

What is Formal Verification and what it means for Daml

author by Gert-Jan Bottu June 30, 2020

In this article

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…

What is Formal Verification?


Overview figure situating proof assistants, unit tests and type systems

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.

Agda vs Coq vs Isabelle formal verification.
Agda vs Coq vs Isabelle formal verification.

Formal Verification in Daml

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?”

How the demo works

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:

What is the Future of Formal Verification in Daml?

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:

 Learn Daml online

 

Formal Verification

DAMLquestionsandanswerson-formal-verification

What is formal verification in software engineering?

Formal verification means proving that programs behave correctly according to their specification, using formal methods.

What are the most common formal verification programming languages?

While formal verification is usually associated with theorem provers (the most common of which are Agda and Coq), languages with strong type systems (like Haskell) also provide a form of formal verification.

What is symbolic execution?

Symbolic execution is a kind of formal verification, analysing a program by investigating all possible paths (branches) throughout the code, in function of their inputs.

What is the difference between formal verification and functional verification?

Functional verification tries to answer the question whether the program behaves as expected. Formal verification provides a way of answering this question, specifically using formal methods.

Are there any good formal verification books?

The Software Foundations series provides a great introduction to most of the topics handled in this post.

What is the difference between eager and lazy evaluation?

Eager, or strict, languages evaluate expressions as soon as they appear in the code. Lazy languages, on the other hand, delay evaluation until the values are actually needed. This avoids needless work when the values are never used, but might result in harder to predict performance.

What does it mean for a language to be purely functional?

These languages force a functional style of programming, based on mathematical functions, and avoiding side effects.

What are side effects in programming languages?

A program has side effects if it has any other effects, besides returning an outcome to the user. Examples include modifying state, performing I/O operations, reading the system clock, etc.

Keep Reading