Dafny 2025
as the organisers put it
About Dafny is a verification-aware programming language that has native support for specifications and proofs, and is equipped with an auto-active static program verifier. The workshop aims to provide a platform for reports about applications of Dafny in industry, research on programming-language concepts that are relevant to Dafny, and talks about Dafny’s role in teaching. Topics include but are not limited to the following: Alternative verifier backends Coinduction and corecursion Comparison with other auto-active program verifiers (SPARK, F*, Why3, Viper, Whiley, …) Comparison with ot ...
| title | author | length |
|---|---|---|
| dafny-annotator: AI-Assisted Verification of Dafny Programs | Gabriel Poesia, Chloe Loughridge, Nada Amin | 23m |
Built a tool called dafny-annotator that uses LLMs plus greedy search (five iterations, five candidates) to insert invariants, decreases, and assertions into… | ||
| Towards Proof Stability in SMT-based Program Verification | Yi Zhou, Bryan Parno | 15m |
Paper and prototype work presents a mutation-driven detector Mariposa mutation-based detector and an SMT-level pruning algorithm that use Z3 proof-of-unsat and… | ||
| Teaching Types and Non-Interference in Dafny | Bryan Parno | 20m |
Teaching Types and Non-Interference in Dafny (Video, Dafny 2025)
Bryan Parno
(Carnegie Mellon University)
Abstract: We relate our approach to teaching a unit… | ||
| Dafny as Verification-Aware Intermediate Language for Code Generation | Yue Chen Li, Stefan Zetzsche, Siva Somayyajula | 15m |
Prototype guides an LLM to emit Dafny as opaque IR which is verified and then compiled to Python, preserving a proof and added unit tests. The system converges… | ||
| Shipwright: A Modular Framework for Verifying Liveness of Byzantine Fault Tolerant(…) | Derek Leung, Nickolai Zeldovich, M. Frans Kaashoek | 18m |
Shipwright is a Dafny framework that proves liveness of BFT systems by modular compositional refinement and novel completion measures. The project is ~12,000… | ||
| VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model,(…) | David Brandfonbrener, Simon Henniger, Sibi Raja, Tarun Prasad, Chloe Loughridge, Federico Cassano, Sabrina Ruixin Hu, Jianang Yang, William E. Byrd, Robert Zinkov, Nada Amin | 21m |
VerMCTS combines a logical verifier, an LLM (FinCode Llama v2), and a modified Monte Carlo Tree Search to synthesize Dafny and Coq programs and proofs; it… | ||
| Helping users to reduce Brittleness in their Dafny programs - a success story | Remy Willems, Matthias Schlaipfer, Olivier Bouissou | 21m |
Dafny adds three concrete features that cut proof brittleness: assertion isolation (split proofs into assertion batches), hide and reveal (exclude function… | ||
| Verifying the Fisher-Yates Shuffle Algorithm in Dafny | Stefan Zetzsche, Tancrède Lepoint, Jean-Baptiste Tristan, Mikaël Mayer | 18m |
Verified Fisher‑Yates implementation in Dafny defines a functional model on bitstreams, proves it yields each permutation with probability 1/n! for… | ||
| Well-Behaved (Co)algebraic Semantics of Regular Expressions in Dafny | Stefan Zetzsche, Wojciech Różowski | 19m |
Formalises that the denotational (language) and operational (deterministic automaton) semantics of regular expressions coincide, proving the inductive algebra… | ||
| Keynote | K. Rustan M. Leino | 01h 29m |
Dafny adds a boogie extractor that proves models for sets, sequences and multisets and emits Boogie axioms (it already caught a faulty multiset axiom), an… | ||
| Laurel: Unblocking Automated Verification with Large Language Models | Eric Mugnier, Emmanuel Anaya Gonzalez, Nadia Polikarpova, Ranjit Jhala, Zhou Yuanyuan | 18m |
Laurel uses large language models to auto-generate missing Dafny assertions and reports a >56.6% success rate on a new DafnyGym benchmark of lemmas extracted… | ||
| Lean on Dafny: Exploring Interactive Verification of Dafny Programs in Lean | Wojciech Różowski, Georges-Axel Jaloyan, Sean McLaughlin | 19m |
Extracts execution paths from Dafny into a tiny Boogie-like language, embeds a fragment of Dafny semantics into Lean, and implements a verified… | ||
| Baking for Dafny: A CakeML Backend for Dafny | Daniel Nezamabadi, Magnus O. Myreen | 18m |
A verified pipeline translates Dafny IR to CakeML by exporting the IR as S‑expressions, parsing and compiling inside HOL4, and extracting runnable CakeML code… | ||
| Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programming | Saikat Chakraborty, Gabriel Ebner, Siddharth Bhat, Sarah Fakhoury, Sakina Fatima, Shuvendu K. Lahiri, Nikhil Swamy | 21m |
Curated a reproducible dataset of about 600K lines and 32K top-level F definitions (extended to 940K lines and 54K defs) plus a program‑fragment checker that… | ||
| DafnyBench: A Benchmark for Formal Software Verification | Chloe Loughridge, Qinyi Sun, Seth Ahrenbach, Federico Cassano, Chuyue Sun, Ying Sheng, Anish Mudide, Md Rakib Hossain Misu, Nada Amin, Max Tegmark | 18m |
DafnyBench is a scraped benchmark of 750 programs and ~53,000 LOC that tests whether LLMs (GPT‑4, Claude 3, etc.) can auto-generate the missing Dafny… | ||
| Randomised Testing of the Dafny Compiler: Into the CI | Karnbongkot Boonriong, Alastair F. Donaldson, Stefan Zetzsche | 20m |
Integrates the fuzzer fuzz-d into Dafny’s CI as CompFuzzCI, running a brief per‑PR fuzzing campaign in containers, auto‑reducing and attempting bisection, and… | ||
| Performant, Readable and Interoperable Rust from Dafny | Mikaël Mayer, Shadaj Laddad, Fabio Madge, Siva Somayyajula, Jean-Baptiste Tristan | 17m |
A Dafny-to-Rust compiler that emits largely readable Rust code, uses a postprocessing pass to reuse local names and factor absolute paths into imports, and… | ||
| nothing matches | ||