PaperlayerView exact revision on arXiv

Source-linked AI summary

SolBehave: Evaluating the Behavioural Correctness of LLM-Generated Smart Contracts

Giovanni Pio Delvecchio, Stefano Fantazzini, Giacomo Frisoni, Gianluca Moro, Lorenzo Bacchiani, Mario Bravetti, Thomas Troels Hildebrandt

arXiv:2610.18745v1cs.SEcs.AI

TL;DR

LLM-generated Solidity is commonly evaluated for compilation, although compiling code can still behave incorrectly and deployed contracts cannot be patched. SolBehave evaluates behavioural fidelity across 250 reproducibility-verified contracts using fuzzing, historical replay, and DCR-guided synthetic replay. For six of seven models, at least one compiling contract in eight diverges under each replay oracle.

  • Problem

    Compilation-based evaluation does not establish whether generated Solidity behaves as intended, despite deployed smart contracts being unpatchable.

    Source: §I · p. 2

  • Method

    SolBehave evaluates seven open-weight models on 250 reproducibility-verified contracts using differential fuzzing, historical replay, and DCR-guided synthetic replay.

    Source: §I · p. 2, §VII · p. 12

  • Results

    For six of seven models, at least one compiling contract in eight diverges from the original under each replay oracle.

    Source: §VII · p. 12

  • Takeaways & Limitations

    The replay oracles are complementary: DCR-guided sequences reach state-changing functions that historical transactions never called.

    Source: §VII · p. 12

    The benchmark covers Etherscan-verified, non-proxy contracts with 1–20 non-trivial functions and is dominated by token-like contracts; generalization to multi-step DeFi, bridges, or governance remains an open question.

    Source: §VI · p. 11

Abstract

from arXiv · show

Large language models increasingly generate Solidity smart contracts that, once deployed, can never be patched, making a single latent fault permanent and exploitable. Yet current evaluations mostly ask only whether generated code compiles. We introduce SolBehave, a benchmark for evaluating the correctness of model-generated contracts at scale, moving beyond ad hoc unit tests. Across 250 real, reproducible Ethereum contracts, we apply three complementary tests of behavioural fidelity: differential fuzzing, historical-transaction replay, and, as our core contribution, synthetic-transaction replay guided by a Dynamic Condition Response (DCR) graph that enumerates the space of legitimate function-call sequences. Differential fuzzing compares each generated function with the original on automatically generated inputs; historical replay compares the whole contract on the transactions it actually received on-chain; DCR-guided replay compares it on sequences of calls that follow its intended usage, including orderings that never occurred on-chain. We evaluate seven state-of-the-art open-weight models after one round of automated repair. Compilation success ranges from 26.4% to 92.7%, but under differential fuzzing only 31.4% of all generated function bodies that compile, pooled over models and samples, are equivalent to the original. Divergence at the contract level is the norm rather than the exception: for six of the seven models, between 13% and 31% of the generated contracts that compile diverge from the original under historical replay, and between 13% and 44% under DCR-guided replay; only Gemma-4-31B stays below 3% on both. Compilation is therefore a necessary condition for correctness and far from a sufficient one.

I. INTRODUCTION

SolBehave evaluates whether regenerated Solidity contracts behave like their originals, addressing the gap between compilation success and behavioural correctness. It combines function-level fuzzing and historical replay with DCR-guided sequences, which exercise intended call orderings that the other tests can miss.

I. INTRODUCTION

  • A latent fault in an immutable deployed contract can be permanent and exploitable, putting assets and users at risk.The paper notes that smart contracts increasingly govern real economic activity.Source: §I · pp. 1–2
  • Compilation success is necessary but insufficient: compiling Solidity can still contain semantic faults that change intended behaviour.The dominant evaluation paradigm measures whether generated code compiles, not whether it behaves as intended.Source: §I · p. 2
  • Historical replay tests recorded calls and differential fuzzing explores function inputs, but neither guarantees reaching states that require a particular sequence of calls.The Vault example’s missing balance check is exposed only after initialization followed by an over-withdrawal.Source: §I · p. 2
  • SolBehave adds DCR-guided synthetic replay, using a graph of lifecycle relations to generate legal call orderings and reach behaviours missed by historical traffic and function-level fuzzing.Its three fidelity oracles are differential fuzzing, historical transaction replay, and DCR-guided replay.Source: §I · p. 2
  • 31.4% of compiling regenerated function bodies are equivalent to the original under differential fuzzing, pooled over models and samples.For six of seven models, at least one regenerated contract in eight diverges under each replay oracle.Source: §I · p. 2

