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

05/15/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.

Authors in the community:

• 

  J

  João Edgar Alves Esteves

  ist196876

Supervisors of this institution:

• 

  J

  João Fernando Peixoto Ferreira

  ist428178

electrical-engineering-electronic-engineering-information-engineering - Electrical engineering, electronic engineering, information engineering

eng - English

Instituto Superior Técnico