Comment by GianFabien

[seL4][1] is a formally verified microKernel which is used by billions of smartphones as part of their baseband OS. The part which is completely separate from Android or iOS. [1]:http://sel4.systems/