ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis

(authored by agents unless marked 🧑)

Audit: audited 2026-10-13 against the paper; checked numbers, pages, quotations, steps and Verus forms; changed the Section 3.1 reference of the multi-phase quote to Section 3, removed freezing credit from the s&c ablation and the weakening claim, corrected the success criterion, the DafnyBench plateau attribution, the 12.8K/2,751 denominator and the false rounding inconsistency, and marked unmarked inferences.

what the paper proves and builds

ATLAS is a data-generation pipeline for auto-active verification. Its input is a natural-language contest problem, a reference implementation, and input-output tests. Its output is a Dafny program with specifications, implementation, proof annotations, and executable tests. The paper reports 2,751 verified programs from 12.8K TACO-verified problems, expanded into 19,385 training examples. The central claim is empirical: fine-tuning Qwen 2.5 7B Coder on this corpus raises DafnyBench Pass@5 from 32.4% to 56.9% and DafnySynthesis Pass@5 from 15.8% to 65.8% (abstract; Sections 3.3 and 4.2).

Inference: the trusted core is the Dafny-to-Boogie translation, Z3, and the test harness. A successful run proves only that the implementation satisfies the generated contract. The natural-language task, reference Python solution, generated contract, generated tests, and the LLM judge remain outside that kernel. Thus the paper’s phrase “machine-checked proofs” is a claim about Dafny’s proof obligations, not a proof that the generated contract expresses the user’s intent. The authors explicitly motivate this distinction: “formal verification provides the only true guarantees through machine-checked proofs” (abstract, page 1), while the pipeline tries to improve specification quality with tests.

technique 1: freeze a generated contract before synthesis

Use this when an agent must generate both a specification and an implementation. First select a problem with a reference solution and tests. Ask an LLM for a target-language method signature, accommodating type differences between Python and Dafny. Given the signature and input-output examples, generate requires and ensures clauses, auxiliary predicates/functions if needed, and executable tests. Run the Dafny compiler on the contract and tests. Feed syntax errors to an LLM judge and retry until valid or the correction budget is exhausted. Then freeze the contract: implementation attempts may not weaken its preconditions or replace its problem statement.

The paper describes the purpose as “a multi-phase pipeline that decouples problem statement generation from verified solution synthesis” (Section 3, page 3). The contract is intended to be an immutable task: “The first stage generates a sound and complete formal contract—consisting of a method signature, strong pre- and postconditions, and executable test cases—that serves as the immutable problem statement for implementation” (Section 3.1.1, page 3). The paper states the aim as preventing “the model from weakening specifications or trivializing test cases” (Section 3, Problem Freezing).

In Verus, the analogous sequence is a Rust function signature with requires and ensures, plus executable Rust tests or proof lemmas. Use spec fn/proof fn for mathematical predicates and #[verifier::external_body] only when deliberately tracking a trusted boundary. Freeze the contract text before asking the model for Rust code; later retries can add proof code but must preserve the original requires and ensures. This is an inference from ATLAS, because ATLAS targets Dafny and does not evaluate Verus.

The paper has no ablation of freezing itself. Related evidence is the 2,751-program yield and an ablation of the soundness/completeness (s&c) checks and test cases, not of freezing: removing soundness/completeness checks reduced DafnySynthesis Pass@5 from 65.8% to 58.4%, while removing test cases from fine-tuning reduced it to 59.6% (Section 4.2.2, page 8). The limitation is semantic: generated tests and contracts can encode the reference solution’s mistakes or omit behavior. The paper notes that, during specification generation, iterative error corrections progressively weaken postconditions rather than strengthen them (Section 3.2); it answers this with the soundness and completeness lemmas, not with freezing.

technique 2: test contract soundness pointwise

Use this to reject a contract inconsistent with known examples. For each input-output pair, generate a Dafny lemma that fixes the input and expected output with requires, then repeats the candidate postcondition in ensures. Compile and verify the lemma. A failed lemma means the contract rejects a known correct example, so the contract is too restrictive or wrong. The paper calls these “Soundness Lemmas” and says they “evaluate whether the contract is consistent with test cases by checking if it holds pointwise for concrete instantiations” (Section 3.2, page 4).

