That&#x27;s the exact one I thought of. On top of it, there&#x27;s typed assembler:<p><a href="https:&#x2F;&#x2F;www.cs.cornell.edu&#x2F;talc&#x2F;" rel="nofollow">https:&#x2F;&#x2F;www.cs.cornell.edu&#x2F;talc&#x2F;</a><p>And Vx86 used in Microsoft hypervisor:<p><a href="http:&#x2F;&#x2F;swt.informatik.uni-freiburg.de&#x2F;staff&#x2F;maus&#x2F;dissemain.pdf" rel="nofollow">http:&#x2F;&#x2F;swt.informatik.uni-freiburg.de&#x2F;staff&#x2F;maus&#x2F;dissemain.p...</a><p>Note: Microsoft also used a TAL, though can&#x27;t recall if same as Cornell, in their VerveOS that was verified down to assembler. Combined with SLAM, it&#x27;s safe to say their researchers are kicking serious behind on practical, cutting-edge verification. I wouldn&#x27;t have believed it 10+ years ago if someone told me haha.