This year, we published a #formalmethods paper "Engineering with Logic: Rigorous Test-Oracle Specification
and Validation for TCP/IP and the Sockets API" https://www.cl.cam.ac.uk/~pes20/Netsem/paper3.pdf in the Journal of the ACM! :) https://www.cl.cam.ac.uk/~pes20/rems/ #hol4 #tcpip #network so glad that this is finally out :D (happy to hear your thoughts on that, still working on a TCP/IP stack based on that work)
and now, thanks for nothing, I'm actually going through the specification (384 pages, typeset HOL4 code with lots of comments) and the source (there are more internal notes and comments) to come up with an actual implementation (in a pure functional subset of some programming language)... pretty interesting what my brain comes up in respect to things that are not needed (in certain environments -- such as "process of this socket no longer exists" -- which can't happen in a unikernel)... :D
@epicmorphism there is http://anil.recoil.org/papers/2013-asplos-mirage.pdf and also https://usenix15.nqsb.io on the TLS stack, and some more on jitsu, irmin, etc -- http://anil.recoil.org/papers/ lists them (http://unikernel.org/resources/ as well), but yep, nothing recent major...
Server run by the main developers of the project It is not focused on any particular niche interest - everyone is welcome as long as you follow our code of conduct!