The repository contains the extended report of the ITP'21 paper
Verified Progress Tracking for Timely Dataflow
by Matthias Brun, Sára Decova, Andrea Lattuada, and Dmitriy Traytel. The report provides proof sketches for the safety
properties and additional details on the formalization (rep.pdf).
The Isabelle formalization described in the paper can be found in the Archive of Formal Proofs: