It is a question of responsibility. Whatever the language your SML runtime or compiler is written in (SML is a specification and an SML compiler does not have to stand on C code, it could be anything else), your responsibility is to make your SML program work according to the SML specification. If the SML compiler is buggy, that is someone else's problem.
Have you thought about the processor the compiled instructions for your SML runtime run on? Who formally proved that? And what about the electrons that move inside the processor's transistors? Who tells them to work according to the physics “laws” on which the processor's design was predicated? Who formally proved those laws?
It is not your problem.
This said, there is at the time of this writing a C compiler written essentially in Coq, CompCert. This compiler defines formal semantics for both the input language (most of C) and the target assembly languages. The input language does not have to be exactly C as long as an SML implementation is designed to work when compiled with this flavor of C. If you implemented SML in CompCert's input language, following the formal definition as closely as possible, you would have an SML interpreter with a chain of confidence that goes down nearly uninterrupted to assembly.