I feel this would be a good place to use a spark-based TCP stack. You're bypassing the kernel, have to run stuff as root or risky CAP_ rights, your stack should

I feel this would be a good place to use a spark-based TCP stack. You're bypassing the kernel, have to run stuff as root or risky CAP_ rights, your stack should be as solid as possible. https://www.adacore.com/papers/layered-formal-verification-of-a-tcp-stack https://www.adacore.com/papers/layered-formal-verification-o... Might also give people here some ideas on how to combine symbolic execution, proof, C and SPARK code and how to gain confidence in each part of a network stack. I think there's even some ongoing work climbing up the stack up to HTTP but not sure of the plan (not involved).