seL4 is the world's first formally verified kernel from the specification to the implementation. The applications are endless, from drones, medical device implants, and self-driving vehicles.
However, there are a couple of caveats.
First, the proofs themselves are cryptic and pages and pages long. It takes considerably effort for one to understand, tweak, and even modify the specification and subsequent proofs.
Second, it's kernel only and does not include device drivers. As we have seen before (e.g., Juniper router attack) many of the targeted internet domain attacks occur at low levels like the firmware. In this case seL4 provides no detection.
Third, the guarantees are only as good as the spec. Who's responsible to define the specification? The guarantee is only bug-free deviation against the specification.
The future is quite bright. Hopefully this will spawn more innovations and implementations in the area of end-to-end formal verification and implementation.
