Thanks to @NGIZero @nlnet, we have funding work on μTCP, our TCP/IP stack for #MirageOS / #mkernel #OCaml #unikernels https://nlnet.nl/project/microTCP/ .

The longer story is this project I first heard about in 2012 at ICFP in Copenhagen where @peter_sewell_ gave an impressive talk "Tales from the Jungle". I was at that moment doing my PhD on software verification (Coq, separation logic) and it was so nice to see real world stories of verification.

For several reasons (MirageOS melting pot, OCaml-TLS with David Kaloper), I went to Cambridge and worked with Peter on that formal model, read our JFP journal paper http://www.cl.cam.ac.uk/~pes20/Netsem/paper3.pdf .

Then I left academia, and worked in my spare time (finding projects, going through team processes, ...) on the OCaml implementation very slowly. Motivated by @dinosaure and @reynir we deployed it in 2024, and fixed issues. Now we have several months of funded work to push it over the finish line.

Big thanks to everyone involved so we can push this forward. 🎉💕