Formal verification – a mathematical means of ensuring that algorithms work as intended – is already used to test a wide variety of systems ranging from integrated circuits and high-speed trains to Amazon services and surgical robots. And it’s being increasingly explored as a way to check for vulnerabilities in smart-contract systems and other blockchain applications.
“Formal verification is a systematic process that uses mathematical reasoning to verify that design intent (spec) is preserved in implementation (RTL),” according to a 2010 article published by EE Times Asia. Because formal verification “algorithmically and exhaustively explores all possible input values over time,” the article continues, it can do for digital designs what simulations cannot: control, measure and observe all potential bugs.
“Formal verification requires you to think differently,” the article notes. “For example, simulation is empirical, i.e., you use trial and error to try to uncover bugs that can take an intractable amount of time to try all possible combinations. Hence, it is never complete. Furthermore, since engineers have to define and generate a significant number of input scenarios, they are focusing their effort on how to break the design not on what the design is supposed to do. Formal verification, on the other hand, is mathematical, exhaustive and allows the engineer to focus solely on intent or ‘What is the design’s correct behaviour?’ ”
Better use of formal verification could have prevented a range of costly software failures, from the damaging Heartbleed bug to the 2012 high-frequency trading “glitch” that cost Knight Capital $440m in a half-hour, according to the blockchain venture Tezos.
“Formal verification has progressed by leaps and bounds in recent years,” Tezos said in a white paper, adding, “it is time to use it in real systems.”
Tezos says its blockchain protocol, written in OCaml, enables formal verification that “helps secure smart contracts and avoid buggy code”.
The use of formal verification could be especially useful in the world of smart contracts, the blockchain-based startup Kadena points out in a 2018 white paper.
“Due to the notoriety of failures and exploits that emerged in the Ethereum ecosystem, the risks of automating central business processes with smart contracts have become apparent,” the Kadena paper states. “Formal verification offers a powerful tool to vastly increase safety and assurance of smart contracts.”
For instance, Kadena says that Pact – its “mini” programming language – uses a formal verification system to ensure that high-value business workflows on a blockchain work as they’re supposed to.
“Instead of requiring human (therefore, error-prone) smart contract authors to try to imagine all possible ways an attacker could exploit their contract – and inevitably make a hundred million-dollar mistake – we allow you to mathematically prove your code is protected against attacks, without requiring a background in formal verification,” Kadena’s communications and media manager Vivienne Chen wrote in a Medium blog post last year.
Another project, Cardano, launched in 2015 with the goal of improving how cryptocurrencies are designed and developed. Cardano’s formal verification approach uses the Haskell programming language to ensure cryptocurrency protocols are clear, reliable, secure and accountable.
"Cryptography and distributed systems are both extraordinarily involved topics with far too many examples of how naive hands can make horrific mistakes,” Cardano says. “Protocols – especially ones to be used by billions of people – are not short lived and rapidly evolving. Rather they are intended to be followed for years to decades. It seems entirely reasonable that, prior to burdening the world with a new financial system we all have to live with for the next 100 years, we want to demand some tedium and rigour from its designers.”
Still, formal verification has limitations, Amy Castor noted in a 2017 article in Bitcoin Magazine.
“Because of the rigour involved, formal methods can be a time-consuming, costly undertaking for projects developing the code,” she writes. “Because of this, formal methods are best used to guarantee smaller building blocks of code that get reused over and over. You would not use it for, say, an entire operating system, but only those parts of a system that require the highest safety or security assurances.”
Such systems, Castor concludes, could clearly include smart contracts involving millions of dollars.
“If, for instance, you had the choice of entrusting your funds to a smart contract that had been formally verified versus one that has not,” she asks, “which one would you choose?”