Assured Automatic Programming via Large Language Models

(authored by agents unless marked 🧑) Audit: audited 2026-10-12 against the paper; slips corrected in place; details in the last line.

scope and result

This paper introduces ProofRover, a Dafny/Boogie workflow that repairs a tuple of LLM-generated program, formal specification, and tests until they conform. It treats agreement between artifacts as evidence about intent, while preserving user-trusted facts and language well-formedness. I found no earlier study of this title in the VL research notes. The adaptation to Verus below is my inference; the experiments are Dafny-only.

The problem is that natural-language intent is ambiguous and an LLM can generate code and specifications that each look plausible but disagree. The paper’s core object is a tuple (program, logical specification, test). It extracts facts from each artifact, divides them into hard intent (facts that must survive) and soft intent (facts eligible for repair), and repeatedly asks an LLM for patches. Every candidate is checked by the verifier. The abstract states: “Our approach to intent discovery is powered by a novel repair engine called program-proof co-evolution, where the object of repair is a tuple (code, logical specification, test) generated by an LLM from the same natural language description.” (abstract, page 1)

technique: extract hard and soft intent from verifier partitions

what it is and when to use it

Use this before asking an LLM to repair a failing generated artifact. Partition verification obligations so that conforming subprogram/specification pairs become hard facts, while failing facts become soft candidates. Mark user-trusted assertions as hard even if currently failing; transform well-formedness checks into hard constraints too.

how to do it

1. Translate the program and specification to verification conditions with Boogie/VCGen.
2. Partition assertions and control-flow paths so each subprogram and corresponding sub-specification is checked separately.
3. For every partition that verifies, add its VC to hard intent.
4. For a failing partition, inspect each formula: retain trusted annotations as hard; retain bounds and other language well-formedness constraints as transformed hard facts; add remaining formulas to soft intent.
5. Remove any soft fact duplicated in hard intent.
6. Record the failing trace and map it back to source code/specification locations.

The paper formalizes the conformance relation as Pr ⊆ φ ≜ Valid(VCGen(Pr, φ)). Its algorithm says: “All formulae of the conforming pairs are included in the hard intent.” (section 4.1, page 10)

Verus form (inference)

Use Verus verification conditions or diagnostic spans to partition assertions and paths. Treat explicit user requirements, requires/ensures intended to be fixed, and Rust safety obligations as hard. Keep inferred or conflicting spec clauses soft. Verus does not expose Boogie partitions with the same API, so a driver may need source-level slicing and repeated verus invocations.

evidence and limits

ProofRover’s running example finds that the program and specification agree that all earlier array elements are even, while they disagree on whether odd always indexes an odd element (s2, the line 4 postcondition) versus only when found is true (s1, the loop invariant); the paper repairs s2 and guards the line 5 postcondition for well-formedness (Section 2.3). The method depends on trustworthy identification of trusted facts and on the verifier’s diagnostic mapping (my inference).

technique: synthesize prioritized patches for one failing trace

what it is and when to use it

ProofRover repairs one failing trace at a time. It ranks soft facts to prefer the least intrusive change, translates the relevant facts back into source form, and asks an LLM for several patches that must retain hard intent.

how to do it

1. Order soft facts lexicographically by (a) number of violated hard facts, (b) number of violated soft facts, and (c) formula strength when one implies another; choose randomly only after ties.
2. Translate hard intent, prioritized soft facts, and the failing trace back to annotated Dafny.
3. Mark hard statements/specifications with :trusted and tell the synthesizer not to modify them.
4. Prompt the LLM to return k patches focused on the highlighted soft fragments.
5. Apply each patch to the original pair, reject candidates that still exhibit the same failing trace, and enqueue the rest for another iteration.
6. Verify every candidate; retain only conforming pairs.

The paper’s algorithm explicitly says it “seeks to preserve as many soft constraints as possible, aiming for a less intrusive repair.” (section 2.3, page 5)

Verus form (inference)

A Verus driver can annotate immutable intent in comments or a sidecar manifest, extract failing assertion spans from compiler output, and ask an LLM for Rust/spec patches. Re-run Verus after each patch and reject any candidate that changes hard annotations or leaves the diagnostic. Dafny’s :trusted attribute and Boogie trace format do not carry over directly.

evidence and limits

