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.