News for hackers. Stuff that matters.

A comment on L4 microkernels: The lessons from 20 years of research and deployment. Parent comment

Re:L4 microkernels: The lessons from 20 years of research an... by DashRattlesnake on Tuesday September 20, 2016 @11:29AM (#12540259)
> The full verification of seL4 came a lot earlier (by about a decade) than I thought possible.

Is it a full verification yet? I am by no means an expert, but IIRC, they were still using a simplified model MMU in their proofs.

[ Parent | on HN ]
Re:L4 microkernels: The lessons from 20 years of research an... by cmrx64 on Tuesday September 20, 2016 @12:10PM (#12540609)
It's a simplified model, but it's well validated. Without connecting the proofs to a formally verified chip, it's about the best you can do.
[ Parent | on HN ]