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

Idea

LeVer 将 smart contract synthesis 变成生成、形式验证、对抗执行和修复的闭环：不仅检查已有漏洞模式，还从需求推断 safety properties，并将 Solidity 抽象为 Lean 4 状态转移模型进行证明。攻击轨迹还能反向扩充待验证性质，使动态测试与形式推理共同推动代码演化。

Research Problem

LLM 能轻易生成 Solidity，但传统编译、静态扫描和测试很难证明资产管理逻辑满足需求；仅枚举已知漏洞也难覆盖复杂状态交互。另一个缺口是自然语言需求与可证明 invariant 之间存在语义距离，完整性质集合无法直接给定，复杂性质还可能超出证明预算。

Insight

针对选定的状态安全性质，若初始状态满足 invariant 且每个成功转移保持它，就能约束所有可达状态。实际攻击则提供具体反例及缺失性质的线索。两种机制互补，但形式结论依赖所采用的语义抽象与性质集合，不能直接扩大为任意 EVM 行为的保证。

Method

1. Coder 根据自然语言需求生成候选合约；PropertySelector 依据 Hierarchical Assurance Spectrum 选择相关 invariant，覆盖基础执行约束到更高层经济行为。
2. LeanFormalizer 在 deterministic closed-system abstraction 下，将 storage 映射为不可变状态、函数映射为状态转移，并将事件与转账意图显式编码为输出；为各性质生成待证明 theorem 模板。
3. LeanProver 通过 LLM 生成 tactics，利用 Lean compiler 反馈修复 proof，替换临时 sorry 占位；成功证明说明形式模型中的指定性质成立。
4. Attacker 在 POMG sandbox 中组织诚实和恶意代理，并允许对抗性交易排序；Runtime Oracles 在原子转移后检查性质。AttackAnalyst 汇总反例和证明失败，反馈 Coder 修复，并通过 Attack-to-Property 扩展性质库，直到满足停止条件或预算耗尽。