This is very, very, important. As the NICTA project notes:
…software systems are increasingly trusted with critical operations. Yet, the traditional ways in which they are engineered provide limited or no assurance that they are worthy of such trust: In general, no guarantees can be made for the security, safety or reliability of such devices. The implications are scary: these systems are becoming more and more complex, and thus error prone. At the same time, more and more trust is put on them. This is a time bomb of silently growing destructive power.
The Path to Trustworthy Software Systems
NICTA believes that this situation is far too dangerous to tolerate, and that fundamental change is both necessary and possible. Such change is exactly what the Trustworthy Systems project is aiming to achieve. The project takes a strategic approach to trustworthiness, by combining and integrating innovation in operating systems, systems architecture and formal methods. The outcome will be a software-systems design framework, design rules and techniques which together enable system designers to make guarantees about the security, safety and reliability of software systems. These guarantees are based on the rigour of mathematical proof.
[bold emphasis added]
Another member of the L4 microkernel family runs in over 1.5 billion mobile devices.
Perhaps seL4 will follow.
Update: It’s in the same pipeline.