AxDafny: Agentic Verified Code Generation in Dafny

Sign up for free to create and run prompts on this paper using GPT-5.

What is this paper about?

This paper is about teaching AI to write programs that are not only correct but also come with a “proof” that they are correct. The team uses a language called Dafny, which lets you write both code and its rules (like a contract). Their system, called AxDafny, works like a careful student: it writes code, checks it with a strict checker, reads the error messages, and fixes the code and the proof steps over several tries. They also built a new set of problems, LCB-Pro-Dafny, to test how well such systems can create both working code and solid proofs.

What questions did the researchers ask?

They focused on two simple questions:

• Can an AI agent do better at writing verified code if it gets detailed feedback from a verifier and uses that feedback to repair its work step by step?
• How well does this approach work on different kinds of tasks: (1) filling in missing proof hints for already-written programs, and (2) writing whole programs (plus proofs) from a problem description?

How did they do it?

Think of an AI coder playing a game with three moves: try, check, repair.

• “Try”: The AI writes a complete Dafny solution (the code plus the proof notes it needs).
• “Check”: A verifier (like a super picky math teacher) checks every promise the code makes. If something is wrong or missing—like a loop rule (“invariant”) or a reason the program stops (“termination argument”)—the verifier points out exactly where and why.
• “Repair”: The AI reads that feedback and fixes the code and the proof parts, over and over, up to 20 tries.

They also make sure the AI can’t “cheat” by weakening the rules or turning off checks.

A quick translation of Dafny ideas

• Preconditions and postconditions: Before-and-after promises. For example, “input must be nonnegative” (pre) and “the result equals the sum from 0 to n” (post).
• Invariants: Facts that must stay true each time a loop runs (like keeping track that the part you’ve already processed is sorted).
• Assertions: Local mini-claims the verifier must check where they appear.
• Termination arguments: Proof that your loops/recursions eventually stop.
• Counterexamples: When a promise fails, Dafny can sometimes show a concrete example of why.

The agent’s parts

• Proposer: Writes the Dafny file (code + proof notes).
• Reviewer system:
  • Automatic checks prevent cheating (don’t weaken the original spec, don’t use shortcuts like “assume” or “verify false”).
  • The Dafny verifier runs and returns precise error messages.
  • A second AI reviewer looks for trickier cheating (like redefining a rule to always be true).
• Memory: The agent keeps notes about past mistakes and fixes so it can learn across tries.

What did they test on?

• DafnyBench: Existing programs with some proof hints removed; the task is to restore the missing hints so the verifier accepts the file.
• LCB-Pro-Dafny (their new benchmark): 250 competitive-programming style tasks translated into Dafny. Here, the agent must write the program and the proof from a problem statement and a formal specification.

What did they find, and why is it important?

• On DafnyBench (proof-hint filling):
  • AxDafny got 92.7% of tasks verified, beating the previous best reported system by 6.5 percentage points.
  • Most gains happened in the first few repair iterations—verifier feedback helped a lot, quickly.
• On LCB-Pro-Dafny (full program + proof writing):
  • AxDafny verified 56.4% overall.
  • Easy: 75%
  • Medium: 52%
  • Hard: 28%
  • A simple, one-shot baseline without the repair loop (just generate once) only got 11.6%. So iterating with verifier feedback made a big difference.
• Correctness vs. speed:
  • They also compiled the verified Dafny solutions to Python and ran the original test suites with time limits. Many verified solutions timed out instead of producing wrong answers.
  • This shows two different goals: (1) being mathematically correct (what Dafny checks), and (2) being fast enough for contest-style time limits. The current specs usually demand correctness, not speed, so some verified solutions were correct but slow.

Why this matters: It proves that using verifier feedback in a loop helps AI write provably correct code much more reliably than doing it in one shot. It also highlights that “proven correct” doesn’t automatically mean “fast enough,” which is important in real-world use.

What does this work mean for the future?

