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

Jul 16, 2026

Upload by Maeve

Rapid advances in AI agents reduce the cost of generating code, yet verification quality has lagged because verified-program data in verification-aware languages is scarce. FORMAL DISCO is proposed as a distributed coordination system for LLM workers to produce open-ended synthetic verified programs. It logs agent traces, enables distillation and self-improvement, and applies maximum-entropy generation via iterative supervised fine-tuning. Large datasets are released for Dafny, Verus, and Frama-C, training open models for verification-relevant tasks.

LanguageEnglish

CategoryResearch & Report

FormatPDF

Pages46

Reading Time1 h 56 min

Abstract

Introduction

arXiv :2607 .0463 1v 1 [ cs .AI] 6 Jul 2026 FORMAL DISCO: Scalable Open-Ended Generation of Formally Verified Programs Gabriel Poesia 1 Simon Henniger2 Tzu-Han Hsu2 Yilun Du 1 ,2 Nada Amin 1 ,2 1 Kempner Institute, Harvard University 2 School of Engineering and Applied Sciences, Harvard University Corresponding authors: [gabriel_poesia@fas.harvard.edu](gabriel_poesia@fas.harvard.edu), [namin@seas.harvard.edu](namin@seas.harvard.edu) 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 humanwritten 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 opensource 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 several proprietary models. Overall, our work offers a path to create synthetic data at scale for formal reasoning domains and overcome the long-standing data barrier. 1 Introduction AI coding agents are rapidly changing the practice of software engineering [30] . Frontier AI agents at scale have been shown to author complete, highly complex code bases spanning tens to hundreds of thousands of lines of code, such as the C compiler implemented by Anthropic’s Claude Code [26] . While the cost of writing code is rapidly diminishing, we still lack means to verify the correctness of AI-written programs at scale: testing can only cover finitely many cases, and manual code review is infeasible at this new pace. But bugs can be extremely costly—a bug in a compiler, for instance, can carry over to all programs compiled by the compiler, with potential catastrophic consequences downstream. How can we ensure that programs behave as intended, so we can rely on AI-written code? Formal program verification provides the strongest possible form of correctness assurance [25, 19, 18, 17] . A formally verified program comes with both a logical specification of its behavior as well as a proof that a given implementation satisfies the specification. If AI agents write verified programs, humans can check correctness by writing or inspecting a formal specification, but can then trust a symbolic verifier to judge whether the implementation satisfies the given specification. Preprint. Unfortunately, current LLMs, especially open-weight models, are still limited in their ability to write verified programs, or even assist humans with verification-related tasks (such as annotating loops with invariants) . This is to be expected given the lack of human-written examples of programs inmost languages supporting formal verification. For instance, while there are millions of Python repositories on GitHub, the largest existing public dataset of programs in Dafny—a verificationaware programming language—is DafnyB

FAQs

What problem does FORMAL DISCO address in verified-program generation?

The work targets the mismatch between rapidly improving AI code generation costs and the lack of scalable quality assurance. It also addresses data scarcity for human-written examples in verification-aware languages.

How does FORMAL DISCO generate verified programs at scale?

It coordinates LLM-based workers through a shared agenda and uses three agent roles: initiators (sketch programs from READMEs and documentation), fixers (apply compiler/verifier feedback), and extenders (patch working programs to increase complexity).

How are the synthetic programs used to improve models for verification tasks?

FORMAL DISCO records all agent traces for distillation from stronger models and self-improvement. It further proposes maximum-entropy synthetic program generation using iterative supervised fine-tuning to learn increasingly diverse programs.

Jul 16, 2026

Upload by Maeve