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

On 11/22/20 1:36 PM, Matthew Fernandez wrote:

...

On Nov 22, 2020, at 10:01, Demi M. Obenour wrote:

(Speaking of avionics: is it possible to scale formal verification to systems of that scale? I would love to see formally-verified avionics software.)

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.

Is this full functional verification, or “merely” proving freedom from runtime errors? (Quotes because proving freedom from runtime errors is still a substantial victory.) Sincerely, Demi