This repository contains the Coq/Iris proofs that accompany the paper Spy game---Verifying a local generic solver in Iris