II. PRELIMINARIES

The preliminaries establish why contract executions can be replayed and what the behavioural oracles compare. They also introduce the Ethereum tools used to source, deploy, and test contracts.

II. PRELIMINARIES

  • A blockchain’s append-only history makes past transactions permanent and publicly visible, enabling replay of a contract’s past.Ethereum runs programs in the EVM, where computation is priced in gas.Source: §II · p. 3
  • A smart contract’s code and storage persist on-chain, and deterministic execution means the same call on the same storage has the same effects.Only state-changing functions alter storage; constructors run once at deployment, while view and pure functions are excluded from behavioural comparison.Source: §II · p. 3
  • Oracles compare outcomes such as success or revert, return values, emitted events, and resulting storage after a transaction call.A revert undoes storage changes, commonly when a check fails.Source: §II · p. 3
  • Etherscan supplies verified contract source and historical transactions, while Hardhat provides a local node for deployment and replay.The benchmark uses both services in its pipeline.Source: §II · p. 3
  • Echidna generates Solidity transactions guided by reached code and powers the differential-fuzzing oracle; Slither, Mythril, and Diffusc are related-work tools, not pipeline components.Slither analyzes source statically, Mythril explores executions symbolically, and Diffusc fuzzes two contract versions in parallel.Source: §II · p. 3

III. RELATED WORK

Prior evaluation approaches use static analysis, generated inputs, fixed tests, or historical transactions, each with limits on observing intended behaviour across call sequences. SolBehave instead uses sequences drawn from a description of legitimate contract use.

III. RELATED WORK

  • Existing generated-Solidity evaluations use static analysis, differential fuzzing, unit tests, or historical replay, but these inputs do not guarantee exercising calls that require specific preconditions.Historical replay is bounded by the contract’s transaction history, while random or fixed tests may miss ordered calls.Source: §III · p. 3
  • Tools for hand-written contracts test explicit developer properties, whereas generated contracts lack a corresponding list of properties describing intended behaviour.For generated code, divergence from intended behaviour can take many forms.Source: §III · p. 3
  • Sequence-aware fuzzers order calls to reach state-dependent branches, but they infer useful sequences from code or branch coverage rather than intended usage.IR-Fuzz uses state-variable reads and writes to infer order; MuFuzz mutates sequences that approach unexplored branches.Source: §III · pp. 3–4
  • SolBehave’s DCR graph supplies sequences the original contract accepts as legitimate uses, so behavioural differences can be assessed on intended call sequences.This differs from single-contract bug-finding fuzzers that seek broad code coverage.Source: §III · p. 4
  • The LLM extracts DCR relations as constraints for a graph-traversal component, and the paper uses DCR graphs proactively to generate transactions rather than to monitor executions against a hand-written specification.The authors identify this as the first use of DCR graphs for test-sequence generation in evaluating LLM-generated code.Source: §III · p. 4

IV. METHODOLOGY

The framework regenerates benchmark contracts and compares them with the original using a compilation filter and three behavioural oracles. Benchmark construction narrows verified mainnet contracts to a tractable set that reproduces its own recorded behaviour.

IV. METHODOLOGY

  • The framework regenerates each contract, then evaluates samples against the deployed original using Compile@k and three behavioural oracles.The oracles are differential fuzzing, historical transaction replay, and DCR-guided synthetic replay.Source: §IV · p. 4

A. Benchmark Construction

  • Benchmark construction crawls candidates that have verified source, are not proxies, and have at least 200 historical transactions.The crawl yields 8,360 candidates.Source: A. Benchmark Construction · p. 4
  • Candidates are deployed fresh and their first 200 historical transactions replayed; contracts reproducing less than 80% of recorded behaviour are discarded.This reproducibility check leaves 2,098 contracts.Source: A. Benchmark Construction · p. 4
  • The size filter retains contracts with 1–20 non-trivial functions, producing the final 250-contract benchmark from the reproducibility-verified set.The filter excludes constructors and view/pure functions; the figure shows the 1–20 band across the construction stages.Source: A. Benchmark Construction · p. 4, Figure 2 · p. 5

B. Code Generation

The evaluation regenerates contracts from common skeletons, then tests behavioural fidelity with function-level fuzzing and two replay oracles. DCR-guided replay uses a permissive model of intended call order, with state-dependent guards, to reach sequences historical traffic may not cover.

B. Code Generation

  • Each contract is regenerated ten times from the same skeleton, with function bodies completed one at a time in source order and later functions conditioned on earlier generated code.Samples share signatures but differ in function bodies; compilation success is reported as Compile@k.Source: B. Code Generation · p. 5

C. O1: Differential Fuzzing

  • O1 fuzzes each state-changing function with primitive arguments against original and regenerated contracts, checking call status and successful return data without interleaving different functions.Echidna searches for assertion violations; the harness deploys both contracts and can exercise owner-only functions.Source: C. O1: Differential Fuzzing · p. 5

D. O2: Historical Transaction Replay

  • O2 replays each contract’s first 1,000 recorded mainnet transactions, in original order, against fresh deployments of the original and regenerated contracts.Real-user arguments and call order are not synthesized.Source: D. O2: Historical Transaction Replay · p. 5

E. O3: DCR-Guided Synthetic Transaction Replay

  • O3 synthesizes sequences from an explicit model of intended call structure to reach orderings and preconditions that historical records may not cover.The DCR graph is deliberately permissive, leaving unconstrained event orderings free while representing state-changing function branches as events.Source: E. O3: DCR-Guided Synthetic… · p. 5, 1) The DCR formalism · p. 5

1) The DCR formalism:

  • DCR relations encode conditions, responses, inclusion, and exclusion; this method adds Solidity-state guards so relations apply only while their expressions hold.An event that may occur only once is represented as a self-exclusion and recorded as an event flag.Source: 1) The DCR formalism · pp. 5–6

2) Validated Sequence Generation:

Validated sequence generation traverses a DCR graph against the original deployed contract, using live state to select allowed calls and retaining only calls the original accepts. Ownership-transferring events are postponed so they do not cut off later owner calls.

2) Validated Sequence Generation:

  • The generator builds ordered call sequences from a DCR graph and original deployment, checking calls on a local node and restarting from a fresh deployment when no event can be executed.Each sequence begins with the graph’s initial marking and grows one call at a time until the successful-call budget is reached.Source: 2) Validated Sequence Generation · pp. 6–7
  • Before each step, the procedure reads guarded state variables through contract getters and evaluates guards on their actual current values.Only events whose guards hold remain candidates for selection.Source: 2) Validated Sequence Generation · p. 7
  • Selection prioritizes pending obligations, then prerequisites, before using an exploration rule that favors untried events and balances success rates with rare attempts.Obligation and prerequisite priorities are applied probabilistically, at β=0.7 and α=0.8, to retain exploration.Source: 2) Validated Sequence Generation · p. 7
  • Ownership-transferring events are held until the sequence ends because executing them earlier would make later calls from the original owner fail.Such events average 0.52 per contract versus 6.0 total events per contract in graphs extracted by GEMMA-4-31B; 71.6% of contracts have none.Source: 2) Validated Sequence Generation · p. 7
  • A selected call is retained only if the original contract accepts it; reverted calls are discarded without updating the graph marking.Across 250 contracts, 212,904 of 256,923 attempted calls were kept and 17.1% were discarded as reverts.Source: 2) Validated Sequence Generation · p. 7
  • For 32 contracts, more than 98% of calls were discarded, leaving no sequence for 32 contracts because extracted arguments could not satisfy guards and were not searched anew.The median discard rate was 4.9%; pairing DCR orderings with argument fuzzing is identified as future work.Source: 2) Validated Sequence Generation · p. 7

F. Comparison Axes

The replay oracles compare the original and regenerated contracts call by call, primarily by success-or-revert status. They also record receipt and exposed-state observations, while sequence availability determines which contracts O3 can evaluate.

