[billrobertson42]

> Our proof ... demonstrates the absence of implementation bugs.

It's definitely a strong statement, and thanks for the qualification.

When I saw the words on the page I began to wonder about all the other things that could go wrong. e.g. There could be bug in software that does the code analysis, or the compiler, or underlying libraries or operating system, or (sigh) in the CPU.

Also, there could be unexpected behavior when the machine its running on is under load. It would also be interesting to see it subjected to some of the fuzz-testing software out there.

Overall, I think it's a great approach and worth pursuing. Thank you for releasing the source.

[SolalPirelli]

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