Correction: in Apple's case, the Secure Enclave, which runs L4, does not run on the application processor but on a separate ARM processor integrated on chip. Competitors tend to use TrustZone and hypervisor mode for this, but Apple currently uses them only for kernel patch protection rather than anything more important.
Not that that changes the core fact that Apple is shipping L4.
Not that that changes the core fact that Apple is shipping L4.