At Galois, we’re always looking for better ways to build reliable systems. A big part of that is doing our own research. At 130 people, we’re one of the world’s largest formal methods research teams! But another part of our work is understanding new tools and techniques from the research community. We’re interested in solving problems using any approach that works, including learning from other formal-methods researchers. Of course, it can be difficult to know how well a technique will work in practice from reading a research paper, so we often test new techniques out ourselves to learn more about them. One area that we’re very interested in at the moment is black-box testing of network protocol implementations. Two important examples are the ubiquitous TLS protocol and QUIC, a new transport-layer protocol under standardization at the IETF that will underlie HTTP/3. These protocols are critical for security but are notoriously difficult to get right, and implementations of TLS have often suffered from security vulnerabilities in the wild. To make matters worse, network protocols are inherently difficult to test because exercising a bug might require that several nodes play out a long sequence of interactions. Traditionally, protocol developers use interoperability testing, in which, e.g., a server running implementation A of QUIC is tested against a client running a different implementation B. By running the protocol between the two implementations, long sequences of complex interactions can be generated. This approach also provides a limited sort of adversarial testing, as implementation B might have interpreted the QUIC specification differently, resolved ambiguities differently, or might behave erroneously. The problem with this approach is that it is very hard to achieve a high coverage of the QUIC specification. Doing so depends on the implementation of B, the precise sequence of network operations, and other contingent factors. Testing erroneous behaviour is...