It looks like Microsoft’s does the translation, so the only risk is bugs in the code generator, which seems nice.
There’s also Google’s wuffs, but I don’t think that is formal, it just ensures memory safety.
What it does not mean is that the program is bug free. That would, of course, violate the halting problem, or its generalization Rice's Theorem - non-trivial programs can not have arbitrary properties proven about them.
There's also Gödel's Incompleteness Theorem, obviously, as well as the fact that a proof is only as good as its model.
Even formal verification can be insufficient.
funny enough, much like rust, one of its most widely-deployed applications lives in firefox; see project-everest.github.io
All automagic, can’t see how it could get much simpler than that.