My paper KLAIM, Certified: Mechanising Flow Logic for Tuple-Space Coordination has been published (open access) in the Journal of Logical and Algebraic Methods in Programming (Elsevier). The accompanying Rocq mechanisation is available on Zenodo.