Don't Just Translate: Verify - LLM-Guided Solidity Migration with Semantic Guarantees

Abstract

: Smart contracts operate in immutable blockchain environments where preserving correctness during software evolution is critical. The transition from Solidity 0.5.x to 0.8.x introduces important safety improvements but also semantic changes that make manual migration of legacy contracts error-prone. Although large language models (LLMs) can automatically translate code across versions, they offer no guarantee that the generated contracts preserve the original behavior. This paper presents a closed-loop framework for semantics-preserving smart contract migration that combines LLM-based code generation with formal verification. Our approach performs migration iteratively through compilation, bytecode-level equivalence checking, counterex-ample generation, and refinement. Behavioral equivalence is verified using differential fuzzing and symbolic execution over Ethereum Virtual Machine semantics, and detected discrepancies are fed back to guide improved LLM outputs.