Deductive Verification of SmartML Smart Contracts with KeY

Smart contracts play an increasingly central role in financial systems, decentralized applications, and digital asset management. Their execution is typically irreversible, and even small errors in contract logic can lead to permanent loss of funds or unintended behavior. For this reason, the design of smart contracts requires a level of assurance that goes beyond traditional software testing. Yet, smart contracts combine stateful updates, external interactions, and intricate failure modes, making them difficult to analyze with conventional programming and quality-assurance techniques.

SmartML [15] was introduced to address the modeling side of this challenge. It is a domain-specific, executable modeling language with a formally defined operational semantics [13], designed to capture contract behavior at an abstract and implementation-independent level. Its key features include explicit transactional control, resource-aware operations, and algebraic data types, thereby enabling developers to express contract logic precisely and unambiguously. With this, it is possible to write clearly structured smart contract implementations. However, the language by itself does not provide formal guarantees about correctness. For safety-critical smart contracts, such guarantees are essential.

Deductive verification is a natural fit for verifying functional correctness and transactional safety of smart contracts, as it allows one to prove the absence of entire classes of errors rather than detecting individual bugs. However, existing deductive verification tools do not support SmartML, and its distinctive constructs – most notably its explicit transactional execution model – cannot be analyzed directly within established verification frameworks.

The goal of this paper is to enable deductive verification of SmartML models using the KeY verification system. We achieve this by introducing SmartJML, a lightweight specification layer for expressing correctness properties directly in SmartML, and by defining a semantics-preserving translation from SmartML+SmartJML to Java Card annotated with JML, the input language supported by KeY. As a result, correctness proofs carried out in KeY are sound with respect to the behavior of the original SmartML contracts, including their transactional execution.

Our work builds on the previously introduced SmartML framework, which already provides the modeling language itself, its formal operational semantics, and a type-system-based analysis for safe reentrancy [15]. These aspects are assumed in the present paper and are not re-developed here. The novelty of this work lies instead in enabling deductive verification for SmartML: we introduce SmartJML as a specification layer, define a translation from SmartML+SmartJML to Java Card annotated with JML, and thereby make KeY applicable to SmartML models. In summary, the contributions of this paper are:

• $\mathrm{■}$

  we extend the existing SmartML framework with SmartJML, a JML-style specification layer for writing method contracts, invariants, and ghost variables directly at the SmartML level;

• $\mathrm{■}$

  we define a translation from SmartML+SmartJML to Java Card+JML that encodes SmartML’s transactional execution model in a form suitable for deductive verification with KeY;

• $\mathrm{■}$

  we provide a tool-supported implementation of this translation pipeline, generating Java Card/JML artifacts automatically from annotated SmartML models;

• $\mathrm{■}$

  we evaluate the approach on escrow case studies and demonstrate that correctness properties of SmartML contracts can be established in KeY, including transactional reasoning.

These contributions establish a verification workflow for smart contracts, illustrated in Figure 1. Starting from a smart contract, the developer models it in SmartML and annotates it with SmartJML specifications. The translation produces a Java Card/JML representation suitable for deductive verification with KeY. A successful proof implies correctness of the original SmartML model with respect to the specified properties, and – assuming faithfulness of the model – of the intended smart contract.

The paper proceeds as follows. Section 2 provides background on SmartML and KeY. Section 3 introduces SmartJML and in Section 4 we discuss our translation to Java Card/JML. Section 5 describes our implementation, while Section 6 evaluates it on a representative case study. Finally, Section 7 discusses related work, and Section 8 concludes with future research directions.

This section summarizes the technical background required for our verification workflow, focusing on the SmartML modeling language and the KeY deductive verification system.

This section introduces SmartJML, our JML-inspired specification layer for SmartML. SmartJML provides a set of JML-style specification constructs that can be embedded directly into SmartML programs. In the following, we introduce these constructs step by step using small, focused examples. SmartJML is written as comments inside the SmartML code.

KeY reasons about Java programs annotated with JML and provides dedicated support for the Java Card dialect; it has no native notion of SmartML contracts, resources, or transactions. We therefore translate each SmartML construct into a Java Card/JML counterpart that simulates its semantics. The translation is defined on top of the formal operational semantics of SmartML, and we only sketch its main ideas here.

From a semantic perspective, a SmartML program is executed according to the operational semantics defined in [15]. A method contract in SmartJML therefore represents a partial correctness specification over these semantics: a precondition $P$ and postcondition $Q$ constrain the set of reachable configurations before and after evaluating a SmartML method. In particular, SmartML’s transactional execution model induces two kinds of postconditions, depending on whether a transaction commits or aborts. This distinction is reflected explicitly in SmartJML.

The goal of our translation is to ensure that such specifications are preserved under translation: iff a SmartML program satisfies a SmartJML contract with respect to its formal semantics, then the generated Java Card program satisfies the corresponding JML contract with respect to the Java/JML semantics implemented in KeY. Formally, for a method $m$, we can write

where $\rho \in \{\mathrm{𝗌𝗎𝖼𝖼𝖾𝗌𝗌},\mathrm{𝖺𝖻𝗈𝗋𝗍}\}$ captures the transactional outcome and $T$ denotes our translation. Therefore, in this section, we outline the design choices and requirements that make this preservation feasible.

The implementation follows the theoretical translation principles introduced in the previous section and produces a Java Card program annotated with JML. This program can then be loaded directly into KeY for verification. We also provide a repository containing our implementation¹¹1https://github.com/TudorBalan/SmartJML.

The translator is implemented in Java and follows a structure similar to that of a source-to-source compiler: it takes a SmartML program as input, parses it into a parse tree which our translator turns into an abstract syntax tree (AST), transforms this AST into a JML-annotated Java Card AST, and finally generates Java Card source code compatible with KeY. The workflow of our translator is illustrated in Figure 3.

