The Design of an Interactive Proof Mode for Dafny
Logic in Computer Science
2025-12-24 v1
Abstract
We propose to extend the Dafny system with an interactive proof mode. We present a motivating example, how the IPM works, including the main design choices we make, and a prototype implementation.
Cite
@article{arxiv.2512.20486,
title = {The Design of an Interactive Proof Mode for Dafny},
author = {Ştefan Ciobâcă and K. Rustan M. Leino and Ştefan-Alexandru Mercaş and Roxana-Mihaela Timon},
journal= {arXiv preprint arXiv:2512.20486},
year = {2025}
}