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

🕒 Published (v1): 2026-07-06 03:31 UTC · Source: Arxiv · link

Why this paper was selected

Formal Disco: AI agents generating formally verified code at scale; Poesia (Stanford) + Yilun Du (MIT)

Ask a follow-up

Open an assistant pre-loaded with this paper's context.

💬 Ask ChatGPT✦ Ask Claude

TL;DR

Formal Disco is a distributed multi-agent system that coordinates LLM-based workers to generate synthetic formally verified programs at scale, addressing the chronic data scarcity in verification-aware languages. It introduces a principle of maximum entropy over program features to guide and directly optimize for dataset diversity. The system releases >100k verified programs in Dafny, Verus, and Frama-C, and fine-tuned open models that approach proprietary model performance on verification tasks.

Problem

Formal verification languages (Dafny, Verus, Frama-C) are extreme low-resource languages: the largest public Dafny dataset (DafnyBench) contains fewer than 800 files. Without sufficient training data, LLMs cannot reliably write verified programs or assist with verification subtasks (e.g., loop invariant annotation). Testing and manual code review cannot scale to AI-generated codebases, making formal verification the only viable correctness guarantee — yet the data bottleneck blocks AI progress on it.

Method

Formal Disco is a distributed agenda-based system where LLM workers asynchronously consume and produce tasks referencing a shared object database (programs + metadata). Three worker types operate in a pipeline:

• Initiator: samples a random GitHub README and 1–2 language reference snippets as seed, prompts an LLM to sketch an initial verified program, then creates either an extend or repair task based on verifier feedback.
• Fixer: claims repair tasks, performs chain-of-thought reasoning over compiler/verifier errors, and outputs a diff; retries up to 3 times before marking the task failed.
• Extender: claims extend tasks on verified programs and proposes complexity-expanding patches (new lemmas, methods, etc.); on failure, re-queues for repair.

Every LLM call is logged as a distillation example. Initial runs use frontier models (Claude Opus/Sonnet) to seed distillation data; subsequent runs use fine-tuned open models (Qwen 2.5-Coder 32B with LoRA). Self-improvement is guided by entropy maximization: given program features \(f_1, \ldots, f_k\) (e.g., loop depth, lemma usage, identifier vocabulary), the per-program \(f\)-surprisal

\[S(f, p, D) = -\log P_f^D(f(p))\]

decomposes Shannon entropy \(H(f, D) = \frac{1}{|D|}\sum_{p \in D} S(f, p, D)\), enabling ranking/filtering (ReST/RAFT-style) of training examples to prefer outputs that increase dataset diversity rather than just verification success.

Key Contributions

• Formal Disco framework: language-agnostic distributed agenda for coordinating LLM workers on open-ended verified program generation, with full trace logging for distillation and self-improvement.
• Maximum-entropy principle for synthetic datasets: unifies prior intuitions (size, feature coverage, complexity) under a single measurable objective; enables tracking and direct optimization of dataset diversity across iterations.
• Large-scale dataset releases: dafny-disco, framac-disco, and verus-disco — each exceeding 100k complete verified programs; Dafny and Frama-C corpora are orders of magnitude larger than any prior public dataset.
• Fine-tuned open models: Qwen 2.5-Coder 32B trained on Formal Disco data achieves performance competitive with Claude 4.5 Opus on verification tasks in Dafny and Verus.

Results

• Frontier model success rate per worker task is typically below 15% at initiation; even so, 10k attempts suffice to produce enough distillation data for open model bootstrapping.
• Datasets in all three languages exceed 100k complete verified programs; Dafny and Frama-C corpora achieve orders of magnitude more programs than prior public datasets.
• Qwen 2.5-Coder 32B fine-tuned on Formal Disco data matches or exceeds several proprietary models and in some cases is competitive with Claude 4.5 Opus on verification-relevant tasks (loop invariant annotation, lemma proving).
• README-seeded initiation measurably improves corpus entropy over program themes compared to LLM-only seeding (theme collapse without external signal).

Limitations

• Frontier model task success rate is low (<15%), making initial data collection expensive; the system requires a costly seed run before open-model self-improvement becomes viable.
• Entropy maximization framework requires hand-selecting which program features \(f_i\) to optimize; the choice of features is language-specific and may miss important dimensions.
• Generation is inherently open-ended, not task-directed; downstream task alignment requires an additional fine-tuning stage on top of the synthetically generated corpus.
• Evaluation is limited to tasks with human-written benchmarks in Dafny and Verus; Frama-C downstream task performance is not reported (paper text provided is truncated).
• Self-training collapse risk (diversity shrinkage over iterations) is addressed by entropy maximization but not fully ablated in the available text.

Relevance to Agentic AI / LLM Agents

Formal Disco is a concrete instantiation of a multi-agent workflow where specialized LLM agents (initiator, fixer, extender) collaborate through a shared task queue and object store, with the verifier serving as an automated reward signal — a pattern directly relevant to building self-improving agentic systems. The distributed agenda design, with asynchronous task claim/dispatch and horizontal scaling, is a transferable architectural primitive for any domain where correctness can be checked symbolically. The entropy-maximization framework addresses a core failure mode of agentic self-improvement (diversity collapse), offering a principled, measurable alternative to ad-hoc diversity heuristics. This work extends the "LLM agent + verifier-as-oracle" paradigm from theorem proving (DeepSeek-Prover, Goedel-Prover) into executable verified programs, directly relevant to building agents that can produce trustworthy code.