Automating Invariant Generation for Smart Contracts with Large Language Models: An Empirical Evaluation

15/05/2025

Smart contracts are critical components of blockchain systems, but ensuring their security and correctness is challenging due to their immutable and autonomous nature. Property-based fuzzing tools like Echidna rely on user-defined invariants to uncover bugs, yet writing such invariants is a manual and expertise-intensive bottleneck. This thesis investigates whether Large Language Models (LLMs) can automate invariant generation for smart contracts. We present an end-to-end workflow that analyzes contracts, prompts LLMs to generate candidate invariants, filters and injects them, and validates them using Echidna fuzzing. The approach is evaluated on 116 vulnerable Ethereum contracts using five different LLMs. Results indicate that while LLMs can produce some syntactically valid invariants, most are trivial, invalid, or too complex for practical fuzzing, with only a small fraction passing validation. These findings highlight both the potential and current limitations of LLM-driven automation for smart contract verification. This work demonstrates the feasibility of integrating LLMs into the invariant generation workflow, provides empirical insights into their effectiveness, and outlines directions for improving automated smart contract analysis.

Autores da comunidade :

• 

  J

  João Edgar Alves Esteves

  ist196876

Orientadores desta instituição:

• 

  J

  João Fernando Peixoto Ferreira

  ist428178

electrical-engineering-electronic-engineering-information-engineering - Engenharia Eletrotécnica, Eletrónica e Informática

eng - Inglês

Instituto Superior Técnico