F. Comparison Axes

  • All three oracles treat a call as matching when it succeeds on both deployments or reverts on both; O1 additionally compares returned values on successful calls.O2 and O3 compare transaction receipts, since user accounts do not receive return values.Source: F. Comparison Axes · p. 7
  • A contract is divergent under an oracle if any sample disagrees with the original on status for at least one call.Status match rate is the fraction of calls agreeing on status.Source: F. Comparison Axes · p. 7
  • Replay records gas, event emissions, and periodic view-function snapshots as secondary observations, but none exposed a divergence that status had not.Gas deviations are flagged only beyond ±10%.Source: F. Comparison Axes · p. 7
  • O2 requires at least one compiling sample, while O3 also requires a validated sequence, available for 218 of the 250 contracts.The reported divergence denominators are the numbers of contracts actually compared for each oracle and model.Source: F. Comparison Axes · p. 7

V. EVALUATION

The evaluation applies the framework to 250 contracts regenerated by seven open-weight models from five model families. A common repair protocol and fixed oracle budgets govern behavioural evaluation of compiling samples.

V. EVALUATION

  • The evaluation uses seven open-weight models from five families on a 250-contract benchmark, with each model regenerating contracts in ten samples and extracting DCR graphs.Models run as 4-bit GGUF quantisations on a single RTX 5090 with temperature 0.7 and up to 2,048 output tokens per function.Source: §V · p. 7, A. Experimental Setup · p. 8

A. Experimental Setup

  • Non-compiling samples receive one repair attempt from their generating model, and samples still failing compilation are excluded from behavioural evaluation.The model receives the sample and compiler error and is instructed to fix only the reported error.Source: A. Experimental Setup · p. 8
  • Each compiling sample is tested with O1, while O2 and O3 use budgets of 1,000 transactions per contract; O3 can use either the tested model’s graph or a reference extractor’s graph.Runs use seed 42; O2 uses the first recorded transactions and O3 uses successful calls collected by sequence generation.Source: A. Experimental Setup · p. 8

B. Compilation Separates Models but Does Not Certify Them

Compilation separates the models but does not certify behavioural correctness. Human validation finds generally reliable DCR relations with specific over-constraining errors, while historical and DCR-guided replay flag different divergences.

B. Compilation Separates Models but Does Not Certify Them

  • After one repair pass, Compile@10 remains widely separated at 26.4%–92.7%, and repair preserves the model ranking.Repair lifts every model by 3.6–10.8 percentage points; the relative gain ranges from +40% for DEVSTRAL-24B to +4% for GEMMA-4-31B.Source: B. Compilation Separates Models but… · p. 8

C. Extracted DCR Graphs Are Reliable

  • Across 200 judged relations, DCR extraction reaches 0.72 precision and 0.88 recall, while inclusion and exclusion errors add relations and over-constrain graphs.Condition has 0.96 precision; the permissive DCR semantics and on-chain guard evaluation absorb part of the over-constraint.Source: C. Extracted DCR Graphs Are Reliable · p. 8

D. The Two Replay Oracles Are Complementary

  • O3 flags contracts O2 certifies as correct for every model; conversely, O2-only flags occur for every model except GEMMA-4-31B. For QWEN3.6-27B, O3 flags 20 contracts, including 7 not flagged by O2, while O2 flags 16 alone.The oracles’ status match rates order models almost identically (Spearman ρ=0.86). With fixed reference graphs, O3-only flags remain non-zero for every model.Source: D. The Two Replay Oracles Are… · p. 9
  • O3 evaluates fewer contracts than O2 because it also requires a validated sequence: 85–174 versus 122–234, depending on the model’s compiling samples.On reference-extractor runs, O2 took 19.8 s per contract over 234 contracts and O3 took 22.1 s over 174; graph extraction is amortized across models.Source: D. The Two Replay Oracles Are… · p. 9

E. Coverage Explains the Complementarity

O2 and O3 reach different state-changing functions: O3 adds functions absent from historical traffic, while O2 covers functions O3 misses. Their relative coverage varies across contracts, and graph-extraction skill differs from Solidity-generation skill.

E. Coverage Explains the Complementarity

  • O2 covers 55.7% of state-changing functions on average, while O3 covers 33.6%–47.3% depending on extractor; each oracle reaches functions the other misses.O3 reaches 246–311 functions no historical transaction called, while O2 reaches 511–619 that O3 misses; better extraction shrinks only the latter set.Source: E. Coverage Explains the Complementarity · p. 9
  • With GEMMA-4-31B graphs, O3 covers more functions on 84 contracts, fewer on 121, and the same on 45; the median favours O3, 57.1% to 50.0%.O3 tends to win where preconditions gate functions users never called; O2 tends to win on wide, heavily used interfaces that dominate the mean.Source: E. Coverage Explains the Complementarity · p. 9
  • DEVSTRAL-24B ranks last in Compile@10 at 26.4% but third in O3 graph coverage at 44.2%, showing that Solidity generation and DCR extraction rank differently.Only GEMMA-4-31B ranks first on both tasks.Source: E. Coverage Explains the Complementarity · p. 9

