Proposal: verify Verdi shim functions down to machine code

[palmskog]

Several parts of the Verdi shims (currently based on OCaml) can be specified and verified down to machine code, for example using VST.

The current limitation is that there is no formal specification of UDP or TCP, which are used in the shims (all shims use TCP in some way).