The paper “Diagnostics in Probabilistic Program Verification” by Philipp Schröer, Darion Haase, and Joost-Pieter Katoen has been accepted at the Dafny 2026 workshop. The paper focuses on effective user diagnostics generated during the deductive verification of probabilistic programs. It is based on providing different kinds of program slices for (1) error reporting, (2) proof simplification, and (3) preserving successful verification results.