I am not denying it, nor am I claiming that "just move to Rust" is an universal escape hatch.

What I am saying is that if it were as simple as "just learn CBMC" then maybe Microsoft and Google would have not published their studies demonstrating that 60% - 75% of all CVEs are memory safety errors like buffer under-/over-flows.

These studies aren't wrong. But, that's also because neither Microsoft nor Google make use of practical formal methods in practice. Both have research teams and pie-in-the-sky projects, not dissimilar to this DARPA project. But, when it comes down to the nitty-gritty development cycle, both companies use decades old software development practices.