Author here: I tried to capture networking on a conceptual level, not an implementation level. The idea is to describe the network as a graph of idealized processes and switches. If every message trace that is valid for the model is valid for the actual Kubernetes Network, the model and the network are trace compatible, therefore any true statement about the model is a true statement about the actual network. So far I have gotten some positive feedback, especially from non-network engineers, and some negative feedback, especially from network engineers. Let me know what you think.