Our translator also translates SmartJML specifications to JML. This feature does not yet cover all possible SmartJML constructs, which is planned as future work. While not a fundamental limitation of the approach, some auxiliary specifications – such as loop invariants – currently need to be written directly in the generated Java Card program. In practice, this affects only a small portion of the specifications: in our case study, loop invariants were required only for recursive operations over ADTs, while the remaining contracts were translated automatically without manual intervention.

In the implementation, our translator uses ANTLR [12] and JMLParser²²2JMLParser repository on GitHub: https://github.com/jmltoolkit/jmlparser, which extends JavaParser [14] to include functionality for parsing and generating JML code. The parser is generated using ANTLR and the code generation is almost completely handled by JMLParser. This only leaves us having to implement the translation of the two ASTs by hand, for which both ANTLR and JMLParser again provide useful functionality. The choice of our tools led to a major reduction in required development time. Furthermore, following best practices for building a source-to-source compiler, such as the usage of the visitor pattern and designing the translator modularly, has led to a robust code base that is easily extendable for when SmartML is expanded in the future.

To illustrate our verification workflow, we consider a practical example: a SmartML escrow contract. Escrow contracts are commonly used in online marketplaces, where a third party holds the buyer’s funds until the promised goods are delivered. Our case study shows how to model the contract in SmartML, specify its properties in SmartJML, translate it to Java Card, and verify it using KeY.

Due to the safety and security of smart contracts being of utmost importance, given the financial incentives involved, numerous approaches have been proposed for the purpose of verifying the behavior of smart contracts and preventing attacks. The use of KeY for the deductive verification of smart contracts is discussed in [7]. This work shows that multiple classes of correctness properties are suitable for verification with KeY. The authors also present an approach for the deductive verification of Hyperledger Fabric smart contracts with KeY in [6]. They achieve this by extending KeY with functionality for Fabric ledger implementations, which differs from our translation approach. Another verification methodology that is quite similar to ours is proposed in [8], which focuses on verifying smart contracts written within the EVM environment and uses Dafny instead of KeY.

A similar approach to the translator which we have built is seen in Javadity [4], a translator for Solidity programs to Java including JML for the purpose of verifying these programs using KeY. Solidity is a programming language designed for the development of smart contracts which run on the Ethereum Virtual Machine (EVM). Consequently, Javadity is only capable of verifying smart contracts which have been written in Solidity and are therefore designed to run on the EVM. SolidiKeY [3] is a verification tool for smart contracts written for Solidity and based on KeY, which is also limited to the verification of smart contracts written in Solidity. The process of translating SmartML and SmartJML to Java Card and JML differs notably from previous approaches that translate Solidity programs to Java for verification with KeY. One key difference is that SmartML now provides a dedicated specification language (SmartJML), allowing contracts to be annotated with verification properties directly at the modeling level before translation. Furthermore, SmartML includes language constructs that do not have direct counterparts in Solidity, such as the explicit transactional statement try … abort … success …, which models rollback semantics for external calls. The translation therefore needs to encode these semantics explicitly using Java Card’s transactional memory mechanism. In addition, SmartML follows a simplified state model in which the persistent state consists only of contract fields and no shared mutable state across contracts. These characteristics lead to different translation challenges compared to Solidity-based approaches.

Another approach of verifying smart contracts is through the use of model checking, as in [5] the authors propose a formal method to construct models for smart contracts in ProMeLa. These models can then be verified using the SPIN model checker. Similarly, in [1] the authors employ a statistical model checking approach in which the smart contracts as well as the users and the decentralized ledger are all represented as timed automata. Furthermore, static analysis techniques are used for smart contracts, as for example seen with Oyente [10]. Oyente is a tool used for bug finding that has the capacity to perform reentrancy detection as well as other analyses. However, this method relies on symbolic execution which makes it unable to guarantee the absence of false negatives. This approach is also not compositional, thereby disabling verification that is independent of the external contract’s behavior. Consequently, Oyente is incapable of blocking cross-contract reentrancy, thereby hindering the ability to protect against cross-contract reentrancy attacks. Since SmartML is blockchain-agnostic, our approach is not tied to the EVM and supports expressive first-order specifications beyond typical finite-state model-checking workflows.

In this paper we proposed a verification workflow to deductively verify SmartML smart contract models using the well-established verification tool KeY. We did this by developing a translation from SmartML smart contract models to Java Card to allow the use of KeY for SmartML models. We found that the translation cannot be fully equivalent in every case due to assertions reverting fields in SmartML. Therefore, we are able to translate a subset of SmartML that does not allow nested transactions within a method and limits assertions to the first and last line of a method. We also extended SmartML with SmartJML to allow for specifications to be written within SmartML programs. Furthermore, we developed a tool that automates the translation process from SmartML and SmartJML to Java Card and JML. Some SmartML programs still require manual translation of some SmartJML expressions, especially when working with algebraic data types. Lastly, we have also shown our verification workflow in action through the context of a case study.

The main advantage of our verification workflow is that it allows smart contracts to be deductively verified, demonstrating the absence of errors, not just their presence, in addition to the safety and security guarantees already provided by SmartML. Meanwhile, its main drawback is that it becomes increasingly complex to prove properties about a program the larger it gets. Especially when working with algebraic data types, the effort required to verify a smart contract model increases substantially due to KeY’s increased proof complexity when dealing with recursion. Nonetheless, having the ability to formally verify smart contract models, thereby increasing the functional correctness and security of critical applications such as smart contracts, is highly useful.

As of now, the translator only supports a subset of SmartJML specification. Expanding the translator’s SmartJML to JML translation would further increase the accessibility and usefulness of writing specification in SmartJML.