I was under the impression that SeL4 exists.
From a quick google, seL4 has around 10,000 lines of C code, whereas the Linux kernel has around 30,000,000.
I think CSIRO disbanding the team was a huge mistake, but in any case they weren't producing the kind of success metrics that sustained their funding.