Do you have some links about the known soundness issues? I was under the impression that although it hadn't yet been proven it was still a medium-term goal, and any soundness bugs were considered fairly major.

(And yeah, "mathematical proof" is strong regardless since e.g. LLVM is also in there somewhere. But it captures the idea more closely than any comparison of "compile vs. runtime" or "static vs. dynamic" does.)