Elamur Research⌕
☰
home / papers / 2026 / Towards Trustworthy Smart Contract Synthesis: A Multi-Agent Framework with Lean-Based Verification

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

Paper · 2026 · Bowei Zhang, Hanbing Liu, Qixin Tian et al.

Summary

LLMs make it easy to produce Solidity smart contracts from natural-language requests. But deployed contracts cannot be changed and they hold real funds, so a hidden bug can cause permanent losses. The authors call this the "trust gap." Existing safeguards each fall short. Static analyzers raise many false alarms. Manual audits are expensive and do not scale. LLM-based auditors give informal, non-deterministic feedback.

The paper presents LeVer, a closed-loop system with three agents:

  • a Coder that writes and repairs contracts;
  • a Verifier that extracts security invariants, auto-formalizes the Solidity logic into Lean 4 and builds machine-checked proofs;
  • an Attacker that searches for adversarial transaction sequences, targeting properties that are hard to prove.

An Attack-to-Property mechanism converts each discovered exploit into a new theorem, so the system keeps protecting against that threat in later iterations.

On a large-scale benchmark, LeVer brings the attack success rate down to 2.4% and outperforms strong baselines. The work is a proof-of-concept for using LLMs in financial settings that tolerate no errors. It also shows that combining formal proofs with adversarial testing is practical.

Key points

  • Ablations show both checkers are needed:
    • Removing the Verifier raises the attack rate (AR) from 2.4% to 10.0% and lowers the verification rate (VR) from 74.1% to 68.4%.
    • Removing the Attacker raises VR to 81.5% but sends AR to 23.3%, close to baseline. Without new hard properties from attacks, the Verifier only proves easy theorems.
  • Faithfulness of the Solidity-to-Lean translation: on 300 randomly sampled tasks, 96.7% passed expert review and 97.4% passed an execution cross-check. The authors stress that this is empirical evidence, not a formal proof of equivalence.
  • Contract model: contracts are treated as deterministic state machines with persistent state Σ, execution context Γ and transition function Υ. A failed check causes an atomic revert.
  • Limitations:
    • No modeling of cross-contract composability, such as flash loans.
    • No support for randomness-based logic, such as lotteries.
    • Valid theorems sometimes go unproven because proofs are generated in full rather than through step-wise tactic interaction.
  • Availability: code and datasets are open-sourced at github.com/gl-bowei/LeVer.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓Renmin University of ChinaBeijing · China139 works · 17,752 citations

 Fields, topics and concepts

📚 Shelves 4The field of science this work belongs to (OpenAlex fields).Computer Science · 18,614 worksArtificial Intelligence · 17,965 worksInformation Systems · 1,730 worksComputational Theory and Mathematics · 321 works

Cite

Cite as Bowei Zhang, Hanbing Liu, Qixin Tian, Siyu Chen, Ziyuan Wang and Qi Qi. 2026. Towards Trustworthy Smart Contract Synthesis: A Multi-Agent Framework with Lean-Based Verification. Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers).

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.18653/v1/2026.acl-long.1836

@inproceedings{zhang2026trustworthy,
  title = {{Towards Trustworthy Smart Contract Synthesis: A Multi-Agent Framework with Lean-Based Verification}},
  author = {Bowei Zhang, Hanbing Liu, Qixin Tian, Siyu Chen, Ziyuan Wang and Qi Qi},
  booktitle = {Proceedings of the 64th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers)},
  year = {2026},
  doi = {10.18653/v1/2026.acl-long.1836},
  url = {https://doi.org/10.18653/v1/2026.acl-long.1836}
}

References

