It's only Monday and that paper lead me to L3 and the UNSW course[1] notes. There goes my next weekend or four. Thanks, ya son of a gun ;)
Just throwing that out there for you or anyone interested in lengthening the chain of verification. VAMP doesn't get enough attention. On HW side, someone could do a verified front-end for RISC-V on top of the VAMP components to get a mostly-verified RISC-V. Lots of low-hanging fruit out there.