You may have heard that Cardano ADA is aiming for formal verification of its core software.
What does it mean for software programs to be formally verified? Why is it important for cryptocurrencies?
In this article we take a quick and superficial look at formal verification and why it may be desirable in the future of cryptocurrencies.
There are several methods for testing software. One of them is called black box testing, where you treat software like a black box and inject data into it, taking note of the data that is output. This kind of test is not interested in how the software does what it does, but only if the output is correct. It’s called black box testing because you treat the software like a black box, not caring what it does, how it does it.
Most methods for testing software use some similar strategy: they pump tons of possibilities into the software and verify that the outputs are the expected values.
For this to work, you need to know the expected values and you need to provide these correct values to the testing routines for them to be able to compare the outputs to the expected values. It is a well known principle of computer science that you cannot have software test itself for correctness and cover all possibilities – software must be trained in order to cover a LOT of possibilities, but not all.
This limitation of software engineering has intrigued computer scientists, mathematicians and logicians for a very long time.
It depends on the rules of the programming system you use. There’s a special case where you can assure that programs are perfect.
There is a mathematical technique called formal verification, through which if you limit what your software can do to some specific rules and you control the inputs to the software, then you can assure that this software is perfect.
One of the limitations imposed on formally verified software is that it cannot, under any circumstance, be able to run infinite loops.
Software which is verifiable must be guaranteed to always finish executing, which avoids one of Alan Turing and Alonso Church’s most notable scientific result: the halting problem.
The halting problem states that no algorithm is able to determine whether any other algorithm will finish executing one day. That is, computers are unable to know whether another computer will halt or not, for all problems given.
If you exclude the halting problem from the computer’s programming system, then you can avoid this pitfall and software becomes verifiable.
Software which is guaranteed to finish executing is also limited, for obvious reasons.
Every routine must show the verification system how it plans on stop executing.
The Coq Proof Assistant, for example, is one such formal verification system and it imposes a constraint that all whole number functions be decreasing and must reach zero. This guarantees that after a certain number of iterations the counter will eventually reach zero and therefore the routine will halt. Other formal verification systems impose similar restrictions on software in order to avoid the halting problem.
There are shortcomings to formal verification, as you can imagine. We’ve already mentioned one of them: formally verified software is restricted in what it can do. You must adapt to these limitations in order to work with formally verified code.
Another limitation is how difficult it is to formally verify even the most basic algorithms. A simple bubble sort or insertion sort algorithm, two of the most trivial sorting strategies (like sorting a deck of cards by moving and inserting cards in your hand), require hundreds of lines of formally verified code. They must restrict every input and every subroutine and this quickly becomes a large verification routine.
This is one of the biggest complicating factors found in formal verification systems. Since they’re based on strict mathematical principles, every little step of the way must be proven like a theorem.
If you say “reverse this list of numbers”, after reversing it you must prove mathematically that the list has indeed been correctly reversed. For instance, should a list be sorted, you must prove that for every item in the list the item before the next is smaller than the next. To do this, you create a subroutine to prove this fact, like “prove_sorted(mylist)”, then prove_sorted itself must be proven, and this chain of proofs runs until you reach a fundamental mathematical truth called an axiom. Axioms do not need to be proven, as they are the basis on which math is built. As you can see, formal verification is a very expensive process.
Every single step of a software program must be linked to a fundamental axiom of math or it will not be accepted. Then, after you have proven every single step to be mathematically correct, then when you wire all these steps up together you are guaranteed to have mathematically perfect software.
From the above description of the workflow involved in formal verification, the reader must have deduced by now that it is a very slow and painstaking process. And it is. Formally verified software is very expensive to build and it requires extremely high qualifications from its developers.
You can easily recruit PHP, Python, Scala and Java developers, but Haskell, the functional programming language used in Cardano ADA has a much smaller group of developers. Functional programming languages are used in lots of formal verification systems because of their close relation to math. Coq generates formally verified code in the OCaml programming language, a language based on ML and developed in France ( ML is also a very popular family of functional programming languages). All these functional programming languages usually present difficulty during recruitment. It’s hard to find good ML programmers, especially because the market offers much more job openings for popular languages like PHP, Perl, Java and C/C++.
But the market for functional programming languages is expanding fast, thanks to large projects like Scala, Akka, Apache Spark and the Haskell community itself which is quickly growing and gaining more fans every year. Still, the market reality is that functional programming is still a lot more expensive than other methodologies and formal verification almost certainly will require knowledge of some functional programming concepts.
A technique exists which applies methods from formal verification along with more traditional software testing techniques.
This mixed strategy is often called semi-formal software verification.
While it is a highly effective technique that reduces the complexity of software verification, not requiring strict mathematical proof for every step of the program, it does not provide the 100% assurance that purely formal methods do.
Formal verification is a mathematical method for making sure software is correct. We mean “correct” in the strict mathematical sense of the word: formally verified software is 100% correct. (Unless the underlying machine fails somehow, the software will not.)
The mathematical strictness imposes a set of limitations on what the software can do, but the end result is perfectly verified correct software. It adds cost and development complexity to a project and is not suited for every software application. In fact, projects which use formal verification are usually very critical and related to health and hospital systems, nuclear power systems, military systems and other critical applications which simply cannot fail.
Cryptocurrencies and financial systems can be classified as critical and formally verified systems will have their place in this niche as well. Cardano ADA is one large project which aims to be formally verified and probably the most advanced attempt so far in this direction.
We hope this article has given you a perspective on this interesting field of software engineering and how it relates to cryptocurrencies.
As more and more software projects adopt this methodology you’ll end up hearing lots about formal verification systems and we hope this introduction will allow you to understand what it means when cryptocurrencies claim they have been formally verified.