Yeah, CompCert will certify a binary for those willing to buy it or use a GPL license. Empirical testing showed it had no bugs in its middle end, unlike other compiler.
On Astree, I couldn't believe it supported all language constructs. I found this on your link:
"and is subject to the same restrictions as Astrée for C.
The high-level abstraction features and template library of C++ facilitate the design of very complex and dynamic software. Extensive use of these features may violate the established principles of safety-critical embedded software development and lead to unsatisfactory analysis times and results. The Astrée manual gives recommendations on the use of C++ features to ensure that the code can be well analyzed. For less constrained (less critical) C++ code, we recommend using the standalone RuleChecker."
So, it still does require a language subset that reduces complexity to benefit from the full analysis. They have greatly expanded what errors they catch since I first read about them. So, thanks for the link.
https://www.absint.com/astree/index.htm
By the way, C has a formally verified C compiler:
https://compcert.org/compcert-C.html