Not true. seL4 (for example) is an example of a real time kernel proven correct end-to-end and used on millions of devices.

Another example is CompCert (a proven correct C compiler used by Airbus and others for real production software).