Hmm, good point. You'd have to extend the formal verification into the C code, at least. If you can do that, it might be easier to just write verified C.
Inline ASM is exactly as verifiable as the underlying CPU, given an adequate model in the verifier. That's probably easier than verifying C, which introduces extra ambiguity in its semantics. But yeah, verifiable CPUs would be nice.
