https://www.absint.com/astree/index.htm
You can use it to produce code that is semi-formally verified to be safe, with no need for extensions. It is used in the aviation and nuclear industries. Given that it is used only by industries where reliability is so important that money is no object, I never bothered to ask them how much it costs. Few people outside of those industries knows that it exists. It is a shame that the open source alternatives only support subsets of what it supports. The computing industry is largely focused on unsound approaches that are easier to do, but do not catch all issues.
If you want extensions, here is a version of C that relies on hardware features to detect pointer dereferences to the wrong places through capabilities:
https://github.com/CTSRD-CHERI/cheri-c-programming
It requires special CHERI hardware, although the hardware does exist.