Formal verification of smart contracts using Constrained Horn Clauses

Abstract

The growing popularity of smart contracts on blockchain platforms in recent years has made the development of reliable verification techniques that ensure code is both logically correct and secure an urgent priority. One of the most effective methods adopted by existing tools is formal verification. This thesis addresses the problem of smart contract verification, particularly focusing on those developed for the Ethereum platform. It concentrates on using Constrained Horn Clauses (CHCs) as an intermediate formalism for representing and analysing program properties. Various verification tools were analysed and compared during the course of the work, particularly those based on CHCs, to identify practical limitations, methodological gaps, and opportunities for improvement. Based on this analysis, new tools and optimisations were designed and developed. On the one hand, we implemented CHCViz, a visualisation system that assists auditors and developers in inspecting and understanding CHCs generated by existing tools, such as SolCMC. On the other hand, a verifier for Yul code was built from scratch to extend the applicability of formal verification via CHCs to the recently released intermediate code from the Ethereum foundation.