[pron]

When you want to verify functional properties these tools are not easy to use. For safety, they are easier than a rewrite and largely automatic. Large, sensitive codebases have been verified (for undefined behavior, not functional correctness) relatively quickly. In general, they cover more ground significantly more quickly and cheaply than a rewrite.