Critical to the Ethereum blockchain’s success is the practice of verification, which can be applied to assess the system’s safety. During Bitcoin Wednesday on 3 May, 2017, the Ethereum Foundation’s Formal Verification Engineer, Yoichi Hirai will talk about his work.
He writes:
Amsterdam has a strong tradition of formal logic (search for Arend Heyting and Anne Troelstra if you are interested). Formal logic has been implemented as theorem provers in computers. I’m using that for Ethereum, namely,
1) To remove bugs from Ethereum smart contracts, especially by writing specification and proving it, and
2) To analyze the distributed consensus algorithm at the core of the upcoming proof-of-stake protocols.
Before Ethereum, Yoichi worked in Dresden, Germany for the American cybersecurity firm, Fire Eye. Prior to that he was a researcher for Japan’s National Institute of Advanced Industrial Science and Technology (AIST). He earned his Ph.D. in computer science from the University of Tokyo.
Yoichi Hirai is a formal verification engineer at the Ethereum Foundation. He is interested in turning mathematical proofs into working software. He once visited the University of Amsterdam for half a year because he was fascinated by the constructive logics that originated there. His interest in becoming a