Given your experience in the area, I highly encourage you to get the 30 day free trial and evaluate Astree yourself. You should be better positioned than I am to assess their claim of zero false negatives in all of the classes of issues that its creators claim that it can detect, which to my eye, appears to cover a superset of what is typically considered under memory safety. I very much look forward to the result of your effort. Given its use by Boeing and the ESA to prevent runtime errors in C/C++ code, I would be surprised if it failed your scrutiny.

Astree uses the theory of abstract interpretation that most of those in the formal methods community publishing papers do not touch as far as I know. It is therefore a different kind of tool for verifying properties of code than the techniques put forth in most formal methods papers.

NIST evaluated Astree and it got a perfect score on their test suite. It was actually a better than perfect score, as it found flaws in the test suite that NIST had not known existed. I have not heard of runtime errors in the Astree verified C/C++ code running on Boeing airliners or ESA space probes, unlike the prominent Toyota issues where they did not use any such tools and their slogan “always moving forward” became literal. So far, those who can afford it seem to be avoiding runtime issues in C/C++ code, which would be impossible if it did not work as advertised.

I acknowledge that correctness by external observation is not airtight logic. However, substantially similar reasoning applies to the security of RSA, since the RSA hardness assumption is an assumption and not a verifiable proof. A key difference is that with Astree, a claim is made that the software can make proofs internally to justify its claims, but we can scrutinize neither the proofs nor its source code. I choose to believe claims about Astree until they are proven otherwise given that Astree appears to be preventing runtime errors in a great number of mission critical applications and the independent NIST review found no flaws in its ability to statically detect sources of runtime errors.