一句话：提出基于 Lean 多模态验证器 Velvet 的分阶段 agent 流水线 LeetProof，实现从自然语言到程序、规格与机器可检验证明的可认证合成。
可认证程序合成（vericoding）需从自然语言同时生成程序、形式规格与机器可检验的对齐证明，但合成的规格常过弱或过强而缺乏系统检测手段，且验证器按推理模式（自动主动式 vs 交互式）割裂，迫使方法局限于单一范式。作者以 Lean 中融合动态验证、自动证明与交互式证明脚本的多模态验证器 Velvet 为核心，构建分阶段 agent 流水线 LeetProof：先以随机化性质测试验证规格，再依验证条件分解合成子任务，最后将残余证明义务交给面向 Lean 的前沿 AI 证明器。在由既有工作扩充的可认证合成基准上，其规格验证发现参考基准中的缺陷，且在固定预算下 LeetProof 的完全认证成功率显著优于单模态基线，并在两种前沿 LLM 后端上保持一致。
Certified program synthesis (a.k.a. vericoding) is the process of automatically generating a program, its formal specification, and a machine-checkable proof of program/specification alignment from a natural-language task description. Two key challenges make vericoding difficult. First, specifications synthesised from natural language descriptions are often either too weak to be meaningful or too strong to be implementable, yet existing approaches lack systematic means to detect such defects. Second, the program verifiers used to validate results are fragmented: each tool supports a particular reasoning mode—auto-active (e.g., Dafny, Verus) or interactive (e.g., Rocq, Lean)—with its own trade-off between automation and expressivity. This forces each synthesis methodology to target a single paradigm, limiting the tasks it can handle. We overcome both challenges by structuring the synthesis workflow in stages around a multi-modal verifier—a single tool that combines dynamic validation, automated proofs, and interactive proof scripting within one foundational framework. We realise this idea in LeetProof, a new agentic pipeline built on Velvet, a multi-modal program verifier built in the Lean theorem prover. Multi-modality enables LeetProof to validate generated specifications via randomised property-based testing before any code is synthesised, decompose the synthesis task into sub-problems guided by verification conditions, and delegate residual proof obligations to frontier AI provers specialised for Lean. We evaluate LeetProof on an extensive benchmark suite derived from prior work on certified synthesis. Our specification validation uncovers defects in existing reference benchmarks, and LeetProof's staged pipeline achieves a significantly higher rate of fully certified solutions than a single-mode baseline at the same fixed budget—consistently across two different frontier LLM backends.
@inproceedings{abs-2604-16584,
title = {Certified Program Synthesis with a Multi-modal Verifier},
author = {Yueyang Feng and Dipesh Kafle and Vladimir Gladshtein and Vitaly Kurin and George Pîrlea and Qiyuan Zhao and Peter Müller and Ilya Sergey},
booktitle = {ASE},
year = {2026},
doi = {10.1145/3832783.3837559}
}