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

• URL: http://arxiv.org/abs/2607.04631v1
• Date: Mon, 06 Jul 2026 03:31:14 GMT
• Title: Formal Disco: Scalable Open-Ended Generation of Formally Verified Programs
• Abstract summary: Formal Disco is a distributed system for coordination of LLM-based workers.<n>It can be easily applied to open-ended synthetic data generation at scale.<n>We release large datasets of synthetic verified programs in three languages.
• Score: 43.83836626474095
• License: http://creativecommons.org/licenses/by-sa/4.0/
• 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.

Related papers

• The Imitation Game: When LLMs Learn to Reason Like Programs via Code-Centric Reasoning Data Synthesis [50.473217152006875]
  MIMIC is a framework that leverages executable code as a rigorous medium for reasoning data synthesis.<n>MIMIC transforms algorithms into verifiable reasoning trajectories through narrative fusion, code-guided test synthesis, and dynamic code instrumentation.<n>Our method significantly elevates accuracy across general reasoning, complex mathematical benchmarks, and fine-grained deterministic tasks.
  arXiv  Detail & Related papers  (2026-09-13T17:04:16Z)
• Intent Formalization: A Grand Challenge for Reliable Coding in the Age of AI Agents [7.228124845671868]
  Agentic AI systems can now generate code with remarkable fluency.<n>But a fundamental question remains: emphdoes the generated code actually do what the user intended?
  arXiv  Detail & Related papers  (2026-03-17T21:28:59Z)
• Automatic Syntax Error Repair for Discrete Controller Synthesis using Large Language Model [8.741815980649667]
  This paper presents an automated approach that leverages Large Language Models (LLMs) to repair syntax errors in DCS models.<n>It equips the LLM with DCS-specific domain knowledge, including formal grammar rules and illustrative examples, to guide accurate corrections.<n>It achieves a speedup of 3.46 times compared to human developers.
  arXiv  Detail & Related papers  (2025-12-08T07:57:15Z)
• Autoformalizer with Tool Feedback [52.334957386319864]
  Autoformalization addresses the scarcity of data for Automated Theorem Proving (ATP) by translating mathematical problems from natural language into formal statements.<n>Existing formalizer still struggles to consistently generate valid statements that meet syntactic validity and semantic consistency.<n>We propose the Autoformalizer with Tool Feedback (ATF), a novel approach that incorporates syntactic and consistency information as tools into the formalization process.
  arXiv  Detail & Related papers  (2025-10-08T10:25:12Z)
• Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [78.1575956773948]
  Large Language Models (LLMs) trained with Reinforcement Learning (RL) face a significant challenge: their verification processes are neither reliable nor scalable.<n>A promising yet largely uncharted alternative is formal language-based reasoning.<n>Grounding LLMs in rigorous formal systems where generative models operate in formal language spaces (e.g., Dafny) enables the automatic and mathematically provable verification of their reasoning processes and outcomes.
  arXiv  Detail & Related papers  (2025-07-22T08:13:01Z)
• GenerationPrograms: Fine-grained Attribution with Executable Programs [72.23792263905372]
  We introduce a modular generation framework, GenerationPrograms, inspired by recent advancements in "code agent" architectures.<n>GenerationPrograms decomposes the process into two distinct stages: first, creating an executable program plan composed of modular text operations explicitly tailored to the query, and second, executing these operations following the program's specified instructions to produce the final response.<n> Empirical evaluations demonstrate that GenerationPrograms significantly improves attribution quality at both the document level and sentence level.
  arXiv  Detail & Related papers  (2025-06-17T14:37:09Z)
• Accessible Smart Contracts Verification: Synthesizing Formal Models with Tamed LLMs [7.087237546722617]
  One of the most powerful ways of establishing software correctness is by using formal methods.<n>Our work addresses this critical disadvantage by automating the creation of a formal model.<n>In this way, we significantly reduce the amount of time necessary to create formal models.
  arXiv  Detail & Related papers  (2025-01-22T15:57:29Z)
• Joint Verification and Refinement of Language Models for Safety-Constrained Planning [25.390607788572535]
  Large language models can generate programs from natural language descriptions to execute robotic tasks.<n>However, these generated programs often contain errors that violate externally given task specifications.<n>We develop a method that converts generated robot programs into an automaton-based representation and verifies them against task-relevant safety specifications.
  arXiv  Detail & Related papers  (2024-10-18T21:16:30Z)
• Procedures as Programs: Hierarchical Control of Situated Agents through Natural Language [81.73820295186727]
  We propose a formalism of procedures as programs, a powerful yet intuitive method of representing hierarchical procedural knowledge for agent command and control. We instantiate this framework on the IQA and ALFRED datasets for NL instruction following.
  arXiv  Detail & Related papers  (2021-09-16T20:36:21Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.