[lower]

> 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.