Formal Analysis of Smart Contracts: Applying the KeY System

Smart contracts are programs running on decentralized, distributed ledger platforms. Rigorous formal analysis of these programs is highly desirable because they manage valuable assets and therefore are a prime target for security attacks. In this paper, we show that the computation model of smart contracts allows the application of formal methods designed for analysing single-threaded imperative programs. We discuss different classes of correctness properties and the formal methods that may be applied. Furthermore, we show how deductive program verification in particular can be used to prove correctness of smart contracts, and we discuss two approaches where we have applied the program verification tool\ua0KeY