Formally verified software still has its limitations. Knuth's famous "Beware of bugs in the above code; I have only proved it correct, not tried it." is funny but true.

Formal verification is a good and useful tool, but it provably cannot cover the entire system, and practical limitations will limit it even further.

Formal verification of source code is still subject to compiler bugs. Formally proven compilers are subject to bugs in the larger system (IIRC Csmith was able to find an incorrectness in code generated by CompCert because of a bug in a system header file).