1. 6
  1.  

  2. 2

    Github:

    https://github.com/project-everest/vale

    Prior work from Microsoft Research on verifying assembly involves both separation logic and Coq:

    https://www.microsoft.com/en-us/research/publication/high-level-separation-logic-low-level-code/

    https://www.microsoft.com/en-us/research/publication/coq-worlds-best-macro-assembler/

    It’s good that this project is on Github, though, as I didn’t see code releases for the others when I got those links.