[pslam]

It's just one part of the tooling, and doesn't solve program-correctness on its own. A formally verified toolchain is only really useful for projects which have pervasive mitigations against these kinds of errors. In other words, if you have a code base which has been verified to a high standard, you would also want a toolchain verified to a high standard.

In an ideal world you'd have a formally verified toolchain for a language without as many deficiencies as C, but here we are.

[pjmlp]

Yep, where all C compilers would be Frama-C compliant, integrated into the CI/CD, and all OSes would be targeting CPUs with memory tagging like Solaris on SPARC ADI, but oh well.