In this tutorial you will learn how to use the Iris concurrent separation logic framework in Coq to verify message-passing programs. We will start with the basics of Iris to verify functional correctness of stateful programs using Hoare-style specifications. You will then learn how to implement a simple library for message-passing, and verify the library with respect to high-level specifications based on so-called “dependent separation protocols”, inspired by dependent session types, first introduced in the Actris framework in Iris. Finally, you will learn how to use the high-level specifications to verify message-passing programs.

For Coq exercises see: https://gitlab.mpi-sws.org/iris/tutorial-popl24