← 研踪 PaperTrailACL Anthology · ACL 2026:acl:2026.acl-long.1836 · 记录 #1
Towards Trustworthy Smart Contract Synthesis: A Multi-Agent Framework with Lean-Based Verification
来源日期（仅到月份） 2026-07
来源记录日期 2026-07
雷达观测 2026-11-01 21:48
摘要
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 auto-formalization 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 open-source our framework and datasets at: https://github.com/gl-bowei/LeVer
论文发现出处
这些页面提供论文线索，不代表同行评审或质量认证。
观测到的版本
平台记录号代表本站观测到的元数据变化，不是作者修订号。来源日期仅到月份或年份时，按该月或该年首日存档。
记录 #1 · 2026-07 · 最新观测版本
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 auto-formalization 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 open-source our framework and datasets at: https://github.com/gl-bowei/LeVer
查看此版本解读 →查看此版本原文 ↗