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

Formally verified gets rid of a class of bugs, but you can still have a bad specification. Also what is a bug might change in the future. I imagine as we learn more from plane crashes what is ok today might be a big tomorrow.

Check this out: https://news.ycombinator.com/item?id=22082869

How Amazon Web Services Uses Formal Methods

Think of it as writing the software in a very barebones language and then requiring unit test coverage of all possible input combinations, asserting the full output. A lot of work, but gives you reasonable certainty that your code is indeed correct (does what it was designed to do). That's at least what I learned in that one masters course. After implementing the final assignment, which was equivalent to some three lines of C and took a team of four "the semester", I've decided to not look any further into it. It is being used in applications that warrant actual investment into bug-free code, say nuclear reactor control or helicopter rotor control.

I would imagine the MCAS belongs to this class. But even if your software is correct, the design it implements might be flawed, say by assuming the input you get from a single fallible sensor is to be trusted.

Formal verification just proves that the software conforms to some specification. How do you proved the spec has no mistakes?

There's a fourth one but its undefined.

Is it enterprise ready like this one https://gist.github.com/lolzballs/2152bc0f31ee0286b722 ? Even that one is alpha quality, no soap support, no saml2.0, xml is not even mentioned once. It needs couple of major versions before it can reach production in express, standard, developer, enterprise and pro distributions.

But the kernel and/or the CPU you are running it on does.