Formal Disco: Scalable Open-Ended Generation of Formally Verified Programs
Not on the map. Why?
Abstract (arXiv)
The cost of producing code is rapidly diminishing with increasingly capable AI agents, while quality assurance of generated programs has not kept pace. Formal verification provides the strongest possible guarantees, but the ability of AI models to work with verification-aware languages is hindered by the scarcity of human-written examples of programs in those languages. To tackle this prevalent data scarcity issue, we propose Formal Disco: a distributed system for coordination of LLM-based workers that can be easily applied to open-ended synthetic data generation at scale. We use Formal Disco to share tasks and programs between three classes of workers: "initiators", which read random READMEs from open-source repositories and documentation snippets to sketch a related verified program, "fixers" which take compiler and verifier feedback and attempt to resolve issues, and "extenders" that take working programs and propose patches to expand them. Formal Disco records all agent-generated traces and uses them both for initial distillation from a stronger model as well as self-improvement. We also propose a principle of maximum entropy for synthetic program generation, and use entropy maximization via iterative supervised fine-tuning to learn to generate increasingly diverse programs over time. We release large datasets of synthetic verified programs in three languages - Dafny, Verus, and Frama-C -, and fine-tune open models for verification-relevant tasks, often matching or exceeding the performance of Claude Opus 4.5. Overall, our work offers a path to create synthetic data at scale for formal reasoning domains and overcome the long-standing data barrier.
Key facts. Cited by 1 paper in the map (data through 14 Oct 2026). Builds on 21 of its 43 references that are in the map. First posted on arXiv 6 Jul 2026.
Builds on
21 of 43 references.
References · 21
- 2021LoRA: Low-Rank Adaptation of Large Language Modelscited by 14,380
- 2023Voyager: An Open-Ended Embodied Agent with Large Language Modelscited by 2,191
- 2024Qwen2.5-Coder Technical Reportcited by 1,203
- 2023RAFT: Reward rAnked FineTuning for Generative Foundation Model Alignmentcited by 686
- 2023Textbooks Are All You Need II: phi-1.5 technical reportcited by 565
- 2023Reinforced Self-Training (ReST) for Language Modelingcited by 500
- 2023TinyStories: How Small Can Language Models Be and Still Speak Coherent English?cited by 449
- 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 234
- 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 133
- 2025STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Provingcited by 79
- 2023Clover: Closed-Loop Verifiable Code Generationcited by 67
- 2024Towards AI-Assisted Synthesis of Verified Dafny Methodscited by 58
9 more
- 2024DafnyBench: A Benchmark for Formal Software Verificationcited by 57
- 2023Verus: Verifying Rust Programs using Linear Ghost Types (extended version)cited by 53
- 2024AutoVerus: Automated Proof Generation for Rust Codecited by 49
- 2023Knowledge Transfer from High-Resource to Low-Resource Programming Languages for Code LLMscited by 45
- 2024Learning Formal Mathematics From Intrinsic Motivationcited by 45
- 2024Automated Proof Generation for Rust Code via Self-Evolutioncited by 33
- 2026Agentic Much? Adoption of Coding Agents on GitHubcited by 32
- 2024Collapse of Self-trained Language Modelscited by 5
- 2026Reducing the Costs of Proof Synthesis on Rust Systems by Scaling Up a Seed Training Setcited by 3
Built on by
Citing papers per year: 2026: 1.
1 paper.