[seL4] Re: RFC-5: seL4 Core Platform

On 23 Nov 2020, at 05:36, Matthew Fernandez mailto:matthew.fernandez@gmail.com> wrote: Inria and Airbus have had success doing this since at least ~2005. If you want to read about this, Sandrine Blazy and Xavier Leroy have discussed it in some prior publications. Today I believe this process is supported commercially by the company AbsInt. AbsInt AFAIK does high-assurance worst-case execution-time (WCET) analysis, not general software assurance. But yes, Airbus has been a pioneer in formal verification of critical avionics software, for at least 30 years. Gernot