The paper “Verifying Sampling Algorithms via Distributional Invariants” by Daniel Zilken, Kevin Batz, Joost-Pueter Katoen and Tobias Winkler has won the Best Paper Award at the Formal Methods Symposium 2026 in Tokyo! 🎉🇯🇵.

Discrete samplers are to probabilistic computing what arithmetic is for classical programs — powering randomised algorithms, cryptography, AI planning, probabilistic inference, and simulation. But how to prove them correct? Exactly.

The key idea: treat probabilistic programs as distribution transformers and introduce inductive distributional loop invariants — an elegant and simple generalisation of classical loop invariants to the probabilistic setting, embedded in a Hoare-style verification framework. As a showcase, the paper formally proves the correctness of the Fast Dice Roller and Fast Loaded Dice Roller.