The reliability and security of Smart Contracts largely depend on the consistency of their rule design. This paper introduces a novel approach for analyzing and ensuring consistency in Smart Contracts prior to their implementation. By proposing a formal grammar that captures the concurrent primitives inherent in Smart Contracts, and an algorithm that generates finite state machines (FSMs) from these grammar-based rule sets, the study enables the identification of several problems at the design stage. The paper compares this methodology with related works that focus on post-implementation verification, highlighting the advantages of early-stage analysis. Through theoretical and real-world examples, including an analysis of the DAO attack, the paper demonstrates how inconsistencies can be detected systematically. Finally, a formal definition of consistency is presented, offering a foundation for future tools aimed at enhancing Smart Contract designs.
Dávila et al. (Mon,) studied this question.