Formal Verification, Virtual Hardware, and Engineering for Blockchains
How high-assurance software development will push open source economic infrastructure forward and help build up trust
Over the last few months, I have been trying to learn as much as I can about the MakerDAO protocol, the people who created it, and why it has been so successful. I have been reading through thousands of Reddit posts, tweets, Medium articles and Git commits. I have been traveling the world to meet as many of the team as possible and learn about why they are the way they are. It has been a really interesting trip down a totally new rabbit hole. At the bottom of this warren I found two fascinating Jedi called Lev and Martin. They have been kind enough to share what they have learnt about building a set of smart contracts that currently contain around $300 million in collateral.
Smart contract engineering is very different from other kinds of software development. When you publish your code to Ethereum, anyone can interact with it. This is a double-edged sword. On the positive side, it means that anyone can build on top of your infrastructure. On the negative side, it means that lots of people will try to attack your code and find bugs. It requires a totally different mentality when it comes to engineering and shipping.
It turns out that other industries have similar requirements. If you are writing code for rockets, airplanes or medical devices, you do not ship untested software rapidly. You architect a solution and build it out carefully, testing everything as you go. This requirement for incredibly high quality code has led researchers and engineers to the practice of Formal Verification.
“Formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics.”
Crafting Virtual Hardware
When Apple releases a new iPhone, it is the culmination of decades of manufacturing expertise and factory design. They spend an enormous amount of time designing the machines that make the objects. Jony Ive has spoke about this endeavor multiple times: Apple spends an insane amount of time making things to make things. Their factory tooling is as important as the final product itself. If they did not invest in their tools, they could could not ship the iPhone to millions of customers every year.
Andy Milenius, the CTO of MakerDAO, coined this wonderful phrase for smart contracts. He called them “virtual hardware” on the a16z podcast.
I think this description really captures the rigor and intensity required to make software that cannot be hacked and will perform as expected. Both Apple and Maker have invested huge amounts of resources in their tools. It pays off over time.
Engineering for Blockchains
The team at DappHub have been working on a set of tools to help smart contract engineers write high quality software for these public and programmable protocols. As an outsider with very little engineering experience, it strikes me that this kind of work requires a mindset shift as well as a new set of practices. The teams building these kinds of contracts encourage people to specify the goals of the code clearly before you leap into the engineering. This seems to go way beyond test driven development and into the realm of total perfectionism.
- How can we formally verify that our code is correct?
- How can we be sure that everyone’s money will be safe in this extremely adversarial network filled with hackers?
- How can we sleep at night knowing we have done everything possible to look after the people who trusted our code?
These are the questions that go flying around my head when I think about how to build systems for blockchains. We have seen so many huge hacks result in so much lost capital.
The people behind the K Framework have been trying to figure out better ways to tell computers what to do for some time. This is from their overview blog post:
“Unlike natural language, which allows interpretation and miscommunication, programming languages are meant to tell computers precisely what to do. Without a rigorous definition of a programming language that unambiguously says what each program does, also called a formal semantics, it is impossible to guarantee reliable, safe or secure operation of computing systems. K is a framework that allows you to define, or implement, the formal semantics of your programming language in an intuitive and modular way. Once you do that, K offers you a suite of tools for your language, including both an executable model and a program verifier.”
DappHub have been working on a suite of tools called klab, which makes it easier to use the K Framework to specify and formally verify smart contracts.
This allows engineers to step through their Solidity code, look at the byte code it generates for Ethereum, and compare it their original specifications. These tools strike me as debuggers for thought. You are constantly checking what something is doing and what you think it is doing.
Lev was kind enough to hold a workshop on all of this and shared a bunch of resources with everyone. If you are curious to learn more, start here:
Engineering Trust
Ethereum gave us the first trustworthy and global computer. Today, it is extremely slow, very hard to use, and monstrously expensive. However, technology is always good at changing those things. It will speed up, it will get easier to use, and it will get cheaper. The unique quality that Ethereum has is its trustworthiness. Anyone can verify that any piece of code did what it supposed to. That is what blockchains are really useful for. Public, programmable and verifiable computation.
In the world of trustworthy computational networks, we need more trustworthy engineering. MakerDAO is built on Ethereum and generates Dai—a stablecoin which tracks the dollar. Thousands of projects are built on top of Dai. Millions of people will use those applications. Every person is trusting that the system beneath them is going to operate correctly.
It is trust all the way down.
