Proposal: verify Verdi handlers down to machine code for example system

[palmskog]

To push the boundaries for how verified distributed systems can be, we would like to use VST (to refine handlers to C) and CompCert to verify Verdi node handlers down to machine code level for some example system, and demonstrate that the system can be executed successfully. One reasonably simple system is Verdi Lockserv.