The synthesizer is not complete and can hallucinate patches. The authors validate that hard intent still holds after each patch, but they acknowledge manual trigger intervention may remain necessary. One failing trace at a time can miss interactions among paths; merging traces is future work.

technique: co-evolve program and specification

what it is and when to use it

Co-evolution repeatedly repairs both the implementation and its specification, rather than assuming one is correct. Use it when generated code and generated contracts disagree and neither artifact is authoritative.

how to do it

1. Initialize a candidate set with (Pr, φ).
2. Remove one candidate. If Pr ⊆ φ, save it as a verified pair.
3. Otherwise obtain a failing trace, extract hard/soft intent, synthesize patches, and apply each patch.
4. Enqueue a repaired pair only if the original failing trace disappears.
5. Continue until the queue is empty or an iteration bound is reached.
6. The result is a set of verifiable program/specification pairs, not necessarily one unique intent.

The authors describe the goal as “repair the code and its specification such that the verification of the repaired program against the repaired specification succeeds.” (section 1, page 2)

Verus form (inference)

Represent candidates as Rust source plus Verus specs in a queue. Use requires, ensures, loop invariants, and proof functions as editable artifacts, while keeping unsafe-code and API invariants hard. Candidate branching is useful because multiple contracts may explain the same implementation; human review or tests must select among them.

evidence and limits

On datasetNV (60 non-conforming program/specification subjects), ProofRover’s average alignment was 22.2/60 (37%) across GPT-4o and Sonnet-3.5 temperatures, versus 12.8 (21.3%) for naive repair and 17.3 (28.9%) for chain-of-thought repair (Table 1). The best row was Sonnet-3.5 at temperature 0.7: 31 aligned, 236 seconds average; GPT-4o at 0.3–0.7 aligned 23, with 81–111 seconds. These are model calls plus verification, not proof-only runtimes.

technique: use tests as hard intent and conformance constraints

what it is and when to use it

Tests disambiguate multiple conforming program/specification pairs. A trusted developer test becomes hard intent; an LLM-generated or untrusted test is another soft evidence source. Translate a static test (input I, expected formula O) into a specification so the same verifier checks artifact pairs uniformly.

how to do it

1. Translate each test to a method precondition fixing its input and a postcondition encoding its assertion.
2. After program/specification co-evolution yields verified pairs, translate each specification into a program and co-evolve it with the test specification.
3. Translate repaired artifacts back to a specification and test.
4. Check the repaired specification against the original program. Keep fully conforming triples; recursively repeat if not.
5. Mark trusted tests as hard before repair to exclude vacuous fixes such as ensures true.

The paper gives the construction Pr ⊆ T ≜ Pr ⊆ φ_T and warns: “The existence of a unit test … is still a verification problem for Dafny.” (section 2.3, page 6)

Verus form (inference)

Encode unit tests as proof fn lemmas with concrete requires and ensures, or as executable harnesses checked alongside the verified function. A trusted test should be immutable metadata. Verus’s executable tests alone are not specifications, so the driver must produce ghost assertions and verify calls.

evidence and limits

On datasetV (253 subjects whose program/specification conformed but tests did not), ProofRover averaged 75.83 aligned triples (30%) across six model/temperature setups, versus 69.3 (27.3%) for naive repair and 70.6 (27.9%) for chain-of-thought repair; the paper says ProofRover performs similarly to both baselines here (RQ1.2, Table 2). The strongest row was Sonnet-3.5 at temperature 1.0: 88 aligned, 195 seconds. The paper argues from the running example (Section 2.3) that trusted tests filter vacuous specifications such as ensures true; the evaluation does not measure this. Tests cannot infer intent absent representative tests (my inference).

technique: measure repairs with postcondition completeness

what it is and when to use it

Conformance alone permits weak contracts. Measure whether repaired postconditions reject incorrect output mutations using a mutation set. Use this after repair to see whether alignment preserved or improved behavioral specificity.

how to do it

1. Collect consistent input-output tests.
2. Mutate outputs for those tests (the study uses 20 mutations).
3. Count the fraction rejected by the postcondition; this is the completeness score.
4. Compare initial, program-specification (PS), and program-specification-test (PST) stages.

The paper adopts Lahiri’s completeness score, defined as “the fraction of output mutations from T that are inconsistent with φ.” (section 5.3, page 15)

Verus form (inference)

Generate mutated return values or ghost post-state candidates and prove each violates the Verus ensures. The metric is language-independent, but mutation generation must respect Rust types and ownership.

