It Takes a Village: Bridging the Gaps between Current and Formal Specifications for Protocols

Network protocols are fundamental to the functioning of modern society, as more and more services are provided online, including critical infrastructure. Historically, these services have mostly been implemented with wired networks that connect conventional computers. But with the emergence of wireless and cellular technologies, their reach has extended to Internet of Things (IoT) devices and sensors, robotic systems, and autonomous vehicles. The next generation of cellular technologies, often referred to as NextG, will further expand the set of services that can be delivered over a network, including real-time remote healthcare, industrial automation, precision agriculture, smart infrastructure, holographic communication, space-based communication, and more. Experience shows that formal specification can provide significant practical benefits for network protocol development by enhancing clarity, trustworthiness, and productivity. Adoption of formal methods has been hindered not by lack of scalability but by cultural gaps that result in tools and methods that do not align with engineering practice.