Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

FLAMES: Fine-tuning LLMs to Synthesize Invariants for Smart Contract Security

Mojtaba Eshghie, Gabriele Morello, Matteo Lauretano, Alexandre Bartel, Martin Monperrus

TL;DR

FLAMES tackles the problem of hardening smart contracts by automatically synthesizing executable invariants as Solidity require statements using domain-adapted LLMs. The pipeline comprises code analysis, supervised fine-tuning on a large-scale invariant dataset (DISL), and invariant synthesis at pre- or post-conditions during inference, all without vulnerability labels or natural-language specifications. Empirical results show high compilability ($96.7\%$) and substantial semantic alignment to human-written invariants ($44.5\%$ exact/equivalent), along with measurable exploit mitigation (up to $22/108$ cases, $20.4\%$) and a successful real-incident hardening of the APEMAGA attack. The work also contributes a vast, deduplicated Solidity dataset and evaluation harnesses, enabling reproducible research in automated defensive hardening for smart contracts and suggesting a path toward production-ready automated defenses. FLAMES demonstrates that specialized, fine-tuned LLMs can autonomously generate practical, deployable security defenses for smart contracts, reducing reliance on vulnerability labels or formal specifications.

Abstract

Smart contract vulnerabilities cost billions of dollars annually, yet existing automated analysis tools fail to generate deployable defenses. We present FLAMES, a novel automated approach that synthesizes executable runtime guards as Solidity "require" statements to harden smart contracts against exploits. Unlike prior work that relies on vulnerability labels, symbolic analysis, or natural language specifications, FLAMES employs domain-adapted large language models trained through fill-in-the-middle supervised fine-tuning on real-world invariants extracted from 514,506 verified contracts. Our extensive evaluation across three dimensions demonstrates FLAMES's effectiveness: (1) Compilation: FLAMES achieves 96.7% compilability for synthesized invariant (2) Semantic Quality: on a curated test set of 5,000 challenging invariants, FLAMES produces exact or semantically equivalent matches to ground truth in 44.5% of cases; (3) Exploit Mitigation: FLAMES prevents 22 out of 108 real exploits (20.4%) while preserving contract functionality, and (4) FLAMES successfully blocks the real-world APEMAGA incident by synthesizing a pre-condition that mitigates the attack. FLAMES establishes that domain-adapted LLMs can automatically generate production-ready security defenses for smart contracts without requiring vulnerability detection, formal specifications, or human intervention. We release our code, model weights, datasets, and evaluation infrastructure to enable reproducible research in this critical domain.

FLAMES: Fine-tuning LLMs to Synthesize Invariants for Smart Contract Security

TL;DR

FLAMES tackles the problem of hardening smart contracts by automatically synthesizing executable invariants as Solidity require statements using domain-adapted LLMs. The pipeline comprises code analysis, supervised fine-tuning on a large-scale invariant dataset (DISL), and invariant synthesis at pre- or post-conditions during inference, all without vulnerability labels or natural-language specifications. Empirical results show high compilability () and substantial semantic alignment to human-written invariants ( exact/equivalent), along with measurable exploit mitigation (up to cases, ) and a successful real-incident hardening of the APEMAGA attack. The work also contributes a vast, deduplicated Solidity dataset and evaluation harnesses, enabling reproducible research in automated defensive hardening for smart contracts and suggesting a path toward production-ready automated defenses. FLAMES demonstrates that specialized, fine-tuned LLMs can autonomously generate practical, deployable security defenses for smart contracts, reducing reliance on vulnerability labels or formal specifications.

Abstract

Smart contract vulnerabilities cost billions of dollars annually, yet existing automated analysis tools fail to generate deployable defenses. We present FLAMES, a novel automated approach that synthesizes executable runtime guards as Solidity "require" statements to harden smart contracts against exploits. Unlike prior work that relies on vulnerability labels, symbolic analysis, or natural language specifications, FLAMES employs domain-adapted large language models trained through fill-in-the-middle supervised fine-tuning on real-world invariants extracted from 514,506 verified contracts. Our extensive evaluation across three dimensions demonstrates FLAMES's effectiveness: (1) Compilation: FLAMES achieves 96.7% compilability for synthesized invariant (2) Semantic Quality: on a curated test set of 5,000 challenging invariants, FLAMES produces exact or semantically equivalent matches to ground truth in 44.5% of cases; (3) Exploit Mitigation: FLAMES prevents 22 out of 108 real exploits (20.4%) while preserving contract functionality, and (4) FLAMES successfully blocks the real-world APEMAGA incident by synthesizing a pre-condition that mitigates the attack. FLAMES establishes that domain-adapted LLMs can automatically generate production-ready security defenses for smart contracts without requiring vulnerability detection, formal specifications, or human intervention. We release our code, model weights, datasets, and evaluation infrastructure to enable reproducible research in this critical domain.
Paper Structure (33 sections, 10 figures, 4 tables)

This paper contains 33 sections, 10 figures, 4 tables.

Table of Contents

  1. Introduction
  2. Flames Architecture
  3. Overview
  4. Code Analysis Stage
  5. Supervised Fine-Tuning Stage
  6. Invariant Synthesis Stage
  7. Invariant Synthesis Locations
  8. Inference Strategies
  9. Implementation
  10. DISL: Fine-Tuning Dataset
  11. Data Collection
  12. Initial Seeding and Expansion
  13. Source Code Retrieval
  14. Experimental Evaluation
  15. Datasets Used for Experiments
  16. ...and 18 more sections

Figures (10)

  • Figure 1: Flames architecture, evaluation, and results overview.
  • Figure 2: The supervised fine-tuning pipeline yields to Flames models, specialized for Solidity.
  • Figure 3: Preventing the BeautyChain attack with a pre-condition invariant.
  • Figure 4: Flames synthesis stage illustrated with an example.
  • Figure 5: Cumulative distribution of the token length of Disl contracts.
  • ...and 5 more figures