> 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.
Specifically, seL4 formal verification took multiple (5+?) years by computer science PhDs treating it as novel research. And it's less than 50k lines of code total (might have actually been around 20k, if I remember correctly?), excluding the proof, with no dependencies at all outside the CPU.
Now look at Linux, or at Angular, or at any other piece of code you actually care about, and you'll see that even if we assumed simple linear scaling (which is obviously not a safe assumption as complexity increases rapidly with size), and even if LLMs can 10x the productivity, you'd still need decades or a team of dozens or hundreds of PhDs.
And also consider how much of that effort would have had to be redone when Linux added io_uring, for example.
The biggest hurdle is probably the number of bugs in most code. Verification would mean fixing all of those as well.