Sadly, formal verification works only for small amount of code, a few thousands lines of code when I looked at it a while back. It doesn't stop us from imagining a fully verified firefox though.
> 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.
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.