I will briefly explain how computers talk to each other via the Internet Protocol (IP), and explain the transport protocols UDP and TCP, and their interaction with ICMP (for error and control messages). UDP is the user datagram protocol, an unreliable packet-oriented protocol. TCP provides a reliable stream of data, and includes connection establishment, feature negotiation, window management, and teardown.
Over the last years at University of Cambridge I contributed to a formal model of TCP/IP and the Unix sockets API, developed in HOL4. We validated our HOL4 model with the FreeBSD-12 stack using Dtrace (packets, system calls, internal TCP state). In this research, we formalised a more exact TCP state machine than in initial RFCs or common literature (Stevens).