Towards Trustworthy Smart Contract Synthesis: A Multi-Agent Framework with Lean-Based Verification

Smart Contracts are the foundation of Decentralized Finance (DeFi), executing financial logic without trusted intermediaries. Recent advances in large language models (LLMs) have substantially lowered the barrier to smart contract development by enabling code generation from natural language. However, because smart contracts are immutable and directly manage financial assets, this accessibility introduces a critical trust gap: generated contracts are easy to produce but hard to trust. To bridge this gap, We present LeVer, the first trustworthy smart contract synthesis framework that integrates LLM-based generation with Lean-based autoformalization and Verification. LeVer employs a closed-loop multi-agent architecture to iteratively generate, verify, attack, and repair contracts, providing both formal guarantees and empirical robustness. To facilitate the adoption of automated formal verification in smart contract generation and audition, we opensource our framework and datasets at: https: //github.com/gl-bowei/LeVer