It seems to me that we should design for (formal) verification. Much like we should design for testability. But am noob, so what do I know?
That said, my quick search shows some academic efforts to formally verify QUIC, both in whole and in parts.
I would hope that bespoke (boutique?) TCP replacements, like Homa (specifically for datacenters), are verified as part of the design process. From a quick scan, I gleaned that Homa, and other aspirants, are simulated, compared, and benchmarked against each other. Maybe that's sufficient.
That said, my quick search shows some academic efforts to formally verify QUIC, both in whole and in parts.
I would hope that bespoke (boutique?) TCP replacements, like Homa (specifically for datacenters), are verified as part of the design process. From a quick scan, I gleaned that Homa, and other aspirants, are simulated, compared, and benchmarked against each other. Maybe that's sufficient.
https://homa-transport.atlassian.net/wiki/spaces/HOMA/overvi...