Wikipedia says:

> Apple A series processors beginning with the A7 contain a Secure Enclave coprocessor running an L4 operating system called sepOS (Secure Enclave Processor OS) based on the L4-embedded kernel developed at NICTA in 2006.

Are you sure that sepOS was formally verified? seL4, also from NICTA, was formally verified, but I don't think L4-embedded or sepOS were.