I just did it Orange Book B3&#x2F;A1 style by visual, result, and trace-based correspondence between code and executable specifications. Plus lots of FSM&#x27;s. Next project I&#x27;d add Frama-C and Astree for code-level verification. Plus, CompCert for compilation with more result &amp; trace-based simulation for correspondence.<p>Good to see new work, though. I follow Galois&#x27; stuff a lot because they&#x27;re very innovative and practical. Harden et al are also using LLVM simulations for correctness but with ACL2.