Source-linked AI summary
ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis
Mantas Baksys, Stefan Zetzsche, Olivier Bouissou, Remi Delmas, Soonho Kong, Sean B. Holden
TL;DR
Verified code is scarce, despite formal verification’s role in providing machine-checked guarantees when functional correctness alone is insufficient. ATLAS generates verified Dafny programs from algorithmic problems and decomposes them into training examples; fine-tuning improves results on both DafnyBench and DafnySynthesis.
Problem
Verified code is scarce, while safety-critical applications require precise specifications and proofs beyond functional code or testing alone.
Source: §1 · p. 1Method
ATLAS synthesizes verified Dafny programs from natural-language problems, reference implementations, and tests, then decomposes pipeline outputs into multiple training tasks.
Source: §1 · p. 2Results
32.4% to 56.9% on DafnyBench and 15.8% to 65.8% on DafnySynthesis after fine-tuning Qwen 2.5 7B Coder on ATLAS data.
Source: §6 · p. 8Takeaways & Limitations
The results demonstrate synthetic data generation as a viable path to scaling LLM capabilities for formal verification.
Source: §6 · p. 8The approach may be constrained by the 7B parameter scale of its base model, compared with higher reported frontier-model performance.
Source: §4.2.1 · p. 7
Abstract
from arXiv · showhide
Large language models have become proficient at generating functional code, but ensuring the output truly matches the programmer's intent remains difficult. Testing improves trust, yet for safety-critical applications, formal verification provides the only true guarantees through machine-checked proofs. However, verified code remains scarce compared to mainstream languages or mathematical theorem proving, limiting LLM capabilities in this domain. We present ATLAS, an automated pipeline that synthesizes verified programs to address this data bottleneck. Applied to the TACO dataset of Python solutions to LeetCode-style problems, ATLAS generates 2.7K verified Dafny programs, each with high-quality specifications and machine-checked proofs. Through task decomposition, we extract 19K training examples. Fine-tuning Qwen 2.5 7B Coder on this data improves performance from 32.4% to 56.9% on DafnyBench and from 15.8% to 65.8% on DafnySynthesis, demonstrating that synthetic data generation is a viable path to scaling LLM capabilities for formal verification.
1. Introduction
ATLAS targets the scarcity of verified Dafny programs by synthesizing programs with specifications and proofs from problem descriptions, reference implementations, and tests. Its generated data improves Qwen 2.5 7B Coder results on both Dafny benchmarks.
1. Introduction
- Verified code is scarce, and generating it requires implementations, specifications, and proof annotations rather than only functional code.The paper distinguishes this challenge from autoformalizing mathematical statements.Source: §1 · p. 2
- ATLAS takes a natural-language problem, a mainstream-language reference implementation, and tests as input, then iteratively refines a verified program with specifications and proof annotations.It checks specification consistency with test cases and seeks specifications strong enough to determine expected outputs for test inputs.Source: §1 · p. 2
- ATLAS produces 2.7K verified Dafny programs and expands them into approximately 19K training examples through task decomposition.Tasks include synthesizing code and specifications from natural language, inferring implementations from specifications, and repairing specifications, implementations, and proofs.Source: §1 · p. 2
- The pipeline defines test-case-based soundness and completeness criteria to assess specification quality and filter degenerate solutions.Source: §1 · p. 2
2. The Dafny Language
Dafny programs pair implementations with specifications expressed as preconditions and postconditions. Verification uses weakest-precondition reasoning and an SMT solver, with ghost code available to guide proofs.
2. The Dafny Language
- Dafny expresses program specifications as Hoare triples: a precondition, a method body, and a postcondition.The precondition is written as requires and the postcondition as ensures.Source: §2 · p. 2
- Dafny translates code and specifications into Boogie, which computes the weakest precondition; Z3 checks whether the precondition implies it.A valid verification condition means the program is verified.Source: §2 · pp. 2–3
- When automatic verification cannot succeed, ghost code can guide the solver without changing runtime behavior.Examples include assertions, loop invariants, lemmas, and calculational proofs.Source: §2 · p. 3
- Dafny has been used for large-scale verification projects in industry and academia, including AWS’s Cedar authorization engine and IronFleet.The cited examples also include cryptographic libraries, a file system, and an Ethereum Virtual Machine specification.Source: §2 · p. 3
3. ATLAS
ATLAS turns programming problems, reference implementations, and tests into verified Dafny programs through contract generation, implementation synthesis, and iterative validation. It produced 2,751 verified programs, with success varying by problem difficulty and skill type.
3.1. Overview
- ATLAS separates problem-statement generation from solution synthesis, using an immutable formal contract to guide verified implementation generation.It starts from programming problems paired with reference solutions and input-output tests.Source: §3 · p. 3, §3.1 · p. 3
3.1.1. CONTRACT GENERATION
- The first stage generates a method signature, strong pre- and postconditions, and executable tests, refining them with compiler feedback and soundness and completeness checks.Specifications and tests are synthesized from reference solutions and examples, with additional tests generated by the agent.Source: §3.1.1 · p. 3
3.1.2. IMPLEMENTATION GENERATION
- Once the contract is frozen, ATLAS synthesizes implementations, assertions, and lemmas, then checks contract adherence, verification, compilation, and test passage.Implementation generation may regenerate specifications subject to strict adherence constraints.Source: §3.1.2 · p. 4
3.2. Soundness and Completeness
- Soundness lemmas test contract consistency on concrete examples, while completeness checks detect postconditions that permit incorrect outputs.The perturbation approach tests modified outputs as a practical alternative to contradiction proofs that may exceed automated provers’ capabilities; this trades formal completeness guarantees for practical automated verification.Source: §3.2 · pp. 4–5
3.3. Analysis
- 2,751 verified Dafny programs with specifications and machine-checked proofs were generated from TACO-verified.The pipeline analyzes synthesis performance across difficulty levels and problem types.Source: §3.3 · p. 5
3.3.1. DIFFICULTY RATINGS
- 47.1% success on EASY problems falls to approximately 20% for HARD and VERY HARD problems, while successful-program length rises from 3,848 to over 5,600 characters.The authors report that failed attempts remain long across difficulty categories.Source: §3.3.1 · p. 6
4. Supervised Fine-Tuning
ATLAS uses verified programs and their execution traces to create multiple training tasks, then fine-tunes Qwen 2.5 7B Coder for Dafny. The fine-tuned model improves on both Dafny benchmarks, with results varying by task and evaluation setting.
4.1.1. DATASET CURATION
- The curated dataset combines prompts, intermediate specification and implementation attempts, judge feedback, and final programs to produce multiple training tasks per pipeline run.Correction tasks make up over 35% of the dataset, and proof infilling trains reconstruction of annotations such as loop invariants and auxiliary lemmas.Source: §4.1.1 · p. 6
4.1.2. EXECUTION
- Qwen 2.5 7B Coder is fine-tuned with LoRA supervised fine-tuning and evaluated on two downstream Dafny benchmarks.Training uses up to 10 epochs and standard cross-entropy loss with gradient clipping.Source: §4.1.2 · pp. 6–7
4.2.2. DAFNYSYNTHESIS
- On DafnySynthesis, removing soundness and completeness checks lowers Pass@5 to 58.4%, and removing test cases yields 59.6% at Pass@5.The benchmark evaluates generating verified Dafny programs from programming tasks.Source: §4.2.2 · pp. 7–8