> a few thousands lines of code when I looked at it a while back. That's not true anymore. Have a look at CompCert, CakeML or CertiKOS, for example. Verificat

> a few thousands lines of code when I looked at it a while back. That's not true anymore. Have a look at CompCert, CakeML or CertiKOS, for example. Verification still takes a big effort, but it's getting better a lot.