Formal proofs for the paper, written in the Coq proof assistent. The artifact includes the source code for the proofs, along with a VM image with the sources and Coq 8.16.1 installed (which is the only dependency). Further instructions and details included in the README files.