Smart contracts are programs stored on a blockchain that can be used to automate agreements and transactions. Their immutable nature carries the risk of financial losses due to vulnerabilities and bugs. Consequently, verification processes, often supported by formal methods, are indispensable in mitigating these risks. Constrained Horn Clauses (CHCs) are commonly used for representing verification conditions (VCs) in smart contract analysis and verification, and several tools have been developed based on CHCs. Despite their utility in formal verification, CHCs pose a challenge in terms of human readability. In this paper we present preliminary work in the development of a tool aimed at visualizing CHCs, helping experts inspect VCs and their correspondence with smart contract code during the auditing process. The tool combines diferent translations in order to generate Predicate Dependency Graphs (PDGs), depicting the relationships among CHC predicates that have been derived from smart contract functions and the properties under verification. While the current representation of PDGs is static, future developments aim to render it dynamic and user-friendly. This enhancement would enable auditors to selectively display sections of the PDGs, interact with nodes and the associated clauses and code, apply CHC transformations and invoke CHC satisfiability solvers.
Originally introduced as the foundational technology for the Bitcoin [
The blockchain is replicated on multiple nodes that use a consensus mechanism to confirm and add transactions to it. Blocks are cryptographically linked to each other, forming a secure chain that makes tampering dificult. This ensures the blockchain’s integrity and immutability.
The potential applications of blockchain technology are numerous, ranging from financial
services and supply chain management to healthcare and voting systems. Blockchains can
also be used to store smart contracts [
Many of the formal verification tools that have been developed for smart contract analysis use Constrained Horn Clauses (CHCs) (e.g. SeaHorn2, RustHorn3, JayHorn4) as an intermediate language to represent the verification conditions (VCs) for properties. However, for several reasons, CHCs are dificult to read and interpret (see Section 2). In this paper we present a prototype tool for CHC visualization that we have developed to aid developers analyse Solidity smart contracts. The tool takes as input Solidity smart contracts, annotated with properties, and produces a Predicate Dependency Graph (PDG), whose nodes correspond to predicates and whose edges represent the predicates dependencies.
The rest of the document is structured as follows: in Section 2 we provide some details of smart contract verification, with a focus on CHCs and auditing processes. In Section 3 we describe the CHC visualization tool and in Section 4, we demonstrate the tool’s application to a basic smart contract, emphasizing the challenges in interpreting Horn clauses and the outcomes of transformations derived from the tool. In the last section we discuss related work and possible improvements.
Several tools have been developed over the past years to analyse the security of smart contracts,
see [
Properties for Solidity smart contracts can be specified in the form of Hoare triples using require() and assert() annotations. If a precondition, specified with require(), is satisifed at the beginning of code execution, and the code executes correctly, then a postcondition specified with assert() will be checked at the end of code execution. So, while the assert() function is used to test internal errors and verify invariants, the require() function is used to guarantee valid conditions, such as correct inputs, contract status variables or the return of valid values from calls to external contracts.
Ethereum smart contracts can also fail for other reasons. For instance, transactions can fail due to the lack of a suficient amount of gas for code execution. The failure of a transaction may 1Approximately $773 million in 2023.
Source: https://www.slowmist.com/report/2023-Blockchain-Security-and-AML-Annual-Report(EN).pdf 2https://seahorn.github.io/ 3https://github.com/hopv/rust-horn 4https://jayhorn.github.io/jayhorn/ result in several consequences, including the loss of the funds invested in the transaction, the gas fees paid to execute the transaction and, in some cases, the execution of any transactions preceding the failing transaction may be reverted.
Many recent program analysis and verification methods [
CHCs provide a formal framework for expressing verification conditions (VCs), allowing
developers to specify properties and constraints that smart contracts must satisfy. One of the
strengths of CHCs lies in their ability to capture complex program behaviors and dependencies
and summarize them into a standardized framework. This formal verification process provides
mathematical certainty about the behavior of smart contracts, strengthening confidence in their
security and reliability. Several tools for smart contract verification based on CHCs have been
developed, such as SmartAce [
Smart contracts are often manually reviewed by expert auditors. Auditing aims to identify and assess risks, vulnerabilities, compliance issues and technical defects in the smart contract.
During smart contract auditing it is important for verification engineers to be able to inspect the VCs in CHC format. Unfortunately, these clauses are often dificult to be read by humans. In particular, if we consider the CHCs generated by SolCMC, we note some critical issues: (i) CHCs are in SMT-LIB5 format, a quite verbose format that uses prefix notation, that further hinders readability, (ii) CHCs contain several clauses and predicates that are generated to represent diferent scenarios, such as the success and failure of function calls, the relationship between the input and output of a function (function summaries), constructor and function initialization, (iii) predicates may exhibit mutual dependencies, which may increase the dificulty of understanding the CHCs. Thus, finding a direct correspondence between the generated CHCs and the original Solidity source code can be challenging. Therefore, there is a need for a tool to assist verification engineers in graphically inspecting the VCs in CHC format.
Providing a visual representation of the dependencies that exist among the CHC predicates can be useful during the auditing process to ease the understanding of the smart contract behaviour and increase the confidence in the correctness of the VC encoding. We have developed CHCViz, a tool that takes as input a Solidity smart contract and a property, specified using require() and assert() annotations, and generates a Predicate Dependency Graph (PDG), whose nodes correspond to CHC predicates and whose edges represent the dependencies among predicates.
The tool has been implemented as a Python script that coordinates the execution of the following stages: • CHC Generation: generation of CHCs in SMT-LIB format from the Solidity smart contract; • Prolog encoding: translation of the CHCs from the SMT-LIB format to Prolog format; • PDG creation: creation of the PDG in the Graphviz DOT format; • SVG generation: generation of the PDG in Scalable Vector Graphics (SVG) format.
CHC Generation The process initiates with the generation of the CHCs in SMT-LIB format from the annotated Solidity contract. The CHC generation is performed by invoking the SMTChecker module, also known as SolCMC, of the Solidity compiler6 by specifying assert as the only verification target. The satisfiability of the generated CHCs encode the validity of the property for the contract: if the CHCs are satisfiable then the property is valid.
Prolog Encoding After the generation of CHCs in SMT-LIB format, the subsequent phase involves their translation into Prolog format using Eldarica7. The Prolog format is less verbose and more human readable than SMT-LIB and is also the input format required by the tool used in the subsequent phase.
PDG Creation In this phase, taking as input the CHCs in Prolog format generated by Eldarica, we invoke Logtalk8, a Prolog-based declarative object-oriented logic programming language, for creating the PDG specification that encodes the dependencies among the CHC predicates. The PDG is generated as a GraphViz9 DOT file containing all the information needed for displaying the graph. The DOT language is very flexible: it supports diferent attributes of nodes, edges, graphs, and various layout engines and output formats.
SVG Generation In the final phase, the PDG is transformed into an SVG file format using Graphviz. The SVG format has been chosen among other formats, because of its scalability and of its support for interactivity through JavaScript and CSS.
We have run CHCViz on 187 contracts taken from [
We now consider a smart contract that implements a simple banking functionality (Listing 1) allowing users to deposit and withdraw funds from their balance, stored in the contract, via the deposit() and withdraw() functions, respectively. The address of the sender of the message initiating the transaction and the amount of wei, the smallest subunit of Ether (the native cryptocurrency of the Ethereum), sent in the transaction are denoted by msg.sender and msg.value, respectively. The contract contains require() and assert() annotations to specify properties stating that (i) for the deposit() function: the balance of a user after a deposit must be equal to the previous balance increased by the value specified in the transaction (line 8), (ii) for the withdraw() function: (a) in order to withdraw a specific amount from a balance, the specified value must be greater than zero and not greater than the balance of the user requesting the withdrawal (line 12), (b) the return of valid values from external calls is also checked (line 15). The VCs that are generated from this simple contract contain a significant number of CHCs (about 30), and are not easily readable.
An extract of a single CHC clause in Prolog format obtained after the CHC Generation and Prolog encoding phases is shown in Listing 2 (you can see the same clause in SMT-LIB format in the Appendix). In the clause shown in Listing 2, (i) 115...935 and 146...975 denote integers with 78 and 49 digits, respectively, corresponding to the maximum allowed value for a transaction and for an account address, and (ii) select and store are terms encoding read and write operations on the array associated with the balances variable, that maps addresses to the corresponding balances. Note also that clauses may contain redundant constraints, unnecessary variables and multiple occurrences of large constants. Figure 2 shows the PDG corresponding to the deposit() function of the example smart contract. There we can see how the two possible outcomes of a function call are handled: the case of failure, causing the transaction to revert, is identified by block_10_function_deposit while the case of success is identified by block_9_return_function_deposit.
The summary_4_function_deposit predicate is used to keep track of the relationship between the function’s input and output, derived from all its possible executions. This is linked to error_target_4 which occurs in the query false :- error_target_4 that is used to check the satisfiability of the CHCs.
The complete PDG for the Bank contract is shown in the appendix.
Some other tools focus on the visualization of smart contracts on the Ethereum platform, such as
Surya10, Solgraph11 and Solidity Auditor12 which generate Control Flow Graphs (CFG),
SmartGraph [
Ensuring the correctness of smart contracts poses a significant challenge, requiring auditors to employ supportive tools for efective verification. In addition to automated verification tools, CHC visualization tools can be a valuable aid in comprehending predicate dependencies, and increase the confidence in the correctness of the encoding of the considered property.
In this paper, we have presented a prototype tool aimed at visualizing the dependencies
among the CHCs derived from Solidity contracts. The tool can be extended and improved
along several directions. The CHC generation module can be extended to employ translation
schemes based on diferent operational semantics [
In Listing 3 a CHC clause in SMT-LIB format is shown. You can see the same clause in Prolog format in Listing 1. This is to highlight the diferences in verbosity and readability between the Prolog and SMT-LIB formats.
CHC clause extract in SMT-LIB format Listing 3. CHC clause extract: a clause in SMT-LIB format The complete PDG for the Bank contract is shown in Figure 3. Despite the modest complexity of the contract, it is surprising to observe the size of the generated graph. In addition, blocks relating to the initialisation of the contract and the implicit constructor are also included, adding further complexity and detail to the graphical representation.