The focus of this particular project is to verify transformations that work on the LLVM intermediate language. So there is only one interpreter, for the LLVM assembly. This could be used e.g. to prove the correctness of compiler optimization passes.
Of course, the same LLVM semantics could also be used if someone wanted to verify a compiler backend that generates low-level assembly (similar to what CompCert does), but I haven't heard if anyone has any concrete plans to do that. Rather than verifying a complete a new back-end, it would probably be quicker to write verified translations between the CompCert intermediate language and LLVM, and slot in the Vellvm verified transformations as an extra pass in CompCert.
Of course, the same LLVM semantics could also be used if someone wanted to verify a compiler backend that generates low-level assembly (similar to what CompCert does), but I haven't heard if anyone has any concrete plans to do that. Rather than verifying a complete a new back-end, it would probably be quicker to write verified translations between the CompCert intermediate language and LLVM, and slot in the Vellvm verified transformations as an extra pass in CompCert.