If you're looking for programs verified down to the machine code level, using C and the Verified Software Toolchain (VST) is one option. C programs are proven in the Hoare style (pre/postconditions) inside Coq, and then compiled using the verified CompCert compiler. Properties proven in Coq are guaranteed to hold about the compiled code.
There is nothing fundamental to prevent using VST to prove Verdi handler code correct, but the current runtime is not set up for that workflow.
There is nothing fundamental to prevent using VST to prove Verdi handler code correct, but the current runtime is not set up for that workflow.
http://vst.cs.princeton.edu