As AI agents become increasingly capable, the cost of code production is rapidly declining, while the quality assurance of generated programs has not kept pace. Formal verification offers the strongest guarantees, but the ability of AI models to work with verification-aware languages is hampered by a lack of human-written examples. To address this data scarcity issue, we propose Formal Disco: a distributed system for coordinating LLM-based workers, easily applicable for open-ended synthetic data generation at scale.
Formal Disco shares tasks and programs among three classes of workers:
- Initiators: who read random READMEs from open-source repositories and documentation snippets to sketch a related verified program.
- Fixers: who take compiler and verifier feedback to resolve issues.
- Extenders: who take working programs and propose patches to expand them.
Formal Disco records all agent-generated traces to facilitate initial distillation from a stronger model and self-improvement. We also propose a principle of maximum entropy for synthetic program generation and utilize 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 provides a pathway to create synthetic data at scale for formal reasoning domains, overcoming the long-standing data barrier.
Blogger's Review: This research opens new horizons in formal verification and large-scale program generation. By introducing multi-class workers and the maximum entropy principle, it significantly enhances the diversity and quality of program generation, laying a solid foundation for future formal verification applications.