DafnyProver: Agentic Verified Code Generation in Dafny

Motivation

• Known: Dafny는 requires/ensures를 통한 명세와 SMT 기반 verifier를 내장한 언어로, invariant·assertion·termination argument 등의 proof annotation을 통해 formal verification을 지원하며, DafnyBench와 같은 벤치마크는 이미 존재하는 검증된 프로그램에서 proof annotation을 제거한 뒤 이를 복원하는 proof-hint synthesis 과제를 다뤄왔다.
• Gap: 기존 DafnyPro, DafnyBench 등의 시스템은 이미 주어진 구현과 명세에 대해 proof annotation만 복원하는 proof synthesis에 집중했고, proof-hint 라이브러리 검색 등에 의존했다. 또한 기존 Dafny 프로그램 합성 벤치마크(Dafny-synthesis, HumanEval-Dafny)는 규모가 작고 단순하며 데이터 오염 가능성이 있고 runtime 제약이 없어, 경쟁 프로그래밍 수준의 program synthesis와 proof synthesis를 함께 평가하기 어렵다.
• Why: Verification feedback은 단순 테스트케이스보다 훨씬 풍부한 신호(명세 위반, 누락된 proof annotation, 처리되지 않은 edge case 등)를 제공하므로, 이를 활용한 agentic code generation 연구는 inference scaling 및 formal methods를 실제 코드 생성 workflow에 통합하는 데 중요한 시사점을 준다.
• Approach: Verifier-guided repair를 수행하는 agentic 프레임워크 AxDafny(DafnyProver)를 제안하며, proposer-reviewer-memory 구조의 iterative generate-check-repair loop을 통해 구현체와 invariant, assertion, termination argument를 함께 생성하고, 이를 경쟁 프로그래밍 문제 250개로 구성된 새로운 LCB-Pro-Dafny 벤치마크와 기존 DafnyBench에서 평가한다.

Achievement

Figure 3. Cumulative AxDafny pass rate on LCB-Pro-Dafny across

1. DafnyBench 성능 향상: AxDafny(Gemini-3.1-Pro)가 DafnyBench에서 725/782(92.7%) 검증 성공률을 달성하여 기존 최강 proof-hint baseline 대비 6.5%p 향상시켰다.
2. 새 벤치마크 LCB-Pro-Dafny 구축: 250개의 경쟁 프로그래밍 스타일 문제를 formal specification과 함께 Dafny로 번역하고 verifier 기반 평가 harness를 구축하여 program synthesis와 proof synthesis를 동시에 평가할 수 있게 했다.
3. Baseline 대비 큰 폭 개선: LCB-Pro-Dafny에서 GPT-5.5의 direct generation 성공률 11.6% 대비 AxDafny는 56.4%의 검증 성공률을 기록했다.
4. Verification과 runtime test의 차이 규명: 검증된 LCB-Pro-Dafny 솔루션을 Python으로 컴파일해 원본 LiveCodeBench-Pro 테스트 하네스에서 실행한 결과, 대부분의 실행 실패가 자원 제한(resource limit)에서 기인함을 보여, verification success와 runtime test 성능이 서로 다른 코드 측면을 측정함을 입증했다.

How

Figure 2. Cumulative AxDafny pass rate on DafnyBench vs. itera-

• Requena et al. (2026)의 Lean proving용 agentic architecture를 Dafny로 적용하여 proposer agent, review system, memory module로 구성된 iterative refinement loop을 구성
• Proposer: 원본 파일 내용, target 이름, 이전 시도의 memory context를 받아 완전한 annotated Dafny file을 생성
• Reviewer system: (1) deterministic 단계 — requires/ensures 명세 보존 여부를 검사하는 static check와 {:axiom}, {:verify false}, assume, {:extern} 등 proof-bypass construct를 걸러내는 regex filter, 이후 dafny verify 실행으로 verifier diagnostics(미충족 precondition/postcondition/invariant/termination) 확보, 필요시 --counterexamples 플래그로 구체적 반례 제공; (2) LLM 기반 review — deterministic check로 잡히지 않는 cheating pattern(predicate를 trivial하게 재작성 등)을 검사
• Context management: Requena et al. (2026)의 self-managed reflection memory를 Dafny verifier 출력에 맞게 적용하여, 직전 시도의 reasoning/코드/피드백을 verbatim으로 포함하고, 별도 scratchpad call로 누적된 교훈을 압축한 rolling memory를 유지
• Gemini-3.1-Pro 또는 GPT-5.5(low/medium reasoning)을 base LLM으로 사용, 인스턴스당 최대 20회 iterative attempt 예산 부여
• DafnyBench(proof-hint synthesis)와 새로 구축한 LCB-Pro-Dafny(program+proof synthesis) 두 벤치마크에서 평가

Originality

• Proof synthesis만 다루던 기존 Dafny 시스템(DafnyBench, DafnyPro)과 달리 program synthesis와 proof synthesis를 joint하게 다루는 agentic framework를 제시
• Proof-hint 라이브러리 검색에 의존하지 않고 verifier feedback만으로 iterative repair를 수행하는 구조
• Lean proving을 위해 설계된 agentic architecture(proposer-reviewer-memory)를 Dafny 도메인에 최초로 적용
• 경쟁 프로그래밍 문제를 Dafny로 번역한 대규모(250개) 벤치마크 LCB-Pro-Dafny를 새로 구축하여 기존 소규모·단순 벤치마크(Dafny-synthesis 178개, HumanEval-Dafny 129개)의 한계를 보완
• Verification success와 runtime test 성능이 서로 다른 측면(functional correctness vs. asymptotic complexity/resource limit)을 측정한다는 점을 실증적으로 규명

Limitation & Further Study

• LCB-Pro-Dafny에서의 성공률(56.4%)이 여전히 낮아, 경쟁 프로그래밍 수준의 program synthesis+proof synthesis는 아직 미해결 과제로 남아있음
• Dafny 명세가 functional correctness만 강제하고 asymptotic complexity(자원 제약)를 명세화하지 않아, verified code라도 실제 runtime 제약(시간/메모리 제한)을 만족하지 못하는 경우가 많음 — 향후 resource-aware specification 및 검증 체계 필요
• Deterministic check(requires/ensures subset 검사, regex 기반 proof-bypass 탐지)와 LLM reviewer가 여전히 모든 형태의 cheating pattern(예: helper 명세 조작)을 완벽히 걸러낼 수 있는지에 대한 엄밀한 검증이 부족
• 실험이 소수의 특정 base LLM(Gemini-3.1-Pro, GPT-5.5)과 아직 공개되지 않은 최신 모델에 의존하여, 재현성과 일반화 가능성에 제약이 있을 수 있음
• iteration budget(20회)이 성능-비용 트레이드오프에 미치는 영향에 대한 심층 분석이 제한적

Evaluation

총평: Verifier-guided agentic repair를 통해 program synthesis와 proof synthesis를 통합적으로 다루고, 새로운 대규모 벤치마크와 함께 실증적 성능 개선을 보인 견실한 연구로, formal methods와 LLM 코드 생성의 결합 가능성을 잘 보여준다. 다만 경쟁 프로그래밍 수준의 자원 제약 문제는 여전히 해결되지 않은 채 남아 있어 향후 연구의 여지가 크다.