I found the code of the verifyer-in-the-middle! It’s here, in a codebase of the Ocean Observatories Initiative’s cyber infrastructure:
It took me some work to find this, the artefact link in the paper’s References section went to a Conflunce page that is both dead and not in Wayback. Thanks be to SciHub; without them I wouldn’t have been able to access the paper with a better link.
Side note 1: dr. Neykova and prof. Yoshida both have super interesting publication lists.
Side note 2: there is a recent (2018) talk The Do’s and Don’ts of Error Handling, by Joe Armstrong, that also mentions MITM protocol verifyers/enforcers. (Link goes directly to that bit, it runs for about 2 minutes). His argument runs ‘protocols are contracts; contracts assign blame, which encourages both parties to fulfil the contract. What is sent on the wire is rarely observed; a contract checker in the middle lets you know which component is out of spec’. The paper “How to Verify Your Python Conversations” is an (earlier!) practical instance of such a contract checker.
Further notes: this is not, in fact, a verifyer-in-the-middle, but something even cooler: local verifyers that are guaranteed to enforce global correctness.
The authors (Rumyana Neykova did the implementing in the OOI codebase; Nobuko Yoshida is a Very Important Researcher in the field of Multi-Party Session Types, calculus, and verification):