wal.sh
home > events > popl26 > dafny-2026 · Jun 09, 2026
dafnypoplauto-active verificationformal methodstransducersteaching

Dafny 2026 @ POPL — Auto-Active Verification

Table of Contents

The Dafny 2026 workshop (POPL 2026, Sun 11 Jan, Brussels) is a forum for auto-active program verifiers — languages with native specifications and an automatic static verifier: Dafny, SPARK, F*, Why3, Viper, Whiley, and auto-active tools for C, Java, Rust.

1. Program (Sun 11 Jan, Horizons)

Time Session / talk
09:12 Keynote — Software Verification meets Real-World Cryptography, Karthikeyan Bhargavan (Cryspen)
10:12 The Design of an Interactive Proof Mode for Dafny (Ciobâcă, Leino, …)
11:00 Development of Auto-Active Verifiers — probabilistic diagnostics; abstraction barriers; SPARK proof context; tunable automation; Velvet (effectful)
14:00 Applications & Lessons Learned — a verifier in Lean; minimax; Teaching Automata Theory and Formal Languages with Dafny (Ettinger); e-voting; railway data
16:00 LLMs in Auto-Active Verification — ATLAS; vericoding benchmark; DafnyPro; MiniF2F-Dafny; arithmetic-error repair; contamination-free benchmarks

Topic list spans SMT automation, IDE/UX, logical foundations, industry-scale verification, translation to/from the language, and verification in teaching.

2. Companion lab: reversible codec transducers

Following the workshop's verification-in-teaching thread (and next to Ettinger's automata-teaching talk), I built a small Dafny lab: jwalsh/dafny2026-reversible-transducers.

A codec chain from the reversible-pipeline work is a finite-state transducer. Three results, all discharged by Dafny 4.11 / Z3 4.15 (8 lemmas, 0 errors):

  • reverse ∘ reverse = id — over an alphabet type parameter T.
  • Caesar shift round-trip + rot13 as the n=13 involution (and caesar:26 = caesar:0 = id by % 26).
  • a chain of reversible codecs is reversible, decoders composing in reverse order — the tool's reverse-pipeline as a theorem.

The teaching payload: the UTF-16-vs-code-point bug for reverse is the choice of the alphabet type, which Dafny forces you to name — the bug class becomes a refinement boundary, not a footnote. Same boundary as the spec gap filed against the Rust/WASM reimplementation of the tool.

See also: Reversible Pipeline Transforms and the FST feasibility note in docs/transform-tool-automata.org.