I will be joining Ethereum as a formal verification engineer. My reasoning: formal verification makes sense as a profession only in an exceptional situation in which
- the verification objective follows short and simple rules (EVM);
- the target has a lot of value (Eth and other tokens);
- the target is complicated enough to do well (any non-trivial program);
- and the community is aware that it’s important to get it right (maybe).
My last job as a formal verification engineer prepared me for this challenge. Also, around Ethereum, I’ve been playing with two projects: an online service called Dr. Y’s Ethereum Contract Analyzer Y a github repository containing evidence of Coq. These projects are at opposite ends of a spectrum between automated parser and manual test development.
Considering the collective impact on the entire ecosystem, an automatic parser built into a compiler appeals to me. Lots of people would run it and some would notice its warnings. On the other hand, since any surprising behavior can be considered a bug, any surprise should be removed, but computers cannot sense human expectations. To convey human expectations to machines, some manual efforts are necessary. Contract developers must specify the contract in a machine-readable language and give machines clues as to why the implementation matches the specification (in most cases, the machine wants more and more clues until the human is). notices an error, often in the specification). This is very labor intensive, but such manual efforts are justifiable when a contract is designed to carry several million dollars.
Having a person dedicated to formal methods not only gives us the ability to move faster in this important but also fruitful area, but also allows us to better communicate with academia to connect the various unique projects that have appeared in recent weeks.
Here are some projects we would like to tackle in the future, most of them will probably be done in cooperation with other teams.
Solidity:
- extend Solidity to Why3 translation to full Solidity language (maybe switch to F*)
- formal specification of Solidity
- syntax and semantics of modal logic for reasoning about multiple parts
Community:
- creating a map of formal verification projects on Ethereum
- collect Solidity codes with errors, to compare automatic parsers
- analysis of contracts deployed in the blockchain for vulnerabilities (related to: LISTENER Tool)
Tools:
- provide a human- and machine-readable formalization of the EVM, which can also be executed
- development of formally verified libraries in EVM or Solidity bytecode
- developing a formally verified compiler for a tiny language
- explore the potential of interaction-oriented languages (“if X happens, then do Y; you can only do Z if you did A”)
