[0815test]

> Much cheaper and more realistic than a rewrite.

I really have to dispute this, these tools are not simple to use. You'll probably have a far easier time rewriting the code piecemeal, i.e. function-by-function (which will involve a lot of unsafety initially, since you're not using the idiomatic global patterns of a memory-safe language!) and then refactoring into something idiomatic for the language you're using. Projects like Firefox are basically taking a similar approach, only "rewriting" small portions of the codebase that can be deployed immediately once rewritten.

Where similar tools might be useful is for preventing logic-related issues that are not encompassed under simple memory safety. Unfortunately it's still not possible to endow, e.g. Rust code with automatically-checkable proofs, showing that the logic in the code preserves some appropriate conditions/invariants; while this is feasible, e.g. in Agda or Idris. Hopefully by the time these concerns become pressing, practical memory-safe languages will also offer this.

[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.