• Better reliability: If AI tools can routinely produce code with built-in proofs, everyday software could become safer and less buggy, especially for tricky edge cases.
• New challenges: We need:
  • Better specifications that also express efficiency goals (not just correctness).
  • Training and data for languages like Dafny (much rarer than Python), since data scarcity likely limits performance.
  • Smarter agents that can balance “easy to verify” with “fast to run.”
• Useful resources: The authors released their code and the new LCB-Pro-Dafny benchmark and harness, which can help the community build and test better verified coding agents.

In short, AxDafny shows that an “attempt, check, repair” approach guided by a verifier can strongly boost the creation of provably correct code. The next big step is making those verified programs efficient too, so they pass both the proof checker and the stopwatch.

Knowledge gaps, limitations, and open questions

Below is a single, concrete list of what remains missing, uncertain, or unexplored in the paper, framed to guide actionable follow-up research.

• Specifications lack resource guarantees: no formal constraints on time/space complexity are enforced, leading to many TLE/MLEs after compilation. How to express and verify asymptotic or constant-factor bounds in Dafny (e.g., via ghost cost models, amortized proofs, or contracts on data-structure operations), and train/evaluate agents to meet them?
• Runtime-performance–aware verification is not addressed: verified solutions often use slow Dafny runtime constructs (e.g., sets/maps) when compiled to Python. What is the effect of targeting other backends (C++, C#, Java), optimizing runtime libraries, or selecting data structures algorithmically during synthesis to hit time limits?
• Dependence on curated specifications: LCB-Pro-Dafny assumes fixed, trusted specs. How to automatically detect underspecification, vacuity, or misalignment with natural-language intent at scale (e.g., metamorphic checks, adversarial examples, relational specs, or independent checker ensembles), and quantify remaining spec defects beyond the reported spot checks?
• Limited vacuity safeguards: regex filters and an LLM reviewer may miss subtle proof-bypass patterns (e.g., strengthening preconditions, semantic rewrites of helper predicates, dead-code paths). Can we design sounder, verifier-level non-vacuity checks (e.g., caller preservation tests, pre/post equivalence constraints, mutation-based adversarial probes) with formal guarantees?
• Specification-preservation policy is non-uniform: DafnyBench uses a subset check on requires/ensures (allowing strengthened preconditions), whereas LCB-Pro-Dafny disallows modifying specs/definitions. What is the impact of different preservation policies on pass rates and cheating risk, and can we standardize an AST-level protection that prevents both weakening and undue strengthening?
• Component ablations are missing: the paper does not isolate contributions of (i) counterexample feedback, (ii) the LLM reviewer, (iii) static filters, (iv) the self-managed memory, and (v) iteration budget. Which components drive gains on proof vs. program synthesis, and how do they interact?
• Counterexample usage is under-specified: “when enabled” suggests inconsistent use. What is the causal effect of counterexample feedback on repair success, error localization, and iteration efficiency across difficulty splits?
• Error taxonomy is absent: there is no detailed analysis of why verification fails (e.g., missing loop invariants, incorrect specifications of helper methods, termination arguments, non-linear arithmetic, quantifier trigger issues). A fine-grained failure taxonomy could guide targeted prompt/agent designs.
• Generalization to modular, multi-method code is unclear: tasks appear largely single-method and algorithmic. How does the approach scale to modules, classes, data-structure invariants, and multi-function interprocedural specs?
• Scalability to larger codebases and longer proofs is untested: what happens to verification success and inference cost when proofs involve deeper lemma hierarchies, custom inductive datatypes, or heavy quantification?
• Training-data scarcity for Dafny is acknowledged but unaddressed: what is the effect of (i) targeted pretraining on Dafny corpora, (ii) translation-based augmentation from other verification ecosystems (F*, Why3, Coq/Lean to Dafny), or (iii) synthetic data generation of spec–implementation–proof triplets?
• Retrieval and library use are unexplored: AxDafny deliberately avoids proof-hint retrieval. Can task-agnostic retrieval (proof patterns, lemma libraries, spec templates) or structured tool-use (tactics for invariant inference, trigger synthesis) further boost performance without overfitting?
• Prompt and system design sensitivity is not reported: how do prompt templates, instruction granularity, chain-of-thought disclosure, and tool-calling strategies affect success and iteration counts?
• Compute/cost efficiency is unreported: there is no measurement of wall-clock time, tokens, or verifier calls per solved instance. What is the verification cost profile vs. pass rate, and how can we optimize it (e.g., early stopping, adaptive budgets, selective re-verification)?
• Backend semantics and portability are underexplored: Python compilation may introduce performance and semantic differences (e.g., runtime integer semantics, container implementations). What differences arise across backends, and can backend-aware synthesis reduce failures?
• Robustness across Dafny versions and solver configurations is not evaluated: specs emit quantifier-trigger warnings and solver behavior can vary. How stable are results under different Dafny/SMT versions, solver options, or timeouts?
• Termination-proof burden vs. efficiency trade-offs are not analyzed: do termination arguments steer models toward simpler but slower algorithms? Can we guide synthesis toward efficient structural recursion or well-founded measures without compromising verification ease?
• Benchmark scale and coverage are limited: 250 tasks may not cover diverse programming patterns (e.g., bit-level ops, floating-point, concurrency, I/O, probabilistic reasoning). How to expand LCB-Pro-Dafny with broader domains and difficulty gradients while maintaining high-spec quality?
• Contamination and provenance are not systematically audited: although curated, there is no formal contamination assessment against model training sets or code corpora. Can we provide reproducible data provenance and contamination audits?
• Lack of ground-truth reference implementations: relying solely on specs risks subtle omissions. Providing verified reference solutions could enable differential testing, performance baselines, and difficulty calibration.
• No direct comparison to other verification ecosystems: it is unknown how the approach transfers to F*, Why3, Coq, Lean, or Isabelle, and whether verifier-guided repair dynamics differ (e.g., tactic-based vs. SMT-based workflows).
• Limited study of invariant and trigger synthesis: quantifier triggers can make or break Dafny proofs, but automatic trigger/invariant suggestion and their effects on solver performance are not analyzed.
• Handling solver timeouts and non-termination: the agent’s behavior in the face of SMT timeouts is not discussed. Can adaptive strategies (e.g., lemma factoring, trigger tuning, constraint simplification) reduce solver non-termination?
• Alignment between NL problem statements and formal specs: despite curation, residual misalignments may persist. Can we create automated semantic conformance tests (e.g., using reference IO behaviors, NL-to-logic entailment checks) to certify that specs capture intended tasks?
• Evaluation under stochasticity is not characterized: reproducibility under different random seeds, sampling temperatures, or LLM versions is not reported. What variance should be expected, and how should benchmarks report it?
• Multi-objective optimization remains open: how to jointly optimize for verifier acceptance and runtime performance (e.g., Pareto-frontier training/evaluation, bi-criteria reward signals, or dual-objective repair loops)?
• Security aspects are unaddressed: can adversarial prompts or code cause solver blowups or denial-of-service during verification? What safeguards are needed for safe deployment in CI/CD?
• Human-in-the-loop strategies are unexplored: can minimal expert hints (e.g., invariant templates, complexity targets) dramatically reduce iteration counts or improve efficiency-constrained correctness?
• Memory module design is not ablated: the “self-managed, reflection memory” variant may or may not be essential. What memory size, summarization strategies, and retrieval policies optimize learning across iterations?
• Iteration-budget scaling laws are only partially studied: DafnyBench shows early-iteration gains; LCB-Pro-Dafny shows more sustained scaling. What are principled stopping criteria and budget allocations per instance?

Overview

This paper introduces AxDafny, an agentic, verifier-guided code generation framework for Dafny that iteratively synthesizes both implementations and accompanying proof artifacts (invariants, assertions, termination arguments). It also releases LCB-Pro-Dafny, a 250-task benchmark with formal specifications and a verifier-based harness. The system’s reviewer safeguards (spec-preservation checks and proof-bypass filters) and its demonstration that “verified correctness” is distinct from “runtime competitiveness” yield several practical applications across software, education, research, safety/compliance, and tooling.

Immediate Applications

• Spec-preserving verification gate in CI/CD (software, safety-critical industries)
  • Deploy a PR/commit gate that runs Dafny verification, rejects spec weakening, and blocks proof-bypass constructs; integrate counterexample feedback to guide fixes; optionally compile verified outputs to target languages (Python/Java/C++) for smoke tests.
  • Potential tools/workflows: PR bot for “verify-before-merge,” GitHub/GitLab action, buildkite step, verification badges on PRs.
  • Assumptions/dependencies: Team must author/own Dafny specifications for critical modules; modest onboarding to Dafny; LLM access/costs for iterative repair; acceptance that verification focuses on functional correctness, not performance.
• IDE assistant for proof and invariant synthesis (software engineering, education)
  • Use AxDafny’s iterative loop inside VS Code/JetBrains to propose loop invariants, assertions, and termination arguments with verifier feedback in place.
  • Potential tools/workflows: IDE extension with “verify and repair” button, inline diagnostics, quick-fix actions derived from verifier messages and counterexamples.
  • Assumptions/dependencies: Dafny tooling installed; base LLM availability; developer familiarity with specifications.
• Dual-track quality workflow: verify first, then test for performance (software QA/testing)
  • Adopt the paper’s two-tier evaluation: (1) Dafny verification for functional correctness; (2) compiled execution under unit/integration tests with time/memory limits. Use failure modes (TLE/MLE vs. wrong answer) as signals for algorithmic refactoring.
  • Potential tools/workflows: CI step that runs verification and a performance harness; dashboards categorizing failures by “functional” vs. “resource.”
  • Assumptions/dependencies: Benchmarks/time limits tuned to production SLOs; developers ready to rewrite for performance while maintaining proofs.
• Spec- and proof-bypass enforcement in code review (security, compliance)
  • Port the reviewer’s spec-preservation check and regex filters (assume, {:extern}, {:verify false}, {:axiom}) into static analysis and policy-as-code to prevent “cheating” changes and vacuous proofs.
  • Potential tools/workflows: Pre-commit hooks, linters, policy checks in CI, security gates for regulated code paths.
  • Assumptions/dependencies: Centralized policies; consistent Dafny versioning; exception handling for legitimate externs in legacy code.
• Formal verification in curriculum and autograding (education)
  • Use AxDafny to give granular feedback on student submissions (invariants/assertions/termination) and LCB-Pro-Dafny tasks for assignments/exams; auto-grade by “verifies under fixed spec.”
  • Potential tools/workflows: LMS plugins, assignment templates with fixed requires/ensures, leaderboard-based practice labs.
  • Assumptions/dependencies: Students have Dafny local/cloud environments; instructors review specs to ensure alignment with learning objectives.
• Benchmarking and model selection for code assistants (academia, AI vendors)
  • Use LCB-Pro-Dafny to evaluate LLMs on verified program synthesis; compare to runtime tests to understand capability gaps; support ablations and budget sensitivity studies.
  • Potential tools/workflows: Eval harness automation; regression dashboards across model versions; procurement criteria for enterprise AI coding tools.
  • Assumptions/dependencies: Access to models with iterative inference; compute budget; careful interpretation of “verified” vs. “runtime” metrics.
• Verified reference snippets for core algorithms (finance, healthcare, robotics, embedded)
  • Maintain a small internal library of verified building blocks (e.g., sorting, search, graph primitives) compiled to C++/Java for latency-sensitive services.
  • Potential tools/workflows: Internal package registry with proofs; change-management requiring re-verification upon updates.
  • Assumptions/dependencies: Coverage limited to well-specified primitives; performance audits needed; interop with existing codebases.
• Verified ETL/data pipeline contracts (data engineering)
  • Add requires/ensures to data transforms (e.g., schema invariants, aggregation identities), verify against Dafny, and compile wrappers for runtime use.
  • Potential tools/workflows: Contract checks for ingestion and transformations; CI gate for pipeline changes.
  • Assumptions/dependencies: Feasible to formalize invariants; may require stubs or models for external systems; not a substitute for data-quality monitoring.
• Hiring and upskilling using verified tasks (industry, academia)
  • Use curated LCB-Pro-Dafny tasks to assess candidates’ ability to write correct, provable code; run internal workshops on formal verification “in the loop.”
  • Potential tools/workflows: Interview platforms with verifier harness; internal guilds/practitioner playbooks.
  • Assumptions/dependencies: Fairness policies for candidate access to tools; scoped tasks reflecting job duties.
• Governance and audit-ready artifacts (policy/compliance)
  • Produce machine-checkable proof logs and spec-preservation evidence for internal/external audits of critical software changes.
  • Potential tools/workflows: Evidence capture in CI; audit trail of verifier output and reviewer decisions.
  • Assumptions/dependencies: Auditors accept formal verification artifacts; mapping between specs and higher-level requirements is maintained.

Long-Term Applications

• Complexity- and resource-aware verification (software performance, energy)
  • Extend specs with cost contracts (time/memory), amortized bounds, or cost models; integrate performance verification alongside functional proof.
  • Potential tools/products: “Complexity contracts” in Dafny; cost analyzers tied to verifier; energy-aware CI gates.
  • Assumptions/dependencies: Advances in cost-spec languages and automated bound checking; domain libraries with verified asymptotics.
• Cross-language, multi-verifier agent framework (software, embedded, safety-critical)
  • Generalize AxDafny’s architecture to Rust/Prusti, F*/KreMLin, Why3, SPARK Ada, Frama-C; unify reviewer safeguards and repair loops across verifiers.
  • Potential tools/products: Unified “VerifyBot” for polyglot repos; organization-wide formal DevOps pipelines.
  • Assumptions/dependencies: Stable verifier tooling/language coverage; consistent policies for spec-preservation across ecosystems.
• Specification mining and co-design (R&D, software)
  • Use LLMs to draft/repair specifications from natural language, code, and traces; stronger LLM-as-judge validation to detect incomplete or misaligned specs.
  • Potential tools/products: Spec recommender engines; spec-linting and mismatch diagnostics; human-in-the-loop spec workshops.
  • Assumptions/dependencies: Research on safe spec generation; datasets of high-quality specs; guardrails to avoid overtrust.
• Autonomous generation of verified microservices and controllers (cloud, robotics)
  • Agents synthesize provably correct components (APIs, data handlers, control loops) with contracts for safety/liveness; compile to C++/Rust for deployment.
  • Potential tools/products: “Verified service templates,” mission-critical controller libraries with guarantees.
  • Assumptions/dependencies: High-fidelity environment models and interfaces; compositional verification at system boundaries; performance guarantees.
• Smart contract and digital asset safety (finance, web3)
  • Apply verifier-guided repair to contract DSLs or to intermediate representations linked to on-chain bytecode; ensure safety properties (no reentrancy, invariant preservation).
  • Potential tools/products: Contract auditors’ copilots; CI gates for DeFi protocols.
  • Assumptions/dependencies: Bridges to formal tools in target ecosystems (e.g., Move, Vyper, K frameworks); faithful semantics.
• Regulatory-grade certification toolkits (medical, avionics, automotive)
  • Standardize verification evidence packages (specs, proof logs, counterexamples, change diffs) for certification submissions (FDA/FAA/ISO 26262).
  • Potential tools/products: “Verification dossier” generators; traceability from requirements → spec → proof → build artifact.
  • Assumptions/dependencies: Regulator acceptance of formal artifacts; qualified tools; process standards.
• Enterprise-scale formal DevOps (platform engineering)
  • Organization-wide policies for spec-first development; proof pattern libraries; provenance-aware memory modules that reuse verified lemmas across repos.
  • Potential tools/products: Proof-knowledge bases; cross-repo lemma retrieval; policy dashboards.
  • Assumptions/dependencies: Cultural adoption; investment in spec libraries; governance for proof reuse.
• Training LLMs with verifier rewards (AI systems)
  • Use verifier outcomes as learning signals (RL/fine-tuning) for models that natively produce code+proof; improve sample efficiency and robustness to distribution shift.
  • Potential tools/products: Self-play training pipelines on LCB-Pro-Dafny-like corpora; evaluation suites combining verification and runtime.
  • Assumptions/dependencies: Compute budgets; stable, scalable verifier APIs; contamination controls for benchmarks.
• Open-source safety bots and repositories (OSS governance)
  • Community bots that reject proof-bypass constructs and spec weakening; curated repositories of verified utilities for common tasks.
  • Potential tools/products: “Formal safety” GitHub apps; community-driven verified libraries.
  • Assumptions/dependencies: Maintainer buy-in; contributor tooling; license compatibility.
• Formal verification at scale in education and workforce development (education, policy)
  • Integrate verification literacy into standard CS/SE curricula; certification programs for “formal-ready” engineers; public-sector upskilling.
  • Potential tools/products: Courseware around AxDafny-style loops; national programs incentivizing formal methods in public software.
  • Assumptions/dependencies: Curriculum reform; accessible cloud workbenches; instructor training.

• Agentic code generation: An approach where an autonomous agent iteratively proposes, checks, and repairs code to meet goals or specifications. "We study agentic code generation in Dafny, where a model must generate both executable code and the proof artifacts for verification."
• Assertion: A proof annotation that asks the verifier to establish a specific fact at a program point. "Assertions ask Dafny to prove a local fact at a specific point in a program; for example, assert a[j] <= a[j+1] can expose an ordering fact needed to preserve the loop invariant or prove the final postcondition."
• Asymptotic complexity: A measure of how an algorithm’s resource usage grows with input size, typically expressed with Big-O notation. "We observe that most executable failures result from resource limits, because the Dafny specifications enforce functional correctness rather than asymptotic complexity."
• Counterexample: A concrete input that demonstrates a specification or proof obligation does not hold. "it can produce concrete counterexamples for certain failed verification conditions."
• Dafny: A programming language with integrated formal specification and automatic verification. "Dafny is a programming language with built-in support for formal verification \citep{leino2010dafny}."
• Evaluation harness: An automated framework that runs verification or tests to assess solutions consistently. "We also introduce LiveCodeBench-Pro-Dafny (LCB-Pro-Dafny), a benchmark of 250 competition-style programming problems translated into Dafny with formal specifications and a verifier-based evaluation harness."
• Formal verification: The use of mathematical methods and automated proof to establish program correctness against a specification. "Dafny is a programming language with built-in support for formal verification \citep{leino2010dafny}."
• Helper lemma: An auxiliary, named claim used to structure proofs and support verification of main results. "we also test a more permissive setting in which models may introduce helper lemmas and propositions in addition to proof annotations."
• Inference scaling: Improving performance by increasing the compute or iterative reasoning applied at inference time. "Inference scaling for coding agents often takes the form of an iterative generate--check--repair loop:"
• Invariant (loop invariant): A condition maintained to hold true at each iteration of a loop to support verification. "Loop invariants specify conditions that remain true across every iteration of a for or while loop;"
• Memory Limit Exceeded (MLE): A runtime failure where a program exceeds the allowed memory during execution. "4 fail by memory limit exceeded (MLE)."
• pass@1: The fraction of problems solved correctly by the first generated attempt without retries. "For DafnyBench, we compare with pass@1 model results and published proof-hint results using the original evaluation protocol, including DafnyBench, dafny-annotator, and DafnyPro \citep{loughridge2024dafnybench, poesia2024dafnyannotator,banerjee2026dafnypro}."
• Postcondition: A condition that must hold on method outputs upon normal termination. "A Dafny method can state assumptions about its inputs using requires and guarantees about its outputs using ensures; these are known as preconditions and postconditions, respectively."
• Precondition: A condition that must hold on method inputs before execution begins. "A Dafny method can state assumptions about its inputs using requires and guarantees about its outputs using ensures; these are known as preconditions and postconditions, respectively."
• Proof-bypass constructs: Language or annotation features that circumvent verification by assuming truths without proof. "Second, a regex filter rejects proof-bypass constructs: {:axiom} and {:verify false} for specifications, assume for asserting verification facts without proof, and {:extern} for declarations whose implementations are assumed to be verified externally."
• Proof hints: Annotations (e.g., asserts, invariants) that guide the verifier to discharge proof obligations. "DafnyBench evaluates LLM proof-hint generation with a basic iterative loop: the model proposes annotations, Dafny checks the file, and verifier errors are returned for repair \citep{loughridge2024dafnybench}."
• Proof obligations: The specific logical goals generated by the verifier that must be proven for the program to be accepted. "Dafny checks that the implementations satisfy these specifications using an SMT-based verifier, reporting failed proof obligations with source locations and diagnostic messages."
• Proof synthesis: The generation of proof annotations (e.g., invariants, asserts) needed to establish verification. "We therefore distinguish program synthesis, which generates executable Dafny code, from proof synthesis, which generates invariants, assertions, and other annotations needed to establish verification."
• Program synthesis: The automatic generation of executable code that satisfies a given specification. "We therefore distinguish program synthesis, which generates executable Dafny code, from proof synthesis, which generates invariants, assertions, and other annotations needed to establish verification."
• Quantifier-trigger warnings: Alerts from the verifier about patterns that may cause unreliable or inefficient quantifier instantiation. "Under Dafny's stricter default warning policy, 49 specifications emitted quantifier-trigger warnings, but otherwise parsed and type-resolved without errors."
• Reflection memory: An agent memory mechanism that summarizes and retains lessons across iterations to guide future attempts. "We use a self-managed, reflection memory variant as in \citep{requena2026minimalagentautomatedtheorem}, adapted to Dafny verifier output."
• SMT-based verifier: A verifier that reduces proof obligations to queries solved by Satisfiability Modulo Theories solvers. "Dafny checks that the implementations satisfy these specifications using an SMT-based verifier, reporting failed proof obligations with source locations and diagnostic messages."
• Specification weakening: Modifying a specification to make it easier to satisfy (e.g., by removing or loosening requirements). "This prevents specification weakening while still allowing new specifications for helper methods and lemmas."
• Termination arguments: Proof artifacts that show recursive calls or loops make progress and eventually terminate. "Finally, termination arguments show that recursive calls or loops make progress."
• Test harness: The external framework that supplies inputs and checks outputs to evaluate functional correctness. "A secondary evaluation compiles verified LCB-Pro-Dafny solutions to Python and executes them under the original LiveCodeBench-Pro test harness."
• Time Limit Exceeded (TLE): A runtime failure where a program exceeds the allowed execution time. "39 fail by time limit exceeded (TLE)"
• Vacuous proofs: “Proofs” that pass by assuming falsehood or disabling verification rather than establishing correctness. "A solution is accepted only when it verifies in Dafny and does not alter the requires or ensures clauses or rely on vacuous proofs such as assume false or {:verify false}."
• Verification conditions: Logical formulas derived from code and specifications whose validity implies correctness. "the --counterexamples flag can also provide concrete counterexamples for invalid verification conditions."
• Verifier-guided repair: An iterative process that uses verifier feedback to modify code and annotations until the program verifies. "We present AxDafny, a verifier-guided repair framework that iteratively generates implementations, invariants, assertions, and termination arguments."

Sign up for free to add this paper to one or more collections.