# Formal Disco: Scalable Open-Ended Generation of Formally Verified Programs

arXiv: https://arxiv.org/abs/2607.04631 · HTML: https://mlsanity.com/paper/2607.04631/

## Key facts

- Cited by 1 papers 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 (most cited first, 21 of 21)

- [LoRA: Low-Rank Adaptation of Large Language Models](https://mlsanity.com/paper/2106.09685/) (2021)
- [Voyager: An Open-Ended Embodied Agent with Large Language Models](https://mlsanity.com/paper/2305.16291/) (2023)
- [Qwen2.5-Coder Technical Report](https://mlsanity.com/paper/2409.12186/) (2024)
- [RAFT: Reward rAnked FineTuning for Generative Foundation Model Alignment](https://mlsanity.com/paper/2304.06767/) (2023)
- [Textbooks Are All You Need II: phi-1.5 technical report](https://mlsanity.com/paper/2309.05463/) (2023)
- [Reinforced Self-Training (ReST) for Language Modeling](https://mlsanity.com/paper/2308.08998/) (2023)
- [TinyStories: How Small Can Language Models Be and Still Speak Coherent English?](https://mlsanity.com/paper/2305.07759/) (2023)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Proving](https://mlsanity.com/paper/2502.07640/) (2025)
- [STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving](https://mlsanity.com/paper/2502.00212/) (2025)
- [Clover: Closed-Loop Verifiable Code Generation](https://mlsanity.com/paper/2310.17807/) (2023)
- [Towards AI-Assisted Synthesis of Verified Dafny Methods](https://mlsanity.com/paper/2402.00247/) (2024)
- [DafnyBench: A Benchmark for Formal Software Verification](https://mlsanity.com/paper/2406.08467/) (2024)
- [Verus: Verifying Rust Programs using Linear Ghost Types (extended version)](https://mlsanity.com/paper/2303.05491/) (2023)
- [AutoVerus: Automated Proof Generation for Rust Code](https://mlsanity.com/paper/2409.13082/) (2024)
- [Knowledge Transfer from High-Resource to Low-Resource Programming Languages for Code LLMs](https://mlsanity.com/paper/2308.09895/) (2023)
- [Learning Formal Mathematics From Intrinsic Motivation](https://mlsanity.com/paper/2407.00695/) (2024)
- [Automated Proof Generation for Rust Code via Self-Evolution](https://mlsanity.com/paper/2410.15756/) (2024)
- [Agentic Much? Adoption of Coding Agents on GitHub](https://mlsanity.com/paper/2601.18341/) (2026)
- [Collapse of Self-trained Language Models](https://mlsanity.com/paper/2404.02305/) (2024)
- [Reducing the Costs of Proof Synthesis on Rust Systems by Scaling Up a Seed Training Set](https://mlsanity.com/paper/2602.04910/) (2026)

## Built on by (most cited first, 1 of 1)

- [Djinnlang: Higher-Level Programming by Unambiguous Specification with an LLM in the Compiler](https://mlsanity.com/paper/2609.23954/) (2026)

## 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.