一句话：结合形式化方法与LLM，自动生成并验证智能合约漏洞的复现合约与攻击轨迹。
智能合约漏洞复现需构造攻击者合约与特定交互序列，但现有形式化验证工具虽能检测漏洞，却往往不提供执行轨迹或轨迹不完整，也难反映攻击者合约的行为模式。为此，VeriExploit 结合形式化方法与大型语言模型，以易受攻击的合约及其反例为输入，自动生成、验证并精化复现合约与执行步骤，最终输出能重新触发同一漏洞的合约和具体利用轨迹。实验表明，该框架能有效自动化漏洞复现，在自建基准数据集上成功率达 85.60%。
Bug reproduction is becoming an important task in the security analysis of Solidity smart contracts. By simulating attacks, developers and auditors can better understand how a vulnerability is triggered in practice. To reproduce a bug, one often needs to define an attacker contract and a specific sequence of interactions that exploit the vulnerability. However, in smart contracts, there are rarely automated tools that can generate such contracts and sequences and validate their correctness. Existing security tools, such as formal verifiers, are effective at detecting bugs, but they are not designed for bug reproduction. They often omit execution traces or produce incomplete ones. Moreover, their reports rarely reflect the behaviour patterns of attacker contracts. This gap motivates our work. We propose VeriExploit, a framework that combines formal methods and large language models to automatically generate, validate, and refine reproduction contracts and execution steps. Given a vulnerable contract and its counterexample, VeriExploit produces a contract that re-triggers the same bug and outputs a concrete trace showing how the exploit works. Experiments show that VeriExploit is effective at automating bug reproduction, achieving a success rate of 85.60% on our benchmark dataset.
@inproceedings{paperbot9568,
title = {VeriExploit: Automatic Bug Reproduction in Smart Contracts via LLMs and Formal Methods},
author = {Chenfeng Wei and Shiyu Cai and Yiannis Charalambous and Tong Wu and Sangharatna Godboley and Lucas Cordeiro},
booktitle = {ASE},
year = {2025},
doi = {10.1109/ase63991.2025.00120}
}