F. Differential Fuzzing Finds Few Equivalent Functions

Differential fuzzing finds that compiling functions rarely preserve the original behavior, while comparison with replay oracles shows both O1’s broad signal and its inability to compose sequences. The section also bounds these findings by the benchmark’s scope and evaluation choices.

F. Differential Fuzzing Finds Few Equivalent Functions

  • 31.4% of compiling regenerated function bodies are equivalent overall, and only 34% of contracts have a sample in which every fuzzable function is equivalent.The 31.4% figure averages across fuzzable contract-function pairs and models.Source: F. Differential Fuzzing Finds Few… · p. 10
  • 2.0%–35.5% is the range of model function-equivalence rates, from DEVSTRAL-24B to QWEN3.6-27B; QWEN3.6-27B’s 35.5% exceeds GEMMA-4-31B’s 33.4% despite lower compilation, 71.3% versus 92.7%.Five of seven models retain their Compile@10 ranking; the top two swap.Source: F. Differential Fuzzing Finds Few… · p. 10
  • 38%–69% of each model’s divergent contracts are flagged by O1 alone, and only one contract across all models is flagged by a replay oracle but not O1.O1’s larger per-function call budget makes it stronger within the shared evaluation set, but it cannot compose sequences; O2 and O3 capture realistic-use divergences and are complementary to each other.Source: F. Differential Fuzzing Finds Few… · p. 10

VI. THREATS TO VALIDITY

  • O3’s graph extraction can miss valid sequences or block them, but permissive DCR semantics and deployed-contract guard checks constrain these errors to lost coverage rather than false acceptance.Replacing model-extracted graphs with a fixed extractor changes O3’s flagged-contract count by at most two per model; human validation uses a single annotator.Source: §VI · pp. 10–11
  • Reported divergence counts are lower bounds because status-only comparison misses differences in revert reasons or return values, and O3 replays only calls accepted by the original.A regenerated contract that fixes a fault in the original is also counted as divergent, since the original is the sole specification and reference reproducibility does not establish reference correctness.Source: §VI · pp. 11–12
  • The benchmark covers verified, non-proxy contracts with 1–20 non-trivial functions and is token-dominated; oracle complementarity on multi-step DeFi, bridges, and governance remains open.The 20-function boundary reflects falling compile rates and rising generation costs for larger contracts, where models also become less distinguishable.Source: §VI · p. 11, Table VII · p. 11
  • Fresh deployments begin at constructor state, so faults that arise only after accumulated mainnet activity can escape, although initialization and access-control faults are detected reliably.All models use identical 4-bit quantisation, temperature, and k=10 samples; selection probabilities were not varied.Source: §VI · p. 11
  • The evaluation measures equivalence on exercised transactions, not functional correctness; self-repair leaves model rankings unchanged but does not broaden that construct.A regenerated contract that fixes an original fault is scored as divergent.Source: §VI · p. 11

VII. CONCLUSION

SolBehave evaluates generated contracts against their originals using differential fuzzing and historical and DCR-guided replay. Across seven open-weight models, compilation is a poor correctness proxy, and the replay oracles reveal complementary divergences.

VII. CONCLUSION

  • SolBehave evaluates seven open-weight models on 250 reproducibility-verified mainnet contracts using differential fuzzing, historical replay, and synthetic replay guided by a DCR graph.The synthetic sequences represent the contract’s intended lifecycle.Source: §VII · p. 12
  • Only 31.4% of compiling regenerated functions are equivalent, and six of seven models have compiling contracts that diverge under both replay oracles.Compile rates range from 26.4% to 92.7%. DCR-guided replay also reaches state-changing functions that historical transactions never called.Source: §VII · p. 12
  • The authors propose expanding validation and the benchmark to more annotators and complex contract domains, and pairing DCR replay with argument fuzzing and negative testing.The proposed domains include DeFi protocols, bridges, and governance systems.Source: §VII · p. 12
Loading 2610.18745v1…