Dafny 2026
as the organisers put it
About There is an established group of verification-aware programming languages that have native support for specifications and proofs, and are equipped with an auto-active static program verifier. Examples of such languages are Dafny, SPARK, F*, Why3, Viper, Whiley. Auto-active tools also exist for other languages like C, Java or Rust. The workshop aims to be a forum for all auto-active program verifiers and their related techniques. Topics include but are not limited to the following: AI for verification and vice versa Alternative verifier backends Coinduction and corecursion Comparison ...
who it's for
auto-active verification researchers, verification tool developers, program verification engineers, formal methods researchers, computer science educators, applied systems engineers
topics
LLM-guided theorem proving; LLM-assisted Dafny annotations; automated verified program synthesis; Dafny benchmark generation; interactive proof mode for Dafny; explicit abstraction barrier; verification of voting algorithms; verification of minimax with alpha-beta; Why3-based certified checkers; CVC5 and SMT integration
| title | author | length |
|---|---|---|
| Teaching Automata Theory and Formal Languages with Dafny | Ran Ettinger | 15m |
A second‑year automata course encodes textbook definitions in Dafny and produces a machine semantics formalized as a quintuple, a verified imperative simulator… | ||
| Velvet: A Multi-Modal Verifier for Effectful Programs | Vladimir Gladshtein, George Pîrlea, Qiyuan Zhao, Vitaly Kurin, Ilya Sergey | 19m |
Velvet is a Dafny-style verifier implemented as a Lean library that verifies imperative programs with mutable state, loops, and nondeterminism by generating… | ||
| A Correct-by-Construction Checker for Validation of Railway Data | Benoît Boyer, Noé Canva, Matteo Manighetti, Claude Marché | 19m |
A correct-by-construction checker is formally specified and implemented in Why3, extracted to OCaml and linked with non-verified I/O to produce an executable… | ||
| MiniF2F-Dafny: LLM-Guided Mathematical Theorem Proving via Auto-Active Verification | Mantas Bakšys, Stefan Zetzsche, Olivier Bouissou | 19m |
miniF2F gets fully translated into Dafny and a compact library of ~100 axiomatized lemmas, then run through Dafny’s SMT automation and 14 off‑the‑shelf LLMs… | ||
| Verification of E-Voting Algorithms in Dafny | Robert Büttner, Fabian Franz Dießl, Patrick Janoschek, Ivana Kostadinovic, Henrik Oback, Kilian Voß, Franziska Alber, Roland Herrmann, Sibylle Möhle, Philipp Rümmer | 14m |
A verified open-source library implements Score Voting, Instant-Runoff Voting, Borda Count, and Single Transferable Vote in Dafny, with 2,385 lines of code —… | ||
| DafnyPro: LLM-Assisted Automated Verification for Dafny Programs | Debangshu Banerjee, Olivier Bouissou, Stefan Zetzsche | 16m |
DafnyPro is an inference-time pipeline that uses LLMs (Claude Sonnet 3.5/3.7) to generate Dafny annotations while enforcing soundness with a diff-checker that… | ||
| Explicit Abstraction Barrier for Autoactive Verification | Paul Patault | 16m |
Coma is a small continuation‑passing intermediate verification language that implements an explicit abstraction barrier via a hide keyword and a modal VC… | ||
| ATLAS: Automated Toolkit for Large-Scale Verified Code Synthesis | Mantas Bakšys, Stefan Zetzsche, Olivier Bouissou, Soonho Kong, Remi Delmas | 16m |
ATLAS is an automated pipeline that converts Python contest problems into complete Dafny programs by generating a fixed method signature, synthesizing… | ||
| Toward Automated, Contamination-free Dafny Benchmark Generation | Changjie Wang, Mariano Scazzariello, Dejan Kostić, Marco Chiesa | 19m |
TACoDafny automates converting task descriptions (first 200 LeetCode problems) into Dafny programs plus contracts by prompting LMs to produce implementations… | ||
| Formal Verification of Minimax Algorithms | Wieger Wesselink, Kees Huizing, Huub van de Wetering | 17m |
Formal verification uses Dafny to prove correctness of negamax variants with alpha‑beta pruning, depth limits, and transposition tables; the key contribution… | ||
| Specification-Guided Repair of Arithmetic Errors in Dafny Programs using LLMs | Valentina Wu, Alexandra Mendes, Alexandre Abreu | 18m |
An automated repair pipeline for Dafny uses Hoare logic to localize arithmetic faults, prompts LLMs (GPT-4o mini, Llama 3, Mistral 7B, Llemma 7B) to synthesize… | ||
| The Design of an Interactive Proof Mode for Dafny | Ștefan Ciobâcă, K. Rustan M. Leino, Ștefan Mercaș, Roxana-Mihaela Timon | 18m |
Prototype interactive proof mode for Dafny that back-translates SMT-LIB VCs (generated via Boogie and Z3) into Dafny-like goals using injected protect_ helper… | ||
| A benchmark for vericoding: formally verified program synthesis | Sergiu Bursuc, Theodore Ehrenborg, Shaowei Lin, Lăcrămioara Aștefănoaei, Ionel Emilian Chiosa, Jure Kukovec, Alok Singh, Oliver Butterley, Adem Bizid, Quinn Dougherty, Miranda Zhao, Max Tan, Max Tegmark | 15m |
A public benchmark assembles roughly 10,000 tasks across Lean, Rust/Verus and Dafny (Lean ~4,000, Dafny ~800 after splitting/cleaning) and runs LLM prompting… | ||
| Lessons from Building an Auto-Active Verifier in Lean | George Pîrlea, Vladimir Gladshtein, Qiyuan Zhao, Ilya Sergey | 19m |
Veil is an auto‑active verifier implemented as a Lean library that does concrete and symbolic model checking, bounded searches, and inductive‑invariant… | ||
| Tunable Automation in Automated Program Verification | Alexander Bai, Chris Hawblitzel, Andrea Lattuada | 16m |
A Rust-based verifier (Verus) adds a broadcast lemmas mechanism to let libraries export grouped, universally quantified facts and users import them at module… | ||
| Software Verification meets Real-World Cryptography | Karthikeyan Bhargavan | 01h 04m |
Verified cryptography is now practical: about a dozen verified libraries exist and verified code runs in Firefox and on major cloud services, produced from… | ||
| nothing matches | ||