KLAIM, certified: Mechanising flow logic for tuple-space coordination

Control-flow analysis in the style of Flow Logic has long been a central tool in the Pisa school of language-based security: it provides an over-approximating static semantics whose soundness ensures that statically established security properties are preserved at run time. In this paper we revisit a representative instance of this programme, the static analysis of tuple trajectories in a language of the KLAIM family, and certify it in the Rocq proof assistant.We work with the located-network fragment on which the original trajectory analysis is defined: first-order tuple-space coordination over a finite, statically known set of localities, with no code mobility. For this fragment we mechanise the syntax, operational semantics and Flow Logic specification of the analysis using a locally nameless representation with multi-binders of statically varying arity. We then machine-check the main metatheoretic properties of the analysis: closure of acceptable estimates under meets, yielding a least acceptable estimate when one exists; subject reduction; and a trajectory-confinement theorem stating that sensitive data never reach forbidden sites whenever the static estimate excludes them.The mechanisation also exposes a methodological point that is easy to leave implicit on paper. The 0-CFA distinguishes binders by their canonical labels, and is therefore equivariant, rather than invariant, with respect to α-renaming: renaming binders preserves acceptability only when the abstract environment is renamed accordingly. Making this naming discipline explicit reconciles locally nameless binding with finitely supported abstract environments. Finally, acceptability is proved decidable, and the decision procedure is extracted to OCaml, yielding a certified checker for the analysed fragment.