The paper KLAIM, Certified: Mechanising Flow Logic for Tuple-Space Coordination, by Marino Miculan, has been published (open access) in the Journal of Logical and Algebraic Methods in Programming (Elsevier).

The accompanying mechanisation in the Rocq proof assistant is available on Zenodo.