That's the exact one I thought of. On top of it, there's typed assembler:

https://www.cs.cornell.edu/talc/

And Vx86 used in Microsoft hypervisor:

http://swt.informatik.uni-freiburg.de/staff/maus/dissemain.p...

Note: Microsoft also used a TAL, though can't recall if same as Cornell, in their VerveOS that was verified down to assembler. Combined with SLAM, it's safe to say their researchers are kicking serious behind on practical, cutting-edge verification. I wouldn't have believed it 10+ years ago if someone told me haha.