Arrow icon
Ness Labs: Make the most of your mind
Learn more about Joggo

A Summary of

Devcon3 panel on formal verification

by
Phil Daian, Everett Hildenbrandt, Yoichi Hirai, Loi Luu, Reto Trinkler
View original

Formal verification is the act of proving or disproving a specified algorithm.

What makes a good specification?

  • It should accurately capture the intent of the developer
  • It should also encode all of the assumptions of the smart contract
  • This is much easier said than done
  • It should be easy to understand & should follow a standard
  • It should put the contract in the scope of a bigger picture
  • However, any specification is better than no specification!
  • As long as it can be tested, regardless of mathematical or abstract basis, it is advantageous

Verifying hardware vs. smart contracts/blockchains

  • Smart contracts are bounded by their execution times & are generally very simple
  • There is great demand from users for this technology
  • There is an opportunity to set standards for software
  • Ethereum, for example, has non-deterministic specification, a huge improvement

Challenges of formal verification

  • Interactive theorem proving is not user-friendly
  • Smart contracts are difficult to prove-- they must be represented in a mathematical model first
  • Most companies don't have people with the strong backgrounds required to do this
  • There's a wide range of correctness techniques possible: formal, semi-formal & informal
  • The context matters for what technique may be best
  • Formal verification is super expensive & still not a total guarantee

How can we develop tools/approaches that are accessible to users?

  • Logical formulas are reasonable for users to understand
  • Alternatively, tools which require the user to just copy & paste without deep understanding are a possibility
  • Sufficiently motivated developers are needed to improve these tools
  • It is also useful to take these approaches out of academia-- more broad participation can increase accessibility

How can formal verification become mainstream?

  • It is still the user's responsibility to understand the contract they are interacting with
  • A bottom-up push from users being selective will incentivize rigorous development
  • Developers need to respond & enable them

Role of auditors

  • Auditors should inform the team of what may be useful & available
  • However, it is the team's responsibility to follow up on this themselves
  • They should complain more about the tools!

Challenges of verifying most complex contracts

  • The more complicated, the more experimental your contract will be
  • New specifications must be written instead of reusing old building blocks
  • It is crucial to find all of the vulnerabilities
Related content
See all posts
Arrow icon