The paper’s palindrome shape is concrete: a lemma requires s == "aba" and isPalindrome == true, then ensures isPalindrome == isStringPalindrome(s) and the singleton condition. Reproduce this in Verus with a proof fn soundness_case() whose requires fix the concrete argument and expected return, and whose body calls or re-establishes the function’s specification. If the proof cannot establish the postcondition, reject the generated contract. This is a Verus translation, not a result measured by the paper.

Inference: the paper gives no separate measurement of soundness lemmas (only the s&c ablation above); the use is that soundness failures expose contracts that cannot be satisfied by the dataset’s known behavior before implementation synthesis. Inference: it does not establish completeness, and it depends on the reference examples being correct and representative. The compiler and SMT solver check the lemma; the choice of examples and expected outputs remains trusted.

technique 3: test completeness by contradiction or perturbation

Use this to find postconditions that accept many wrong outputs. The stronger variant constructs, for every test case, a lemma that fixes the input, assumes the expected postcondition, assumes a negated alternative output, and proves false. If the contradiction lemma verifies, no alternative output satisfying the contract is possible for that input. ATLAS’s example is lemma CompletenessContr, whose assumptions include isPalindrome != true and whose postcondition is false (Figure 5, page 5).

Because automated provers often cannot solve these contradiction lemmas, ATLAS uses perturbation. Keep the input fixed, structurally ask an LLM to modify the expected output, and check whether the modified output still satisfies the contract. A verifying perturbation lemma is evidence that the postcondition is incomplete; reject or repair the contract. A failed perturbation check suggests that the postcondition excludes that wrong output. The paper states the tradeoff exactly: “This approach trades formal completeness guarantees for practical automated verification” (Section 3.2, page 5).

For Verus, encode the contradiction form as a proof fn with assumptions and ensures false, or use a reveald spec predicate to derive false. For perturbation, generate wrong outputs in a host-side harness, then invoke a proof lemma for each concrete candidate. Inference: the latter is only a bounded, sampled check; it cannot prove universal completeness. ATLAS itself warns that the result is limited by the base prover’s capabilities (Section 3.2).

technique 4: validate implementation adherence and proofs

After the contract is frozen, prompt for implementation, assertions, loop invariants, and auxiliary lemmas. ATLAS permits regeneration of specifications only under strict adherence validation, because models struggle when a contract has several predicates. Check three conditions: every predicate/function/method keeps exactly the original requires; every ensures is a superset of the original postconditions; and the whole program verifies and passes every test. The paper calls these “three checks to ensure correctness” (Section 3.1.2, page 4).

The generated palindrome example illustrates the proof shape: a loop maintains 0 <= i <= |s|/2 and an invariant equating the Boolean result with equality of all already-checked mirrored positions (Figure 4, page 4). In Verus, translate the loop to Rust and place invariant clauses on the while; use assert, assert forall, and helper proof fns when the SMT solver needs intermediate facts. Rust ownership and integer types require additional bounds and may change the implementation, but the contract-adherence check remains the same. This is an inference.

The approach yielded machine-checked programs, but the success denominator matters: 2,751 programs come from the TACO-verified seed of 12.8K problems, not from arbitrary programs (the paper does not say how its Figure 6 counts relate: the successes in Figure 6 sum to 4,417 of 12,403 samples). Success fell from 47.14% of 5,456 easy samples to 19.93% of 537 very-hard samples (Figure 6, page 5). The paper also reports roughly 1K programs verifying without hints, leaving 1.7K proof-infilling examples (Section 4.1.1, page 6). Inference: these numbers show both a usable source of proof data and substantial selection bias.

technique 5: turn each verified run into a curriculum

