Whereas the semantics of probabilistic languages has been extensively studied, specification languages for their properties have received less attention—with the notable exception of recent and on-going efforts by Joost-Pieter Katoen and collaborators. In this paper, we revisit probabilistic dynamic logic ( \(\texttt {pDL} \) ), a specification logic for programs in the probabilistic guarded command language ( \(\texttt {pGCL} \) ) of McIver and Morgan. Building on dynamic logic, \(\texttt {pDL} \)  can express both first-order state properties and probabilistic reachability properties. In this paper, we report on work in progress towards a deductive proof system for \(\texttt {pDL} \) . This proof system, in line with verification systems for dynamic logic such as KeY, is based on forward reasoning by means of symbolic execution.