The Ethereum Foundation is proud to announce that I will be joining them as a formal verification engineer. My reasoning is that formal verification can be applied to exceptional situations with great potential value.
- The verification objective follows simple and concise rules (EVM);
- The target is incredibly valuable (ETH, other tokens);
- It is difficult enough to reach the target (any non-trivial programme).
- The community is aware of its importance, and is willing to work with you.
I was a formal verification engineering engineer in my last job. This prepared me for this new challenge. Additionally, I have been involved in two projects related to Ethereum: an internet service called Dr. Y’s Ethereum Contract Analyzer and a Github repo Evidence of Coq. These projects are located at opposite ends of a spectrum that includes automated parser development and manual test development.
I appreciate the collective impact on the ecosystem and an automated parser is appealing. A lot of people would use it, and some would heed its warnings. However, computers cannot comprehend human expectations and should not be taken aback by unexpected behaviour. Therefore, some manual effort is required to communicate human expectations to machines. Contract developers must create a contract in a machine-readable language. Machines need clues to help them comprehend why the implementation is consistent with the specification. Most of the time, this will require more clues than the human. Frequently, an error is found in the specification. This is time-consuming but is necessary when a contract will be worth millions of dollars.
Having an individual devoted to formal methods not only assists us in moving faster in this important and lucrative area but also allows us to communicate better with academia to link the many unique projects that have been presented in the last weeks.
Below are some projects we would like to tackle in the future. Most of these are likely to be in collaboration with other teams.
Solidity:
- Continue to translate Why3 to full Solidity language (perhaps switch to F*);
- Specification in writing Solidity;
- Syntax and semantics for modal logic to reason about multiple parts.
Community:
- Create a map of formal validation projects in Ethereum;
- Collect Solidity codes with errors;
- Analysis of contracts on the Blockchain for Vulnerabilities (related to the LISTENER Tool).
Tools:
- Provide a human-readable and machine-readable formalisation for the EVM. This can also be executed;
- Development of formal verified libraries in EVM Solidity Bytecode;
- A compiler that is formally validated for a small language;
- Explore the potential of interaction-oriented languages (“if X happens, then do Y; you can only do Z if you did A”).