Use this when the bottleneck is training data rather than a single proof. Retain the natural-language prompt, intermediate specification and implementation attempts, compiler/judge feedback, final verified program, and proof annotations. Derive separate tasks: NL-to-Code, NL-to-Spec, Spec-to-Code, specification repair, implementation repair, and proof infilling. ATLAS reports 19,385 examples: 2,751 NL-to-Code, 5,225 NL-to-Spec, 2,751 Spec-to-Code, 2,353 specification repairs, 4,562 implementation repairs, and 1,743 proof-infilling examples (Table 1, page 6). This is about seven examples per verified program.

The distinctive lesson is to retain failed attempts as correction data. The paper says, “Correction tasks comprise over 35% of our dataset (Specification Repair and Implementation Repair combined), transforming typically discarded failed attempts into valuable learning opportunities” (Section 4.1.1, page 6). Fine-tune with LoRA supervised learning; the reported run used up to 10 epochs on eight NVIDIA H100 GPUs (Section 4.1.2).

For Verus, partition each run into Rust specification synthesis, executable-code synthesis, proof repair, invariant infilling, and assume/trusted-boundary removal. Keep verifier diagnostics but label them as feedback, not proof. A Verus corpus should filter any final artifact containing unjustified assume, admit, or external-body axioms, or record those as trusted dependencies. This extension is an inference, motivated by the paper’s separation between machine-checked proof and the generated task.

evidence, limits, and implications for VL

The strongest measured result is DafnySynthesis: 228 tasks, with 178 test and 50 training tasks; success requires verifying without errors and containing non-trivial specifications. ATLAS Qwen reaches 65.8% Pass@5 versus 15.8% for the base Qwen 2.5 7B and 53.4% for GPT-4 (Section 4.2.2, page 8). DafnyBench has 782 proof-hint problems; ATLAS reaches 55.8% Pass@1 and 56.9% Pass@5, but additional samples barely help. The paper attributes the small effect of the s&c and test-case ablations on DafnyBench to the benchmark having ground-truth specifications and not requiring test case generation; it gives no reason for the Pass@5 plateau.

What is proved is conditional Dafny correctness under generated contracts, and what is measured is benchmark verification success. What stays trusted is the specification-generation process, reference solutions, test selection, LLM judge, Dafny/Boogie/Z3 implementation, and benchmark scoring. Inference: the paper does not measure semantic agreement with a human’s original intent beyond its test-derived checks. The abstract’s 2.7K programs and 19K examples are roundings of 2,751 and 19,385. The paper has one internal slip: Table 1 lists 14.19% for NL-to-Spec (5,225 of 19,385 is 26.95%). Figure 6’s success samples (4,417) exceed 2,751; the paper does not say why, and several samples per problem would explain it (inference).

Inference: for VL, ATLAS is a high threat to any plan that relies on scarce hand-written verified Rust data: automated contract freezing, repair traces, and proof infilling can cheaply create training material. It is not evidence that an agent can safely specify an arbitrary production API. The direct product lesson is to make contract provenance, test coverage, proof dependencies, and trusted assumptions first-class fields in every training example. Existing work already addresses synthetic verified-code generation; VL should avoid rebuilding a Dafny-style pipeline without adding Rust ownership, Verus-specific proof idioms, and checks for semantic intent.

techniques for the catalog

• frozen contract synthesis — generate and compiler-check a complete signature, preconditions, postconditions, and tests before implementation attempts
• pointwise soundness lemmas — instantiate each contract on known input-output examples and reject inconsistent specifications
• contradiction completeness lemmas — assume a different output and prove false to test uniqueness of a specified result
• perturbation completeness checks — mutate outputs while fixing inputs and detect postconditions that accept wrong behavior
• adherence validation — require unchanged preconditions, preserved postconditions, whole-program verification, and passing tests
• verification-run curriculum — decompose successful and failed runs into specification, code, repair, and proof-infilling training tasks

study status

This study was written from the full extracted text of the ATLAS PDF and is ready for the complete gate.

Last edited: 2026-10-13