3 ms·
> formal methods based on proof assistants never took off A few examples of large scale industrial projects using formal assistants: seL4: A proven correct co
by mbrodersen 6y ago
> formal methods based on proof assistants never took off
A few examples of large scale industrial projects using formal assistants:
seL4: A proven correct commercial OS used in billions of mobile devices.
CompCert: A proven correct C compiler used by Airbus for avionics software.
ARM: End-to-end verification of CPUs (https://alastairreid.github.io/papers/CAV_16 https://alastairreid.github.io/papers/CAV_16).
There are many more.