Foundations for Formally Verified Network Protocol Parsers in Lean 4: A Case Study with MQTT

A significant portion of the Internet’s critical infrastructure relies on the precise implementation of network protocols, yet bridging the gap between formal verification and applied network engineering remains a challenge. In this paper, we present a case study in implementing and formally verifying a parser for the MQTT 5.0 protocol using Lean 4. Our approach includes three components: (I) correct-by-construction modeling of the packet format, leveraging dependent types to preclude invalid packets and encode data-dependent structural variations; (II) a layered, proof-carrying parser library utilizing state monads to process inputs whose exact layout depends on runtime parsed values; and (III) formal verification of parser completeness (roundtrip) and soundness (reconstruction) with respect to a serializer. Ultimately, this work serves as a foundational step toward a generalized, embedded domain-specific language for generating verified network protocol parsers.