Compcert uses small-step operational semantics for both the source language and the assembly output (and intermediate languages that are irrelevant to the final statement of the semantic preservation theorem).
Specifying such a semantics is basically like writing a very simple functional interpreter for the language. I don't see how it could get much simpler. Here is the description of the semantics for their input language:
Yes. The approach is probably as good as it can get. And yet, it's not perfect. That functional interpreter could have a bug. And thus Knuth's quote is applicable. Testing the compiler could reveal to you that your specification wasn't really what you intended.
The semantics of the dialect of C that CompCert accepts are precisely defined, as are the semantics of the assembly outputted (that is, it's not strictly x86/PPC/ARM or whatever but some subset with defined semantics which happen to line up perfectly with observed behaviour). The first is fine I think (accepting a subset you define formally); the second is an issue but it's currently impossible to do any better. Still, if you look at this compared to the backends of LLVM and GCC it's certainly an improvement.
