On Nov 22, 2020, at 10:01, Demi M. Obenour demiobenour@gmail.com 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.