Don't Just Translate: Verify - LLM-Guided Solidity Migration with Semantic Guarantees
This paper presents a closed-loop framework for semantics-preserving smart contract migration that combines LLM-based code generation with formal verification and performs migration iteratively through compilation, bytecode-level equivalence checking, counterex-ample generation, and refinement.