本文最初发布在以太坊博客.
今天，我很高兴地宣布，Yoichi Hirai（GitHub 上的 @pirapira）将加入以太坊项目，担任形式化验证工程师。他拥有东京大学关于形式化通信并行进程的博士学位，并在业余时间为以太坊创建了形式化验证工具。
用他自己的话说
我将加入以太坊担任形式化验证工程师。我的理由是：形式化验证只有在很少的情况下才适合作为职业，即
- 验证目标遵循简短、简单的规则（EVM）；
- 目标具有极高的价值（ETH 和其他代币）；
- 目标足够复杂，需要正确处理（任何非平凡的程序）；
- 并且社区意识到正确处理的重要性（也许）。
我最后一次担任形式化验证工程师的工作让我为这项挑战做好了准备。此外，围绕以太坊，我一直使用着两个项目：名为 Dr. Y’s Ethereum Contract Analyzer 的在线服务和 一个 GitHub 存储库，其中包含 Coq 证明。这些项目位于自动分析器和手动证明开发之间的光谱两端。
考虑到对整个生态系统的集体影响，我对集成到编译器中的自动分析器感到兴趣。许多人会运行它，有些人会注意到它的警告。另一方面，由于任何意外行为都可以被视为错误，因此应消除任何意外行为，但计算机无法感知人类的期望。为了将人类的期望告知机器，需要一些手动操作。合约开发人员需要使用机器可读的语言指定合约，并向机器提供提示，说明实现方式与规范匹配（在大多数情况下，机器需要越来越多的提示，直到人类意识到错误，通常是在规范中）。这是劳动密集型的，但在设计用于承载数百万美元的合约时，这种手动操作是合理的。
专门从事形式化方法的人员不仅使我们能够在这一重要且富有成效的领域中更快地前进，而且也有助于我们与学术界更好地沟通，以便连接过去几周出现的各种独立项目。
以下是一些我们希望在未来解决的项目，其中大部分可能与其他团队合作完成。
Solidity
- 将 Solidity 扩展到 Why3 的翻译，以涵盖完整的 Solidity 语言（也许切换到 F*）。
- Solidity 的形式化规范。
- 用于对多方进行推理的模态逻辑的语法和语义。
社区
- 创建以太坊形式化验证项目的映射。
- 收集有错误的 Solidity 代码，用于基准测试自动分析器。
- 分析区块链上的已部署合约是否存在漏洞（相关：OYENTE 工具）。
工具
- 提供 EVM 的人类和机器可读的形式化，它也可以执行。
- 在 EVM 字节码或 Solidity 中开发形式化验证的库。
- 开发一个小语言的形式化验证的编译器。
- 探索面向交互的语言的潜力（“如果发生 X，则执行 Y；只有在执行了 A 的情况下才能执行 Z”）。