It's not going to work. Formally verified assembly needs a low level spec which is comparable in length to the assembly code, so not really comprehensible.

"higher level projections" - wtf is this even about?