37 references, 3 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Danil Annenkov, Jakob Botsch Nielsen, and Bas Spit-ters. 2020. Concert: a smart contract certification framework in coq. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pages 215–228. find
  2. Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Anitha Gollamudi, Georges Gonthier, Nadim Kobeissi, Natalia Kulatova, Aseem Rastogi, Thomas Sibut-Pinote, Nikhil Swamy, and Santiago Zanella-Béguelin. 2016. Formal verification of smart contracts. In Proceedings of the 2016 ACM Workshop… find
  3. Fran Casino, Thomas K. Dasaklis, and Constantinos Patsakis. 2019. A systematic literature review of blockchain-based applications: Current status, classification and open issues. Telematics and Informatics, 36:55–81. find
  4. Siddhartha Chatterjee and Bina Ramamurthy. 2024. Efficacy of various large language models in generating smart contracts. arXiv preprint arXiv:2407.11019. — [arXiv:2407.11019](https://arxiv.org/abs/2407.11019) find
  5. Alessandro Cimatti, Edmund Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, and Armando Tacchella. 2000. NuSMV: A new symbolic model checker. International Journal on Software Tools for Technology Transfer (STTT), 2(4):410–425. find
  6. Edmund M. Clarke, Jeannette M. Wing, Rajeev Alur, Rance Cleaveland, David Dill, E. Allen Emerson, Stephen Garland, Steven German, John Guttag, Anthony Hall, Thomas A. Henzinger, Gerard J. Holzmann, Cliff B. Jones, Robert P. Kurshan, Nancy G. Leveson, Kenneth L. McMillan, J. Strother Moore, Doron A.… find
  7. Isaac David, Liyi Zhou, Kaihua Qin, Dawn Song, Lorenzo Cavallaro, and Arthur Gervais. 2023. Do you still need a manual smart contract audit? arXiv preprint arXiv:2306.12338. Discusses the high time and cost demands of traditional manual smart contract auditing and motivates automated approaches. find
  8. DeepSeek-AI. 2025. DeepSeek-V3.2: Pushing the frontier of open large language models. arXiv preprint arXiv:2512.02556.
  9. Josselin Feist, Gustavo Grieco, and Alex Groce. 2019. Slither: a static analysis framework for smart contracts. In 2019 IEEE/ACM 2nd International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB), pages 8–15. IEEE. find
  10. Asem Ghaleb and Karthik Pattabiraman. 2020. How effective are smart contract analysis tools? evaluating smart contract static analysis tools using bug injection. In Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA), pages 1–13. Empirical evaluation… find
  11. Google DeepMind. 2025. Gemini 3 Pro Model Card. Model card. find
  12. Jingxuan He, Mislav Balunovic, Nodar Ambroladze, Petar Tsankov, and Martin Vechev. 2019. Learning to fuzz from symbolic execution with application to smart contracts. In Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, pages 531–548. find
  13. Everett Hildenbrandt, Manasvi Saxena, Nishant Rodrigues, Xiaoran Zhu, Philip Daian, Dwight Guth, Brandon M. Moore, Daejun Park, Yi Zhang, Andrei Stefanescu, and Grigore Rosu. 2018. KEVM: A complete formal semantics of the ethereum virtual machine. In 2018 IEEE 31st Computer Security Foundations Symp… find
  14. Peter Ince, Jiangshan Yu, Joseph K. Liu, and Xiaoning Du. 2025. Generative large language model usage in smart contract vulnerability detection. arXiv preprint arXiv:2504.04685. — [arXiv:2504.04685](https://arxiv.org/abs/2504.04685) find
  15. Bo Jiang, Ye Liu, and WK Chan. 2018. Contract-Fuzzer: Fuzzing smart contracts for vulnerability detection. In Proceedings of the 33rd IEEE/ACM International Conference on Automated Software Engineering, pages 259–269. find
  16. Dongwei Jiang, Marcio Fonseca, and Shay B. Cohen. 2024. Leanreasoner: Boosting complex logical reasoning with lean. In Proceedings of the 2024 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies. find
  17. Erya Jiang, Bo Qin, Qin Wang, Zhipeng Wang, Qian-hong Wu, Jian Weng, Xinyu Li, Chenyang Wang, Yuhang Ding, and Yanran Zhang. 2023. Decentralized finance (defi): A survey. arXiv preprint arXiv:2308.05282. Comprehensive survey of DeFi applications, risks, and future research directions. — [arXiv:2308.05282](https://arxiv.org/abs/2308.05282) find
  18. Shafaq Naheed Khan, Faiza Loukil, Chirine Ghedira-Guegan, Elhadj Benkhelifa, and Anoud Bani-Hani. 2021. Blockchain smart contracts: Applications, challenges, and future trends. Peer-to-Peer Networking and Applications, 14:2901–2925. find
  19. Ye Liu, Yue Xue, Daoyuan Wu, Yuqiang Sun, Yi Li, Miaolei Shi, and Yang Liu. 2024. Propertygpt: Llm-driven formal verification of smart contracts through retrieval-augmented property generation. arXiv preprint arXiv:2405.02580. — [arXiv:2405.02580](https://arxiv.org/abs/2405.02580) find
  20. Hao Luo, Yuhao Lin, Xiao Yan, Xintong Hu, Yuxiang Wang, Qiming Zeng, Hao Wang, and Jiawei Jiang. 2025. Guiding llm-based smart contract generation with finite state machine. In Proceedings of the Thirty-Fourth International Joint Conference on Artificial Intelligence, pages 5869–5877. find
  21. Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, and Aquinas Hobor. 2016. Making smart contracts smarter. In Proceedings of the 2016 ACM SIGSAC conference on computer and communications security, pages 254–269. find
  22. Wei Ma, Daoyuan Wu, Yuqiang Sun, Tianwen Wang, Shangqing Liu, Jian Zhang, Yue Xue, and Yang Liu. 2025. Combining fine-tuning and llm-based agents for intuitive smart contract auditing with justifications. In Proceedings of the IEEE/ACM 47th International Conference on Software Engineering (ICSE 2025… find
  23. Leonardo de Moura and Sebastian Ullrich. 2021. The lean 4 theorem prover and programming language. In International Conference on Automated Deduction, pages 625–635. Springer.
  24. Bernhard Mueller. 2018. Mythril: Security analysis tool for Ethereum smart contracts. In Black Hat USA. GitHub repository. find
  25. Ivica Nikolic, Aashish Kolluri, Ilya Sergey, Prateek Saxena, and Aquinas Hobor. 2018. Finding the greedy, prodigal, and suicidal contracts at scale. In Proceedings of the ACM Conference on Computer and Communications Security (CCS), pages 653–667. Demonstrates real-world smart contract vulnerabiliti… find
  26. Paradigm. 2021. Foundry: A blazing fast, portable and modular toolkit for ethereum application development. https://github.com/foundry-rs/ foundry. ↗
  27. Jan Peleska. 2019. Formal methods: A roadmap for industrial adoption. ACM Computing Surveys, 52(4):1–30. Discusses the challenges of traditional formal methods, including reliance on proof assistants like Coq/Isabelle and the scarcity of expertise among practitioners. find
  28. Qwen Team. 2025. Qwen3-Max-Instruct. Official blog post. find
  29. Palina Tolmach, Yi Li, Shang-Wei Lin, and Yang Liu. 2021. Formal analysis of composable defi protocols. In International Conference on Financial Cryptography and Data Security, pages 149–161. Springer. find
  30. Petar Tsankov, Andrei Dan, Dana Drachsler-Cohen, Arthur Gervais, Florian Bünzli, and Martin Vechev. 2018. Securify: Practical analysis of smart contracts. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, pages 67–82. find
  31. Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi, and Tong Zhang. 2024a. Theoremllama: Transforming general-purpose llms into lean4 experts. arXiv preprint arXiv:2407.03203. find
  32. Sally Junsong Wang, Kexin Pei, and Junfeng Yang. 2024b. Smartinv: Multimodal learning for smart contract invariant inference. In 2024 IEEE Symposium on Security and Privacy (SP), pages 2217–2235. IEEE. find
  33. Zhiyuan Wei, Jing Sun, Zijiang Zhang, Xianhao Zhang, Meng Li, and Zhe Hou. 2024. Llm-smartaudit: Advanced smart contract vulnerability detection. arXiv preprint arXiv:2410.09381. — [arXiv:2410.09381](https://arxiv.org/abs/2410.09381) find
  34. Lei Yu, Jingyuan Zhang, Xin Wang, Jiajia Ma, Li Yang, and Fengjun Zhang. 2025. SmartCoder-R1: Towards secure and explainable smart contract generation with security-aware group relative policy optimization. arXiv preprint arXiv:2509.09942. — [arXiv:2509.09942](https://arxiv.org/abs/2509.09942) find
  35. Lianmin Zheng, Wei-Lin Chiang, Ying Sheng, Siyuan Zhuang, Zhanghao Wu, Yonghao Zhuang, Zi Lin, Zhuohan Li, Dacheng Li, Eric P. Xing, Hao Zhang, Joseph E. Gonzalez, and Ion Stoica. 2023a. Judging llm-as-a-judge with mt-bench and chatbot arena. In Advances in Neural Information Processing Systems.
  36. Zibin Zheng, Neng Zhang, Jianzhong Su, Zhijie Zhong, Mingxi Ye, and Jiachi Chen. 2023b. Turn the rudder: A beacon of reentrancy detection for smart contracts on ethereum. arXiv preprint arXiv:2303.13770. Empirical study showing reentrancy as a key smart contract vulnerability causing significant fin… — [arXiv:2303.13770](https://arxiv.org/abs/2303.13770) find
  37. OpenAI. 2025. GPT-5 System Card. System card. find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/zhang-2026-trustworthy-smart-contract-synthesis-multi/