We introduce a methodology of Network-centricCompositional Testing (NCT) to develop formal wire specificationsof Internet protocols and to test protocol implementations forcompliance to a common standard. We use formal specificationsto generate automated testers for implementations of the protocol, based on randomized constraint solving using an SMTsolver. This makes it possible to resolve ambiguities in informalstandards documents using knowledge inherent in the implementations, while at the same time testing the implementations forcompliance to the developing formal specification. Because thetesting is compositional, it allows us to detect cases when thespecification is either too weak or too strong, and to refinethe specification accordingly. We apply the methodology toQUIC, a new Internet secure transport protocol currently in theprocess of IETF standardization and intended as a replacementfor the TLS/TCP stack and a foundation for HTTP/3. In theprocess of specifying QUIC, we discovered numerous errors inimplementations, as well as issues in the standard itself. Theseinclude an off-path denial of service attack and an informationleak similar to the “heartbleed” vulnerability in OpenSSL. Thepaper describes the formal foundations of the methodology, andsummarizes its specific application to QUIC.