In this tutorial, participants will learn how to use modern separation logic as developed in the Clutch project to verify quantitative properties of probabilistic programs in Rocq. We will present novel logical concepts introduced by the Clutch logic family—such as error credits, error amplification, and presampling tapes—that we believe to be of general interest for probabilistic program verification. These concepts can be used to capture and reason modularly about the probabilistic aspects of a program’s behavior. After a gentle conceptual introduction, participants will learn how to apply these new techniques to verify illustrative examples such as sampling algorithms and probabilistic data structures.

The tutorial will be interactive and we recommend that participants have pre-installed Rocq and Clutch following the instruction found on this link.

Note that the tutorial spans the 3 hours; it is not a 90 min tutorial twice repeated.