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 behavior 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 88.46% on our benchmark dataset.