I just did it Orange Book B3/A1 style by visual, result, and trace-based correspondence between code and executable specifications. Plus lots of FSM's. Next project I'd add Frama-C and Astree for code-level verification. Plus, CompCert for compilation with more result & trace-based simulation for correspondence.

Good to see new work, though. I follow Galois' stuff a lot because they're very innovative and practical. Harden et al are also using LLVM simulations for correctness but with ACL2.