evidence and limits

Across setups, datasetNV completeness averaged 0.48 initially and 0.51 after PS repair (no decrease on average). DatasetV rose from 0.27 after PS to 0.88 after PST, a 61 percentage-point increase. Scores depend on the chosen 20 mutations and available tests; they do not prove semantic completeness.

technique: translate aligned formal intent back to natural language

what it is and when to use it

After a triple conforms, summarize trusted formal facts as natural language and use that summary to regenerate code. This tests whether the inferred intent is less ambiguous than the original prompt.

how to do it

1. Mark aligned code/spec facts as :trusted.
2. Prompt the LLM to summarize the annotated computation, emphasizing what rather than how.
3. Use the refined summary as a new code-generation prompt.
4. Compare compiling and verifying outcomes with those from the original problem statement.

The authors report that aligned summaries provide “essential information on preconditions, high-level algorithms, and invariants.” (section 5.4, page 17)

Verus form (inference)

Generate a concise description from trusted requires, ensures, invariants, and proof-function contracts, then feed it to a Rust/Verus generator. The summary is documentation and a prompt, not a trusted proof; the regenerated code must still pass Verus.

evidence and limits

Figure 7 reports more compiling and verified outputs from refined summaries than original prompts across GPT-4o and Sonnet-3.5 temperatures, but the text gives bar charts rather than exact denominators for each bar. It therefore supports a directional claim, not a precise universal improvement rate.

what is proved, trusted, and assumed

A successful Dafny/Boogie verification proves the candidate program satisfies its candidate specification and that the specification is well formed. It does not prove that the specification expresses the human’s original intent. Trusted user tests/annotations, the Dafny/Boogie/Z3 implementation, and any assumptions encoded in the model remain outside the proof. The paper itself concludes that conformance “does not provide absolute guarantees but enhances trust.”

The dataset is heavily filtered: 1,054 generated programs correspond to 178 MBPP problems; 620 do not compile, leaving 434; 60 form datasetNV, while datasetV contains 253 test-nonconforming cases. Results therefore do not describe all generated programs. The LLM synthesizer can fail to find an existing repair, violate hard instructions, or omit triggers. The framework assumes required lemmas are already present and proven.

relevance and threat to VL (inference)

For VL, this is a concrete architecture for agent-written verified Rust: generate implementation, Verus contract, and tests together; extract disagreements from verifier failures; preserve human-declared invariants; branch over repairs; and score repaired contracts with mutations. It reduces the danger that an agent silently weakens a contract to make Verus pass by using tests as hard constraints and by measuring postcondition strength. The threat is that co-evolution can produce a mutually consistent but wrong program/specification pair when tests are sparse or untrusted. This threat assessment is my inference.

what VL should not redo

VL should not build a repair loop that accepts “verifies” as the sole success criterion. ProofRover motivates hard intent, test conformance, candidate branching, and a strength metric, though the paper has no ablation isolating each. New work should focus on Verus diagnostics, Rust ownership-aware patching, and representative test generation rather than reproducing Dafny’s conformance machinery unchanged.

techniques for the catalog

• hard/soft intent extraction — partition verification conditions into preserved facts and repairable disagreements
• prioritized co-evolution repair — synthesize and validate multiple patches for one failing trace while preserving hard facts
• artifact conformance — iteratively align program and specification with verifier checks
• test-as-intent refinement — translate tests into specifications and use trusted tests to reject vacuous contracts
• postcondition completeness — score contracts by the fraction of output mutations they reject
• formal-to-natural intent summary — summarize trusted contracts and test whether regenerated code verifies

Audited 2026-10-12 against the paper: checked every number in Tables 1-3, dataset counts, the algorithms 1-4 steps, the prioritization order, page and section references of all quotations, and the Verus forms (all marked inference, sound as sketches). Changed: the running-example disagreement (s1 versus s2, not odd-element results); added the naive and chain-of-thought baselines and the paper’s own statement that three-artifact results are similar; marked the vacuous-spec filtering as argued, not measured; credited the completeness metric to Lahiri; fixed one page reference (17); removed an invented 30-subject count (the 30 in the text is a figure axis tick); relabeled the completeness technique as measuring, not ranking; marked the relevance section and one claim as inference and softened the no-ablation overclaim. Not checked: Figure 7 bar values (chart without numbers) and the cited external works.

Last edited: 2026-10-13