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

The cost of producing code is rapidly decreasing with increasingly capable AI agents, but quality assurance has not kept pace. Formal verification can provide strong correctness guarantees on generated code, but languages supporting verification are still challenging for coding models due to the scarcity of available examples of programs in those languages. To tackle this issue, we propose Formal Disco: a scalable system for coordinated 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 short related verified program, "fixers" which resolve issues given compiler/verifier feedback, and "extenders" that propose patches to expand working programs. Formal Disco records and uses agent traces both for initial distillation from a stronger model and for self-improvement. To prevent diversity collapse, we propose a simple 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 Qwen-2.5 Coder 32B for verification-relevant tasks, matching Claude Opus 4.5 on a Verus annotation task and closing much of the gap in all other cases. Overall, our work offers a path to using synthetic verified programs at scale to overcome the long-standing data barrier in AI-assisted verified programming.