Eiffel: Extending Formal Verification of Distributed Algorithms to Utility Analysis

The security of distributed systems, such as blockchains, relies heavily on the active participation of sufficient participants within the network. In order to incentivize such participation, different blockchains implement different rewarding mechanisms. However, for these mechanisms to be effective, it is essential that they are fair and accurately implemented, taking into account the rational participants. Consequently, utility analysis plays a vital role in assessing the efficacy of these mechanisms. Formal verification methods, such as TLA+, are commonly employed to ensure the correctness of distributed systems, including blockchains. However, the application of these methods for utility analysis remains relatively unexplored. In this paper, we propose Eiffel, a novel approach that extends the formal verification of distributed systems to encompass utility analysis. By leveraging TLA+, Eiffel enables the analysis of rewarding mechanisms and the detection of potential attacks. Eiffel focuses explicitly on the concept of Nash equilibrium, a fundamental notion in game theory that holds significant importance in utility analysis. Through the use of Eiffel, we demonstrate its versatility with different specifications, highlighting its applicability in committee-based blockchains and the Tendermint consensus algorithm. Our analyses show the effectiveness of Eiffel in evaluating rewarding mechanisms and identifying potential vulnerabilities.