AI summaryⓘ
The authors address the problem that while AI can generate code easily, ensuring the code is formally verified is still hard because there are few examples of verified programs for AI to learn from. They create Formal Disco, a system that splits tasks among AI 'workers' to write, fix, and extend verified programs using open-source documentation. Their system improves itself over time by learning from its attempts and focuses on generating a wide variety of verified programs. They produce large datasets of these programs in three specialized languages and fine-tune AI models to perform formal verification tasks effectively. This work helps overcome the challenge of lacking verified code examples for training AI in formal reasoning.
formal verificationverified programsLLM (large language model)synthetic data generationDafnyVerusFrama-Cfine-tuningentropy maximizationcode quality assurance
Authors
Gabriel Poesia, Simon Henniger, Tzu-Han Hsu, Yilun Du, Nada Amin
Abstract
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.