In Formal Verification Push, Ethereum Seeks Smart Contract Certainty

There's a new blockchain buzzword arriving in time for fall – formal verification.

The phrase (used to describe the application of mathematics to verify software programs) has so far been evoked sparsely in the press. But if conversation at ethereum's developer summit last week was any indication, it could play an increasing role given the security questions that still surround smart contracts and blockchains more broadly.

As evidenced by multiple talks dedicated to the subject at Devcon2, the idea that new assurances could be given to ethereum coders is being widely embraced by its development community. Already, the concept is being proposed as a way to inspire confidence in everything from the ethereum protocol itself to its experimental proof-of-stake blockchain.

That this has come to pass is perhaps no surprise given the sudden collapse of The DAO this summer, to date the largest smart contract yet launched on the decentralized application development platform.

But while formal verification may sound complex, the concept can perhaps be summed up succinctly as applied to ethereum – coders currently use a largely new language (solidity) to write smart contracts, writing commands that are then translated into bytecode for use by the ethereum virtual machine (EVM) and disseminated to the network's nodes for execution.

In a sense, formal verification can be seen as a more objective way to ensure that when different component parts of the network receive these instructions, they execute them as intended on behalf of users.

Grant Passmore, co-founder of Aesthetic Integration, is one entrepreneur who sees an opportunity in helping assist in this effort, using Devcon2 to launch Imandra Contracts, a formal verification platform for blockchain smart contracts.

At the event, he evoked the idea that ethereum could serve as a "paradise" for formal verification (a widely cited touchpoint in talks) given the aims of its community and the significant responsibilities it wishes to entrust to code.

Passmore told CoinDesk:

"The ethereum community is in a unique position, where after The DAO, we understand that rigorous engineering is necessary. You can't approach writing a smart contract like a web app."

Elsewhere, speakers like Cornell's Philip Daian spoke to the interest in the methodology more broadly, telling the audience he believes formal verification could help ethereum solve key issues.

"It's going to be one critical piece of the overall picture. I'm looking forward to using ethereum to set the standard and show people how it's done," he said.

Training wheels

Given the recent emphasis financial firms have placed on exploring smart contracting languages, it was perhaps the concept of applying formal verification to Solidity that was the most frequent topic of discussion.

Developed for the ethereum platform, Solidity has faced criticism for being largely untested and difficult to write, largely because it is so new. Such issues have arguably been amplified due to issues with the language’s compiler, a lack of public libraries and the collapse of The DAO, which was vetted by notable members of its development community.

In this light, Christian Reitweissner, the creator of Solidity, acknowledged that there is a drive to implement formal verification so that errors can more effectively be detected by ethereum coders.

Reitweissner told CoinDesk that smart contract developers could one day use formal verification tools to, for example, determine if there are unforeseen errors in their work. He indicated that such a tool could be used to determine if, in adding two balances, the result extended longer than the field allotted by the compiler.

"This could happen and the formal verification tool [would] automatically detect that. You can detect it early on and react on that inside the smart contract," he explained.

Reitweissner said that the Solidity team has already been exploring how to apply formal verification to its work. As early as last October, there were prototypes for how a toolkit called Why3 could be used for this purpose, though such offerings are not yet available for the full language.

Proving ground

That ethereum could be used to test how formal verification might be applied to finance more broadly was also a heavily discussed topic during the conference.

Passmore, for instance, said Aesthetic Integration has been working on applying formal verification in work with financial institutions since 2014, and that so far, clients have sought to use it in limited areas, like dark pools, where traders require certainty about fairness.

In smart contracts, Passmore suggested he sees ethereum as a community that could drive acceptance further.

"Many of our banking clients, as we started working with them, we heard they were interested in the space, but that they were worried about the correctness of smart contracts," he said.

The advancement of formal verification has also attracted Yoichi Hirai for similar reasons. A formal verification engineer now employed by the Ethereum Foundation, his interest in the concept began as a researcher and in his prior employment at cyber security leader FireEye.

In a talk at the conference, Hirai spoke about his frustration applying formal verification in settings where he did not have access to the source code, or the tasks were perhaps too broad to advance the concept.

"I found ethereum, I saw the EVM, the yellow paper, the specification, it was only 32 pages and I thought I can actually translate it and write proofs about smart contracts," he said.

Ethereum, by contrast, offers what he called a "smaller specification" and a "solvable problem" for engineers in determining how best to translate Solidity into bytecode.

"I believe many more formal verification researchers are coming," he said.

No silver bullet

Yet despite the enthusiasm, there are steps being taken to caution how much formal verification could achieve. Developer Alex Beregszaszi, who is working on upgrades to the EVM, spoke to the need for a suite of solutions to help developers ensure smart contract code is working as intended.

Passmore, too, noted that it’s difficult to say whether his new system could have caught issues with The DAO as formal verification tools still require human input.

"You can encode issues that happened with The DAO and check to make sure that you don't have those, but you have to know what to look for," he explained.

The limitations were acknowledged by Reitweissner and Passmore, both of whom cautioned developers not to think of formal verification as a “silver bullet”.

Reitweissner, however, sees the methodology as one that will advance as it is more widely used, with developers becoming slowly better at identifying issues and developing repositories where knowledge of common problems can be made accessible

In this way, Passmore believes the ethereum community is succeeding in "evangelizing" for the concept, something he believes will ultimately advance blockchain research.

Passmore concluded:

"Even though this is something that many have never been exposed to, formal verification is what we need. It's a learning curve, but it must be embraced, and that's exciting."

Images via Pete Rizzo for CoinDesk