For a look at the underlying libraries, read the follow-up "A Formally Verified NAT Stack", which includes DPDK (the kernel-bypass framework used by the NAT) an

For a look at the underlying libraries, read the follow-up "A Formally Verified NAT Stack", which includes DPDK (the kernel-bypass framework used by the NAT) and its network card driver in the verification. In fact, my plane is about to take off for Budapest, where I'll be presenting that work, as I type this. :-) Paper link: http://dslab.epfl.ch/pubs/formally-verified-nat-stack.pdf http://dslab.epfl.ch/pubs/formally-verified-nat-stack.pdf