Apple doesn't use sel4 in the secure enclave, but instead another l4 variant that isn't formally verified.

And they've made a lot of pretty deep changes for example adding native support for Mach-O files.